Skip to content

Commit ac6b844

Browse files
CoolRmalCoolRmal
committed
fix
1 parent 4c8b20b commit ac6b844

2 files changed

Lines changed: 25 additions & 162 deletions

File tree

‎Mathlib/Analysis/Calculus/DerivativeTest.lean‎

Lines changed: 25 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
/-
22
Copyright (c) 2024 Bjørn Kjos-Hanssen. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Bjørn Kjos-Hanssen, Patrick Massot, Floris van Doorn, Jireh Loreaux, Eric Wieser
4+
Authors: Bjørn Kjos-Hanssen, Patrick Massot, Floris van Doorn, Jireh Loreaux, Eric Wieser,
5+
Yongxi Lin, Louis (Yiyang) Liu
56
-/
67
module
78

@@ -95,7 +96,7 @@ lemma isMaxOn_Ioo_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b
9596
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
9697
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
9798
IsMaxOn f (Ioo a c) b := by
98-
refine isMaxOn_of_mono_anti_Ioo ?_ ?_
99+
refine isMaxOn_Ioo_of_mono_anti ?_ ?_
99100
· apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc h hd₀) <;> simp_all
100101
· apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico h hd₁) <;> simp_all
101102

@@ -105,7 +106,7 @@ lemma isMaxOn_Ioc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f
105106
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
106107
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
107108
IsMaxOn f (Ioc a c) b := by
108-
refine isMaxOn_of_mono_anti_Ioc ?_ ?_
109+
refine isMaxOn_Ioc_of_mono_anti ?_ ?_
109110
· apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all
110111
· apply antitoneOn_of_deriv_nonpos (convex_Icc b c) (continuousOn_Icc hb hc hd₁) <;> simp_all
111112

@@ -115,7 +116,7 @@ lemma isMaxOn_Ico_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
115116
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
116117
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
117118
IsMaxOn f (Ico a c) b := by
118-
refine isMaxOn_of_mono_anti_Ico ?_ ?_
119+
refine isMaxOn_Ico_of_mono_anti ?_ ?_
119120
· apply monotoneOn_of_deriv_nonneg (convex_Icc a b) (continuousOn_Icc ha hb hd₀) <;> simp_all
120121
· apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico hb hd₁) <;> simp_all
121122

@@ -125,7 +126,7 @@ lemma isMaxOn_Icc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
125126
(hc : ContinuousAt f c) (hd₀ : DifferentiableOn ℝ f (Ioo a b))
126127
(hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
127128
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Icc a c) b := by
128-
refine isMaxOn_of_mono_anti_Icc ?_ ?_
129+
refine isMaxOn_Icc_of_mono_anti ?_ ?_
129130
· apply monotoneOn_of_deriv_nonneg (convex_Icc a b) (continuousOn_Icc ha hb hd₀) <;> simp_all
130131
· apply antitoneOn_of_deriv_nonpos (convex_Icc b c) (continuousOn_Icc hb hc hd₁) <;> simp_all
131132

@@ -135,7 +136,7 @@ lemma isMaxOn_Ioi_of_deriv {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
135136
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
136137
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0) :
137138
IsMaxOn f (Ioi a) b := by
138-
refine isMaxOn_of_mono_anti_Ioi ?_ ?_
139+
refine isMaxOn_Ioi_of_mono_anti ?_ ?_
139140
· apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all
140141
· apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all
141142

@@ -145,7 +146,7 @@ lemma isMaxOn_Ici_of_deriv {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a)
145146
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
146147
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0) :
147148
IsMaxOn f (Ici a) b := by
148-
refine isMaxOn_of_mono_anti_Ici ?_ ?_
149+
refine isMaxOn_Ici_of_mono_anti ?_ ?_
149150
· apply monotoneOn_of_deriv_nonneg (convex_Icc a b) (continuousOn_Icc ha hb hd₀) <;> simp_all
150151
· apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all
151152

@@ -155,7 +156,7 @@ lemma isMaxOn_Iio_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
155156
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
156157
(h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
157158
IsMaxOn f (Iio c) b := by
158-
refine isMaxOn_of_mono_anti_Iio ?_ ?_
159+
refine isMaxOn_Iio_of_mono_anti ?_ ?_
159160
· apply monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀) <;> simp_all
160161
· apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico hb hd₁) <;> simp_all
161162

@@ -165,7 +166,7 @@ lemma isMaxOn_Iic_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
165166
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
166167
(h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
167168
IsMaxOn f (Iic c) b := by
168-
refine isMaxOn_of_mono_anti_Iic ?_ ?_
169+
refine isMaxOn_Iic_of_mono_anti ?_ ?_
169170
· apply monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀) <;> simp_all
170171
· apply antitoneOn_of_deriv_nonpos (convex_Icc b c) (continuousOn_Icc hb hc hd₁) <;> simp_all
171172

@@ -174,12 +175,10 @@ nonpositive on `(b, ∞)`. Then `f` attains its maximum on `ℝ` at `b`. -/
174175
lemma isMaxOn_univ_of_deriv {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b)
175176
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
176177
(h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0) :
177-
IsMaxOn f univ b :=
178-
isMaxOn_of_mono_anti_univ
179-
(monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀) (by simp_all)
180-
(by simp_all))
181-
(antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) (by simp_all)
182-
(by simp_all))
178+
IsMaxOn f univ b := by
179+
refine isMaxOn_univ_of_mono_anti ?_ ?_
180+
· apply monotoneOn_of_deriv_nonneg (convex_Iic b) (continuousOn_Iic hb hd₀) <;> simp_all
181+
· apply antitoneOn_of_deriv_nonpos (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all
183182

184183
/-- The First-Derivative Test from calculus, maxima version.
185184
Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `(a,b)`
@@ -196,7 +195,7 @@ lemma isMinOn_Ioo_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b
196195
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
197196
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
198197
IsMinOn f (Ioo a c) b := by
199-
refine isMinOn_of_anti_mono_Ioo ?_ ?_
198+
refine isMinOn_Ioo_of_anti_mono ?_ ?_
200199
· apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc h hd₀) <;> simp_all
201200
· apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico h hd₁) <;> simp_all
202201

@@ -206,7 +205,7 @@ lemma isMinOn_Ioc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f
206205
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
207206
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
208207
IsMinOn f (Ioc a c) b := by
209-
refine isMinOn_of_anti_mono_Ioc ?_ ?_
208+
refine isMinOn_Ioc_of_anti_mono ?_ ?_
210209
· apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all
211210
· apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁) <;> simp_all
212211

@@ -216,7 +215,7 @@ lemma isMinOn_Ico_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
216215
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
217216
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
218217
IsMinOn f (Ico a c) b := by
219-
refine isMinOn_of_anti_mono_Ico ?_ ?_
218+
refine isMinOn_Ico_of_anti_mono ?_ ?_
220219
· apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀) <;> simp_all
221220
· apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁) <;> simp_all
222221

@@ -226,7 +225,7 @@ lemma isMinOn_Icc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
226225
(hc : ContinuousAt f c) (hd₀ : DifferentiableOn ℝ f (Ioo a b))
227226
(hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
228227
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsMinOn f (Icc a c) b := by
229-
refine isMinOn_of_anti_mono_Icc ?_ ?_
228+
refine isMinOn_Icc_of_anti_mono ?_ ?_
230229
· apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀) <;> simp_all
231230
· apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁) <;> simp_all
232231

@@ -236,7 +235,7 @@ lemma isMinOn_Ioi_of_deriv {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
236235
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
237236
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x) :
238237
IsMinOn f (Ioi a) b := by
239-
refine isMinOn_of_anti_mono_Ioi ?_ ?_
238+
refine isMinOn_Ioi_of_anti_mono ?_ ?_
240239
· apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all
241240
· apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all
242241

@@ -246,7 +245,7 @@ lemma isMinOn_Ici_of_deriv {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a)
246245
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
247246
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x) :
248247
IsMinOn f (Ici a) b := by
249-
refine isMinOn_of_anti_mono_Ici ?_ ?_
248+
refine isMinOn_Ici_of_anti_mono ?_ ?_
250249
· apply antitoneOn_of_deriv_nonpos (convex_Icc a b) (continuousOn_Icc ha hb hd₀) <;> simp_all
251250
· apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all
252251

@@ -256,7 +255,7 @@ lemma isMinOn_Iio_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
256255
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
257256
(h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
258257
IsMinOn f (Iio c) b := by
259-
refine isMinOn_of_anti_mono_Iio ?_ ?_
258+
refine isMinOn_Iio_of_anti_mono ?_ ?_
260259
· apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀) <;> simp_all
261260
· apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico hb hd₁) <;> simp_all
262261

@@ -266,7 +265,7 @@ lemma isMinOn_Iic_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
266265
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
267266
(h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
268267
IsMinOn f (Iic c) b := by
269-
refine isMinOn_of_anti_mono_Iic ?_ ?_
268+
refine isMinOn_Iic_of_anti_mono ?_ ?_
270269
· apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀) <;> simp_all
271270
· apply monotoneOn_of_deriv_nonneg (convex_Icc b c) (continuousOn_Icc hb hc hd₁) <;> simp_all
272271

@@ -276,10 +275,9 @@ lemma isMinOn_univ_of_deriv {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b)
276275
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
277276
(h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x) :
278277
IsMinOn f univ b := by
279-
refine isMinOn_of_anti_mono_univ
280-
(antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀) ?_ ?_)
281-
(monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁) ?_ ?_)
282-
<;> simp_all
278+
refine isMinOn_univ_of_anti_mono ?_ ?_
279+
· apply antitoneOn_of_deriv_nonpos (convex_Iic b) (continuousOn_Iic hb hd₀) <;> simp_all
280+
· apply monotoneOn_of_deriv_nonneg (convex_Ici b) (continuousOn_Ici hb hd₁) <;> simp_all
283281

284282
/-- The First-Derivative Test from calculus, minima version. -/
285283
lemma isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c)

‎Mathlib/Topology/Order/OrderClosedExtr.lean‎

Lines changed: 0 additions & 135 deletions
Original file line numberDiff line numberDiff line change
@@ -27,141 +27,6 @@ public section
2727

2828
open Set
2929

30-
variable {α β : Type*} [LinearOrder α] [Preorder β] {s : Set α} {a b c : α} {f : α → β}
31-
32-
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c)`, then the maximum of `f` on `(a, c)` is
33-
attained at `b`. -/
34-
lemma isMaxOn_Ioo_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ico b c)) :
35-
IsMaxOn f (Ioo a c) b := by
36-
intro x hx
37-
by_cases! g₀ : x ≤ b
38-
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀
39-
· refine h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
40-
41-
/-- If `f` is antitone on `(a, b]` and monotone on `[b,c)`, then the minimum of `f` on `(a, c)` is
42-
attained at `b`. -/
43-
lemma isMinOn_Ioo_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) :
44-
IsMinOn f (Ioo a c) b :=
45-
isMaxOn_Ioo_of_mono_anti (β := βᵒᵈ) h₀ h₁
46-
47-
/-- If `f` is monotone on `[a, b]` and antitone on `[b,c)`, then the maximum of `f` on `[a, c)` is
48-
attained at `b`. -/
49-
lemma isMaxOn_Ico_of_mono_anti
50-
(h₀ : MonotoneOn f (Icc a b))
51-
(h₁ : AntitoneOn f (Ico b c)) : IsMaxOn f (Ico a c) b := by
52-
intro x hx
53-
by_cases! g₀ : x ≤ b
54-
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀
55-
· exact h₁ (left_mem_Ico.2 (g₀.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
56-
57-
/-- If `f` is antitone on `[a, b]` and monotone on `[b,c)`, then the minimum of `f` on `[a, c)` is
58-
attained at `b`. -/
59-
lemma isMinOn_Ico_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ico b c)) :
60-
IsMinOn f (Ico a c) b :=
61-
isMaxOn_Ico_of_mono_anti (β := βᵒᵈ) h₀ h₁
62-
63-
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of `f` on `(a, c]` is
64-
attained at `b`. -/
65-
lemma isMaxOn_Ioc_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Icc b c)) :
66-
IsMaxOn f (Ioc a c) b := by
67-
intro x hx
68-
by_cases! g₀ : x ≤ b
69-
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx.1)) g₀
70-
· exact h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
71-
72-
/-- If `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of `f` on `(a, c]` is
73-
attained at `b`. -/
74-
lemma isMinOn_Ioc_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Icc b c)) :
75-
IsMinOn f (Ioc a c) b :=
76-
isMaxOn_Ioc_of_mono_anti (β := βᵒᵈ) h₀ h₁
77-
78-
/-- If `f` is monotone on `[a, b]` and antitone on `[b,c]`, then the maximum of `f` on `[a, c]` is
79-
attained at `b`. -/
80-
lemma isMaxOn_Icc_of_mono_anti (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Icc b c)) :
81-
IsMaxOn f (Icc a c) b := by
82-
intro x hx
83-
by_cases! g₀ : x ≤ b
84-
· exact h₀ ⟨hx.1, g₀⟩ (right_mem_Icc.2 (hx.1.trans g₀)) g₀
85-
· exact h₁ (left_mem_Icc.2 (g₀.le.trans hx.2)) ⟨g₀.le, hx.2⟩ g₀.le
86-
87-
/-- If `f` is antitone on `[a, b]` and monotone on `[b,c]`, then the minimum of `f` on `(a, c]` is
88-
attained at `b`. -/
89-
lemma isMinOn_Icc_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Icc b c)) :
90-
IsMinOn f (Icc a c) b :=
91-
isMaxOn_Icc_of_mono_anti (β := βᵒᵈ) h₀ h₁
92-
93-
/-- If `f` is monotone on `(a, b]` and antitone on `[b,∞)`, then the maximum of `f` on `(a, ∞)` is
94-
attained at `b`. -/
95-
lemma isMaxOn_Ioi_of_mono_anti (h₀ : MonotoneOn f (Ioc a b)) (h₁ : AntitoneOn f (Ici b)) :
96-
IsMaxOn f (Ioi a) b := by
97-
intro x hx
98-
by_cases! g₀ : x ≤ b
99-
· exact h₀ ⟨hx, g₀⟩ (right_mem_Ioc.2 (g₀.trans_lt' hx)) g₀
100-
· exact h₁ self_mem_Ici g₀.le g₀.le
101-
102-
/-- If `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of `f` on `(a, ∞)` is
103-
attained at `b`. -/
104-
lemma isMinOn_Ioi_of_anti_mono (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ici b)) :
105-
IsMinOn f (Ioi a) b :=
106-
isMaxOn_Ioi_of_mono_anti (β := βᵒᵈ) h₀ h₁
107-
108-
/-- If `f` is monotone on `[a, b]` and antitone on `[b,∞)`, then the maximum of `f` on `[a, ∞)` is
109-
attained at `b`. -/
110-
lemma isMaxOn_Ici_of_mono_anti (h₀ : MonotoneOn f (Icc a b)) (h₁ : AntitoneOn f (Ici b)) :
111-
IsMaxOn f (Ici a) b := by
112-
intro x hx
113-
by_cases! g₀ : x ≤ b
114-
· exact h₀ ⟨hx, g₀⟩ (right_mem_Icc.2 (hx.trans g₀)) g₀
115-
· exact h₁ self_mem_Ici g₀.le g₀.le
116-
117-
/-- If `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of `f` on `[a, ∞)` is
118-
attained at `b`. -/
119-
lemma isMinOn_Ici_of_anti_mono (h₀ : AntitoneOn f (Icc a b)) (h₁ : MonotoneOn f (Ici b)) :
120-
IsMinOn f (Ici a) b :=
121-
isMaxOn_Ici_of_mono_anti (β := βᵒᵈ) h₀ h₁
122-
123-
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,a)`, then the maximum of `f` on `(-∞, a)` is
124-
attained at `b`. -/
125-
lemma isMaxOn_Iio_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ico b a)) :
126-
IsMaxOn f (Iio a) b := by
127-
intro x hx
128-
by_cases! g₀ : x ≤ b
129-
· exact h₀ g₀ self_mem_Iic g₀
130-
· exact h₁ (left_mem_Ico.2 (g₀.trans hx)) ⟨g₀.le, hx⟩ g₀.le
131-
132-
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,a)`, then the minimum of `f` on `(-∞, a)` is
133-
attained at `b`. -/
134-
lemma isMinOn_Iio_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ico b a)) :
135-
IsMinOn f (Iio a) b :=
136-
isMaxOn_Iio_of_mono_anti (β := βᵒᵈ) h₀ h₁
137-
138-
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,a]`, then the maximum of
139-
`f` on `(-∞, a]` is attained at `b`. -/
140-
lemma isMaxOn_Iic_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Icc b a)) :
141-
IsMaxOn f (Iic a) b := by
142-
intro x hx
143-
by_cases! g₀ : x ≤ b
144-
· exact h₀ g₀ self_mem_Iic g₀
145-
· exact h₁ (left_mem_Icc.2 (g₀.le.trans hx)) ⟨g₀.le, hx⟩ g₀.le
146-
147-
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,a]`, then the minimum of `f` on `(-∞, a]` is
148-
attained at `b`. -/
149-
lemma isMinOn_Iic_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Icc b a)) :
150-
IsMinOn f (Iic a) b :=
151-
isMaxOn_Iic_of_mono_anti (β := βᵒᵈ) h₀ h₁
152-
153-
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,∞)`, then the maximum of `f` is attained
154-
at `b`. -/
155-
lemma isMaxOn_univ_of_mono_anti (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ici b)) :
156-
IsMaxOn f univ b :=
157-
fun x _ => by rcases le_total x b <;> aesop
158-
159-
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,∞)`, then the minimum of `f` is attained
160-
at `b`. -/
161-
lemma isMinOn_univ_of_anti_mono (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ici b)) :
162-
IsMinOn f univ b :=
163-
isMaxOn_univ_of_mono_anti (β := βᵒᵈ) h₀ h₁
164-
16530
/-- If `f` is monotone on `(a,b]` and antitone on `[b,c)` then `f` has
16631
a local maximum at `b`. -/
16732
lemma isLocalMax_of_mono_anti

0 commit comments

Comments
 (0)