Skip to content

Commit a0daec4

Browse files
CoolRmalCoolRmal
committed
Update DerivativeTest.lean
1 parent 0a82ae8 commit a0daec4

1 file changed

Lines changed: 51 additions & 12 deletions

File tree

‎Mathlib/Analysis/Calculus/DerivativeTest.lean‎

Lines changed: 51 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -51,26 +51,65 @@ 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) :
54+
/-- If `f` is continuous at `b` and differentiable on `(a, b)`, then `f` is continuous on
55+
`(a, b]`. -/
56+
private lemma continuousOn_Ioc {f : ℝ → ℝ} {a b : ℝ} (g₀ : a < b) (h : ContinuousAt f b)
57+
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) : ContinuousOn f (Ioc a b) :=
58+
Ioo_union_right g₀ ▸ hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
59+
60+
/-- If `f` is continuous at `a` and differentiable on `(a, b)`, then `f` is continuous on
61+
`[a, b)`. -/
62+
private lemma continuousOn_Ico {f : ℝ → ℝ} {a b : ℝ} (g₀ : a < b) (h : ContinuousAt f a)
63+
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) : ContinuousOn f (Ico a b) :=
64+
Ioo_union_left g₀ ▸ hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
5865

5966
/-- 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`. -/
67+
`(a, b)`, and the derivative `f'` is nonpositive on `(b, c)`. Then `f` attains its maximum on
68+
`(a, c)` at `b`. -/
6269
lemma isMaxOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c)
6370
(h : ContinuousAt f b)
6471
(hd₀ : DifferentiableOn ℝ f (Ioo a b))
6572
(hd₁ : DifferentiableOn ℝ f (Ioo b c))
6673
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
6774
(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)
7275
isMaxOn_of_mono_anti_Ioo g₀ g₁
76+
(monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc g₀ h hd₀) (by simp_all)
77+
(by simp_all))
78+
(antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico g₁ h hd₁) (by simp_all)
79+
(by simp_all))
80+
81+
/-- Suppose `a < b ≤ c`, `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is
82+
nonnegative on `(a, b)`, and the derivative `f'` is nonpositive on `(b, c)`. Then `f` attains its
83+
maximum on `(a, c]` at `b`. -/
84+
lemma isMaxOn_of_deriv_Ioc {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b ≤ c)
85+
(hb : ContinuousAt f b) (hc : ContinuousAt f c)
86+
(hd₀ : DifferentiableOn ℝ f (Ioo a b))
87+
(hd₁ : DifferentiableOn ℝ f (Ioo b c))
88+
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
89+
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Ioc a c) b :=
90+
have hIoc : ContinuousOn f (Ioc a b) := Ioo_union_right g₀ ▸
91+
hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
92+
have hIcc : ContinuousOn f (Icc b c) := Ioo_union_both g₁ ▸
93+
hd₁.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
94+
isMaxOn_of_mono_anti_Ioc g₀ g₁
7395
(monotoneOn_of_deriv_nonneg (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
96+
(antitoneOn_of_deriv_nonpos (convex_Icc b c) hIcc (by simp_all) (by simp_all))
97+
98+
/-- Suppose `a ≤ b < c`, `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is
99+
nonnegative on `(a,b)`, and the derivative `f'` is nonpositive on `(b,c)`. Then `f` attains its
100+
maximum on `(a,c]` at `b`. -/
101+
lemma isMaxOn_of_deriv_Ico {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a ≤ b) (g₁ : b < c)
102+
(ha : ContinuousAt f a) (hb : ContinuousAt f b)
103+
(hd₀ : DifferentiableOn ℝ f (Ioo a b))
104+
(hd₁ : DifferentiableOn ℝ f (Ioo b c))
105+
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
106+
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Ico a c) b :=
107+
have hIcc : ContinuousOn f (Icc a b) := Ioo_union_both g₀ ▸
108+
hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
109+
have hIco : ContinuousOn f (Ico b c) := Ioo_union_left g₁ ▸
110+
hd₁.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
111+
isMaxOn_of_mono_anti_Ico g₀ g₁
112+
(monotoneOn_of_deriv_nonneg (convex_Icc a b) hIcc (by simp_all) (by simp_all))
74113
(antitoneOn_of_deriv_nonpos (convex_Ico b c) hIco (by simp_all) (by simp_all))
75114

76115
/-- The First-Derivative Test from calculus, maxima version.
@@ -95,9 +134,9 @@ lemma isMinOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁
95134
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
96135
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsMinOn f (Ioo a c) b :=
97136
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)
137+
hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
99138
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)
139+
hd₁.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
101140
isMinOn_of_anti_mono_Ioo g₀ g₁
102141
(antitoneOn_of_deriv_nonpos (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
103142
(monotoneOn_of_deriv_nonneg (convex_Ico b c) hIco (by simp_all) (by simp_all))

0 commit comments

Comments
 (0)