Skip to content

Commit 3872f4d

Browse files
CoolRmalCoolRmal
committed
update
1 parent 8c13ace commit 3872f4d

2 files changed

Lines changed: 158 additions & 60 deletions

File tree

‎Mathlib/Analysis/Calculus/DerivativeTest.lean‎

Lines changed: 41 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -51,39 +51,64 @@ public section
5151

5252
open Set Topology
5353

54+
/-- If `f : ℝ → ℝ` id differentiable on a set `s` and continuous at a point `b`, then `f` is
55+
continuous on `s ∪ {b}`. -/
56+
private lemma DifferentiableOn.continuousOn_union {f : ℝ → ℝ} {s : Set ℝ}
57+
(hf : DifferentiableOn ℝ f s) {b : ℝ} (hfb : ContinuousAt f b) :
58+
59+
/-- Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on
60+
`(a,b)`, and the derivative `f'` is nonpositive on `(b,c)`. Then `f` attains its maximum on `(a,c)`
61+
at `b`. -/
62+
lemma isMaxOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c)
63+
(h : ContinuousAt f b)
64+
(hd₀ : DifferentiableOn ℝ f (Ioo a b))
65+
(hd₁ : DifferentiableOn ℝ f (Ioo b c))
66+
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
67+
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Ioo a c) b :=
68+
have hIoc : ContinuousOn f (Ioc a b) := Ioo_union_right g₀ ▸
69+
hd₀.continuousOn.union_continuousAt (isOpen_Ioo (a := a) (b := b)) (by simp_all)
70+
have hIco : ContinuousOn f (Ico b c) := Ioo_union_left g₁ ▸
71+
hd₁.continuousOn.union_continuousAt (isOpen_Ioo (a := b) (b := c)) (by simp_all)
72+
isMaxOn_of_mono_anti_Ioo g₀ g₁
73+
(monotoneOn_of_deriv_nonneg (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
74+
(antitoneOn_of_deriv_nonpos (convex_Ico b c) hIco (by simp_all) (by simp_all))
5475

5576
/-- The First-Derivative Test from calculus, maxima version.
5677
Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`,
5778
the derivative `f'` is nonnegative on `(a,b)`, and
58-
the derivative `f'` is nonpositive on `(b,c)`. Then `f` has a local maximum at `a`. -/
79+
the derivative `f'` is nonpositive on `(b,c)`. Then `f` has a local maximum at `b`. -/
5980
lemma isLocalMax_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c)
6081
(h : ContinuousAt f b)
6182
(hd₀ : DifferentiableOn ℝ f (Ioo a b))
6283
(hd₁ : DifferentiableOn ℝ f (Ioo b c))
6384
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
6485
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsLocalMax f b :=
65-
have hIoc : ContinuousOn f (Ioc a b) :=
66-
Ioo_union_right g₀ ▸ hd₀.continuousOn.union_continuousAt (isOpen_Ioo (a := a) (b := b))
67-
(by simp_all)
68-
have hIco : ContinuousOn f (Ico b c) :=
69-
Ioo_union_left g₁ ▸ hd₁.continuousOn.union_continuousAt (isOpen_Ioo (a := b) (b := c))
70-
(by simp_all)
71-
isLocalMax_of_mono_anti g₀ g₁
72-
(monotoneOn_of_deriv_nonneg (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
73-
(antitoneOn_of_deriv_nonpos (convex_Ico b c) hIco (by simp_all) (by simp_all))
86+
(isMaxOn_of_deriv_Ioo g₀ g₁ h hd₀ hd₁ h₀ h₁).isLocalMax (Ioo_mem_nhds g₀ g₁)
7487

88+
/-- Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on
89+
`(a,b)`, and the derivative `f'` is nonnegative on `(b,c)`. Then `f` attains its minimum on `(a,c)`
90+
at `b`. -/
91+
lemma isMinOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c)
92+
(h : ContinuousAt f b)
93+
(hd₀ : DifferentiableOn ℝ f (Ioo a b))
94+
(hd₁ : DifferentiableOn ℝ f (Ioo b c))
95+
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
96+
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsMinOn f (Ioo a c) b :=
97+
have hIoc : ContinuousOn f (Ioc a b) := Ioo_union_right g₀ ▸
98+
hd₀.continuousOn.union_continuousAt (isOpen_Ioo (a := a) (b := b)) (by simp_all)
99+
have hIco : ContinuousOn f (Ico b c) := Ioo_union_left g₁ ▸
100+
hd₁.continuousOn.union_continuousAt (isOpen_Ioo (a := b) (b := c)) (by simp_all)
101+
isMinOn_of_anti_mono_Ioo g₀ g₁
102+
(antitoneOn_of_deriv_nonpos (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
103+
(monotoneOn_of_deriv_nonneg (convex_Ico b c) hIco (by simp_all) (by simp_all))
75104

76105
/-- The First-Derivative Test from calculus, minima version. -/
77106
lemma isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ}
78107
(g₀ : a < b) (g₁ : b < c) (h : ContinuousAt f b)
79108
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
80109
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
81-
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b := by
82-
have := isLocalMax_of_deriv_Ioo (f := -f) g₀ g₁
83-
(by simp_all) hd₀.neg hd₁.neg
84-
(fun x hx => deriv.neg (f := f) ▸ Left.nonneg_neg_iff.mpr <| h₀ x hx)
85-
(fun x hx => deriv.neg (f := f) ▸ Left.neg_nonpos_iff.mpr <| h₁ x hx)
86-
exact (neg_neg f) ▸ IsLocalMax.neg this
110+
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b :=
111+
(isMinOn_of_deriv_Ioo g₀ g₁ h hd₀ hd₁ h₀ h₁).isLocalMin (Ioo_mem_nhds g₀ g₁)
87112

88113
/-- The First-Derivative Test from calculus, maxima version,
89114
expressed in terms of left and right filters. -/

‎Mathlib/Topology/Order/OrderClosedExtr.lean‎

Lines changed: 117 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
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
4+
Authors: Bjørn Kjos-Hanssen, Patrick Massot, Yongxi Lin
55
-/
66
module
77

@@ -27,70 +27,143 @@ public section
2727

2828
open Set Topology Filter
2929

30-
variable {α β : Type*} [Preorder β] {s : Set α} {a b c : α} {f : α → β}
31-
32-
section PartialOrder
33-
34-
variable [PartialOrder α]
35-
36-
/-- If `b ≤ c`, and `f` is antitone on `[b,c)`, then the maximum of
37-
`f` on `[b, c)` is attained at `b`. -/
38-
lemma isMaxOn_of_anti_Ico (g₁ : b ≤ c) (h₁ : AntitoneOn f (Ico b c)) :
39-
IsMaxOn f (Ico b c) b := by
40-
rcases g₁.lt_or_eq with (hp | hq) <;> intro
41-
· aesop
42-
· simp [show Ico b c = ∅ by rw [Ico_eq_empty_iff]; grind]
43-
44-
/-- If `b ≤ c`, and `f` is monotone on `[b,c)`, then the minimum of
45-
`f` on `[b, c)` is attained at `b`. -/
46-
lemma isMinOn_of_mono_Ico (g₁ : b ≤ c) (h₁ : MonotoneOn f (Ico b c)) :
47-
IsMinOn f (Ico b c) b :=
48-
isMaxOn_of_anti_Ico (β := βᵒᵈ) g₁ h₁
49-
50-
/-- If `b ≤ c`, and `f` is antitone on `[b,c]`, then the maximum of
51-
`f` on `[b, c]` is attained at `b`. -/
52-
lemma isMaxOn_of_anti_Icc (g₁ : b ≤ c) (h₁ : AntitoneOn f (Icc b c)) :
53-
IsMaxOn f (Icc b c) b := by
54-
rcases g₁.lt_or_eq with (hp | hq) <;> intro
55-
· aesop
56-
· simp_all
57-
58-
/-- If `b ≤ c`, and `f` is monotone on `[b,c]`, then the minimum of
59-
`f` on `[b, c]` is attained at `b`. -/
60-
lemma isMinOn_of_mono_Icc (g₁ : b ≤ c) (h₁ : MonotoneOn f (Icc b c)) :
61-
IsMinOn f (Icc b c) b :=
62-
isMaxOn_of_anti_Icc (β := βᵒᵈ) g₁ h₁
63-
64-
end PartialOrder
65-
66-
variable [LinearOrder α]
30+
variable {α β : Type*} [LinearOrder α] [Preorder β] {s : Set α} {a b c : α} {f : α → β}
6731

6832
/-- If `a` is an element of a set `s`, and `f` is monotone on `s ∩ (-∞, a]` and antitone on
6933
`s ∩ [a, ∞)`, then the maximum of `f` on `s` is attained at `a`. -/
7034
lemma isMaxOn_of_mono_anti (ha : a ∈ s) (h₀ : MonotoneOn f (s ∩ Set.Iic a))
7135
(h₁ : AntitoneOn f (s ∩ Set.Ici a)) : IsMaxOn f s a :=
7236
fun x _ => by rcases le_total x a <;> aesop
7337

38+
/-- If `a` is an element of a set `s`, and `f` is antitone on `s ∩ (-∞, a]` and monotone on
39+
`s ∩ [a, ∞)`, then the minimum of `f` on `s` is attained at `a`. -/
40+
lemma isMinOn_of_anti_mono (ha : a ∈ s) (h₀ : AntitoneOn f (s ∩ Set.Iic a))
41+
(h₁ : MonotoneOn f (s ∩ Set.Ici a)) : IsMinOn f s a :=
42+
isMaxOn_of_mono_anti (β := βᵒᵈ) ha h₀ h₁
43+
7444
/-- If `a < b < c`, and `f` is monotone on `(a, b]` and antitone on `[b,c)`, then the maximum of
7545
`f` on `(a, c)` is attained at `b`. -/
7646
lemma isMaxOn_of_mono_anti_Ioo (g₀ : a < b) (g₁ : b < c)
7747
(h₀ : MonotoneOn f (Ioc a b))
7848
(h₁ : AntitoneOn f (Ico b c)) : IsMaxOn f (Ioo a c) b :=
7949
fun x _ => by rcases le_total x b <;> aesop
8050

51+
/-- If `a < b < c`, and `f` is antitone on `(a, b]` and monotone on `[b,c)`, then the minimum of
52+
`f` on `(a, c)` is attained at `b`. -/
53+
lemma isMinOn_of_anti_mono_Ioo (g₀ : a < b) (g₁ : b < c)
54+
(h₀ : AntitoneOn f (Ioc a b))
55+
(h₁ : MonotoneOn f (Ico b c)) : IsMinOn f (Ioo a c) b :=
56+
isMaxOn_of_mono_anti_Ioo (β := βᵒᵈ) g₀ g₁ h₀ h₁
57+
8158
/-- If `a ≤ b < c`, and `f` is monotone on `[a, b]` and antitone on `[b,c)`, then the maximum of
8259
`f` on `[a, c)` is attained at `b`. -/
8360
lemma isMaxOn_of_mono_anti_Ico (g₀ : a ≤ b) (g₁ : b < c)
8461
(h₀ : MonotoneOn f (Icc a b))
8562
(h₁ : AntitoneOn f (Ico b c)) : IsMaxOn f (Ico a c) b :=
8663
fun x _ => by rcases le_total x b <;> aesop
8764

88-
lemma isMinOn_of_anti_mono
89-
{α β : Type*} [LinearOrder α] [Preorder β]
90-
{s : Set α} {a : α} (ha : a ∈ s) {f : α → β}
91-
(h₀ : AntitoneOn f (s ∩ Set.Iic a))
92-
(h₁ : MonotoneOn f (s ∩ Set.Ici a)) : IsMinOn f s a :=
93-
isMaxOn_of_mono_anti (β := βᵒᵈ) ha h₀ h₁
65+
/-- If `a ≤ b < c`, and `f` is antitone on `[a, b]` and monotone on `[b,c)`, then the minimum of
66+
`f` on `[a, c)` is attained at `b`. -/
67+
lemma isMinOn_of_anti_mono_Ico (g₀ : a ≤ b) (g₁ : b < c)
68+
(h₀ : AntitoneOn f (Icc a b))
69+
(h₁ : MonotoneOn f (Ico b c)) : IsMinOn f (Ico a c) b :=
70+
isMaxOn_of_mono_anti_Ico (β := βᵒᵈ) g₀ g₁ h₀ h₁
71+
72+
/-- If `a < b ≤ c`, and `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of
73+
`f` on `(a, c]` is attained at `b`. -/
74+
lemma isMaxOn_of_mono_anti_Ioc (g₀ : a < b) (g₁ : b ≤ c)
75+
(h₀ : MonotoneOn f (Ioc a b))
76+
(h₁ : AntitoneOn f (Icc b c)) : IsMaxOn f (Ioc a c) b :=
77+
fun x _ => by rcases le_total x b <;> aesop
78+
79+
/-- If `a < b ≤ c`, and `f` is monotone on `(a, b]` and antitone on `[b,c]`, then the maximum of
80+
`f` on `(a, c]` is attained at `b`. -/
81+
lemma isMinOn_of_anti_mono_Ioc (g₀ : a < b) (g₁ : b ≤ c)
82+
(h₀ : AntitoneOn f (Ioc a b))
83+
(h₁ : MonotoneOn f (Icc b c)) : IsMinOn f (Ioc a c) b :=
84+
isMaxOn_of_mono_anti_Ioc (β := βᵒᵈ) g₀ g₁ h₀ h₁
85+
86+
/-- If `a ≤ b ≤ c`, and `f` is monotone on `[a, b]` and antitone on `[b,c]`, then the maximum of
87+
`f` on `[a, c]` is attained at `b`. -/
88+
lemma isMaxOn_of_mono_anti_Icc (g₀ : a ≤ b) (g₁ : b ≤ c)
89+
(h₀ : MonotoneOn f (Icc a b))
90+
(h₁ : AntitoneOn f (Icc b c)) : IsMaxOn f (Icc a c) b :=
91+
fun x _ => by rcases le_total x b <;> aesop
92+
93+
/-- If `a ≤ b ≤ c`, and `f` is antitone on `[a, b]` and monotone on `[b,c]`, then the minimum of
94+
`f` on `(a, c]` is attained at `b`. -/
95+
lemma isMinOn_of_anti_mono_Icc (g₀ : a ≤ b) (g₁ : b ≤ c)
96+
(h₀ : AntitoneOn f (Icc a b))
97+
(h₁ : MonotoneOn f (Icc b c)) : IsMinOn f (Icc a c) b :=
98+
isMaxOn_of_mono_anti_Icc (β := βᵒᵈ) g₀ g₁ h₀ h₁
99+
100+
/-- If `a < b`, and `f` is monotone on `(a, b]` and antitone on `[b,∞)`, then the maximum of
101+
`f` on `(a, ∞)` is attained at `b`. -/
102+
lemma isMaxOn_of_mono_anti_Ioi (g₀ : a < b)
103+
(h₀ : MonotoneOn f (Ioc a b))
104+
(h₁ : AntitoneOn f (Ici b)) : IsMaxOn f (Ioi a) b :=
105+
fun x _ => by rcases le_total x b <;> aesop
106+
107+
/-- If `a < b`, and `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of
108+
`f` on `(a, ∞)` is attained at `b`. -/
109+
lemma isMinOn_of_anti_mono_Ioi (g₀ : a < b)
110+
(h₀ : AntitoneOn f (Ioc a b))
111+
(h₁ : MonotoneOn f (Ici b)) : IsMinOn f (Ioi a) b :=
112+
isMaxOn_of_mono_anti_Ioi (β := βᵒᵈ) g₀ h₀ h₁
113+
114+
/-- If `a ≤ b`, and `f` is monotone on `[a, b]` and antitone on `[b,∞)`, then the maximum of
115+
`f` on `[a, ∞)` is attained at `b`. -/
116+
lemma isMaxOn_of_mono_anti_Ici (g₀ : a ≤ b)
117+
(h₀ : MonotoneOn f (Icc a b))
118+
(h₁ : AntitoneOn f (Ici b)) : IsMaxOn f (Ici a) b :=
119+
fun x _ => by rcases le_total x b <;> aesop
120+
121+
/-- If `a < b`, and `f` is antitone on `(a, b]` and monotone on `[b,∞)`, then the minimum of
122+
`f` on `[a, ∞)` is attained at `b`. -/
123+
lemma isMinOn_of_anti_mono_Ici (g₀ : a ≤ b)
124+
(h₀ : AntitoneOn f (Icc a b))
125+
(h₁ : MonotoneOn f (Ici b)) : IsMinOn f (Ici a) b :=
126+
isMaxOn_of_mono_anti_Ici (β := βᵒᵈ) g₀ h₀ h₁
127+
128+
/-- If `b < a`, and `f` is monotone on `(-∞, b]` and antitone on `[b,a)`, then the maximum of
129+
`f` on `(-∞, a)` is attained at `b`. -/
130+
lemma isMaxOn_of_mono_anti_Iio (g₀ : b < a)
131+
(h₀ : MonotoneOn f (Iic b))
132+
(h₁ : AntitoneOn f (Ico b a)) : IsMaxOn f (Iio a) b :=
133+
fun x _ => by rcases le_total x b <;> aesop
134+
135+
/-- If `b < a`, and `f` is antitone on `(-∞, b]` and monotone on `[b,a)`, then the minimum of
136+
`f` on `(-∞, a)` is attained at `b`. -/
137+
lemma isMinOn_of_anti_mono_Iio (g₀ : b < a)
138+
(h₀ : AntitoneOn f (Iic b))
139+
(h₁ : MonotoneOn f (Ico b a)) : IsMinOn f (Iio a) b :=
140+
isMaxOn_of_mono_anti_Iio (β := βᵒᵈ) g₀ h₀ h₁
141+
142+
/-- If `b ≤ a`, and `f` is monotone on `(-∞, b]` and antitone on `[b,a]`, then the maximum of
143+
`f` on `(-∞, a]` is attained at `b`. -/
144+
lemma isMaxOn_of_mono_anti_Iic (g₀ : b ≤ a)
145+
(h₀ : MonotoneOn f (Iic b))
146+
(h₁ : AntitoneOn f (Icc b a)) : IsMaxOn f (Iic a) b :=
147+
fun x _ => by rcases le_total x b <;> aesop
148+
149+
/-- If `b < a`, and `f` is antitone on `(-∞, b]` and monotone on `[b,a]`, then the minimum of
150+
`f` on `(-∞, a]` is attained at `b`. -/
151+
lemma isMinOn_of_anti_mono_Iic (g₀ : b ≤ a)
152+
(h₀ : AntitoneOn f (Iic b))
153+
(h₁ : MonotoneOn f (Icc b a)) : IsMinOn f (Iic a) b :=
154+
isMaxOn_of_mono_anti_Iic (β := βᵒᵈ) g₀ h₀ h₁
155+
156+
/-- If `f` is monotone on `(-∞, b]` and antitone on `[b,∞)`, then the maximum of `f` is attained
157+
at `b`. -/
158+
lemma isMaxOn_of_mono_anti_univ (h₀ : MonotoneOn f (Iic b)) (h₁ : AntitoneOn f (Ici b)) :
159+
IsMaxOn f univ b :=
160+
fun x _ => by rcases le_total x b <;> aesop
161+
162+
/-- If `f` is antitone on `(-∞, b]` and monotone on `[b,∞)`, then the minimum of `f` is attained
163+
at `b`. -/
164+
lemma isMinOn_of_anti_mono_univ (h₀ : AntitoneOn f (Iic b)) (h₁ : MonotoneOn f (Ici b)) :
165+
IsMinOn f univ b :=
166+
isMaxOn_of_mono_anti_univ (β := βᵒᵈ) h₀ h₁
94167

95168
/-- If `f` is monotone on `(a,b]` and antitone on `[b,c)` then `f` has
96169
a local maximum at `b`. -/

0 commit comments

Comments
 (0)