Skip to content

Commit e23dee2

Browse files
CoolRmalCoolRmal
committed
change name
1 parent ebef846 commit e23dee2

1 file changed

Lines changed: 20 additions & 20 deletions

File tree

‎Mathlib/Analysis/Calculus/DerivativeTest.lean‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ private lemma continuousOn_Ici {f : ℝ → ℝ} {a : ℝ} (h : ContinuousAt f a
9191

9292
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `(a, b)` and
9393
nonpositive on `(b, c)`. Then `f` attains its maximum on `(a, c)` at `b`. -/
94-
lemma isMaxOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b)
94+
lemma isMaxOn_Ioo_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b)
9595
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
9696
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
9797
IsMaxOn f (Ioo a c) b := by
@@ -101,7 +101,7 @@ lemma isMaxOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b
101101

102102
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonnegative on
103103
`(a, b)` and nonpositive on `(b, c)`. Then `f` attains its maximum on `(a, c]` at `b`. -/
104-
lemma isMaxOn_of_deriv_Ioc {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
104+
lemma isMaxOn_Ioc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
105105
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
106106
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
107107
IsMaxOn f (Ioc a c) b := by
@@ -111,7 +111,7 @@ lemma isMaxOn_of_deriv_Ioc {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f
111111

112112
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonnegative on
113113
`(a, b)` and nonpositive on `(b, c)`. Then `f` attains its maximum on `[a, c)` at `b`. -/
114-
lemma isMaxOn_of_deriv_Ico {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
114+
lemma isMaxOn_Ico_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
115115
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
116116
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
117117
IsMaxOn f (Ico a c) b := by
@@ -121,7 +121,7 @@ lemma isMaxOn_of_deriv_Ico {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
121121

122122
/-- Suppose `f : ℝ → ℝ` is continuous at `a`, `b`, and `c`, the derivative `f'` is nonnegative on
123123
`(a, b)` and nonpositive on `(b, c)`. Then `f` attains its maximum on `[a, c]` at `b`. -/
124-
lemma isMaxOn_of_deriv_Icc {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
124+
lemma isMaxOn_Icc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
125125
(hc : ContinuousAt f c) (hd₀ : DifferentiableOn ℝ f (Ioo a b))
126126
(hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
127127
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsMaxOn f (Icc a c) b := by
@@ -131,7 +131,7 @@ lemma isMaxOn_of_deriv_Icc {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
131131

132132
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `(a, b)` and
133133
nonpositive on `(b, ∞)`. Then `f` attains its maximum on `(a, ∞)` at `b`. -/
134-
lemma isMaxOn_of_deriv_Ioi {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
134+
lemma isMaxOn_Ioi_of_deriv {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
135135
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
136136
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0) :
137137
IsMaxOn f (Ioi a) b := by
@@ -141,7 +141,7 @@ lemma isMaxOn_of_deriv_Ioi {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
141141

142142
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonnegative on
143143
`(a, b)` and nonpositive on `(b, ∞)`. Then `f` attains its maximum on `[a, ∞)` at `b`. -/
144-
lemma isMaxOn_of_deriv_Ici {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
144+
lemma isMaxOn_Ici_of_deriv {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
145145
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
146146
(h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0) :
147147
IsMaxOn f (Ici a) b := by
@@ -151,7 +151,7 @@ lemma isMaxOn_of_deriv_Ici {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a)
151151

152152
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `(-∞, b)` and
153153
nonpositive on `(b, c)`. Then `f` attains its maximum on `(-∞, c)` at `b`. -/
154-
lemma isMaxOn_of_deriv_Iio {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
154+
lemma isMaxOn_Iio_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
155155
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
156156
(h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
157157
IsMaxOn f (Iio c) b := by
@@ -161,7 +161,7 @@ lemma isMaxOn_of_deriv_Iio {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
161161

162162
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonnegative on
163163
`(-∞, b)` and nonpositive on `(b, c)`. Then `f` attains its maximum on `(-∞, c]` at `b`. -/
164-
lemma isMaxOn_of_deriv_Iic {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
164+
lemma isMaxOn_Iic_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
165165
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
166166
(h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) :
167167
IsMaxOn f (Iic c) b := by
@@ -171,7 +171,7 @@ lemma isMaxOn_of_deriv_Iic {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
171171

172172
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `(-∞, b)` and
173173
nonpositive on `(b, ∞)`. Then `f` attains its maximum on `ℝ` at `b`. -/
174-
lemma isMaxOn_of_deriv_univ {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b)
174+
lemma isMaxOn_univ_of_deriv {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b)
175175
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
176176
(h₀ : ∀ x ∈ Iio b, 0 ≤ deriv f x) (h₁ : ∀ x ∈ Ioi b, deriv f x ≤ 0) :
177177
IsMaxOn f univ b :=
@@ -188,11 +188,11 @@ lemma isLocalMax_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g
188188
(h : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Ioo a b))
189189
(hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
190190
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsLocalMax f b :=
191-
(isMaxOn_of_deriv_Ioo h hd₀ hd₁ h₀ h₁).isLocalMax (Ioo_mem_nhds g₀ g₁)
191+
(isMaxOn_Ioo_of_deriv h hd₀ hd₁ h₀ h₁).isLocalMax (Ioo_mem_nhds g₀ g₁)
192192

193193
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `(a, b)` and
194194
nonnegative on `(b, c)`. Then `f` attains its minimum on `(a, c)` at `b`. -/
195-
lemma isMinOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b)
195+
lemma isMinOn_Ioo_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b)
196196
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
197197
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
198198
IsMinOn f (Ioo a c) b := by
@@ -202,7 +202,7 @@ lemma isMinOn_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (h : ContinuousAt f b
202202

203203
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonpositive on
204204
`(a, b)` and nonnegative on `(b, c)`. Then `f` attains its minimum on `(a, c]` at `b`. -/
205-
lemma isMinOn_of_deriv_Ioc {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
205+
lemma isMinOn_Ioc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
206206
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
207207
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
208208
IsMinOn f (Ioc a c) b := by
@@ -212,7 +212,7 @@ lemma isMinOn_of_deriv_Ioc {f : ℝ → ℝ} {a b c : ℝ} (hb : ContinuousAt f
212212

213213
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonpositive on
214214
`(a, b)` and nonnegative on `(b, c)`. Then `f` attains its minimum on `[a, c)` at `b`. -/
215-
lemma isMinOn_of_deriv_Ico {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
215+
lemma isMinOn_Ico_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
216216
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
217217
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
218218
IsMinOn f (Ico a c) b := by
@@ -222,7 +222,7 @@ lemma isMinOn_of_deriv_Ico {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
222222

223223
/-- Suppose `f : ℝ → ℝ` is continuous at `a`, `b`, and `c`, the derivative `f'` is nonpositive on
224224
`(a, b)` and nonnegative on `(b, c)`. Then `f` attains its minimum on `[a, c]` at `b`. -/
225-
lemma isMinOn_of_deriv_Icc {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
225+
lemma isMinOn_Icc_of_deriv {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
226226
(hc : ContinuousAt f c) (hd₀ : DifferentiableOn ℝ f (Ioo a b))
227227
(hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
228228
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsMinOn f (Icc a c) b := by
@@ -232,7 +232,7 @@ lemma isMinOn_of_deriv_Icc {f : ℝ → ℝ} {a b c : ℝ} (ha : ContinuousAt f
232232

233233
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `(a, b)` and
234234
nonnegative on `(b, ∞)`. Then `f` attains its minimum on `(a, ∞)` at `b`. -/
235-
lemma isMinOn_of_deriv_Ioi {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
235+
lemma isMinOn_Ioi_of_deriv {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
236236
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
237237
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x) :
238238
IsMinOn f (Ioi a) b := by
@@ -242,7 +242,7 @@ lemma isMinOn_of_deriv_Ioi {f : ℝ → ℝ} {a b : ℝ} (hb : ContinuousAt f b)
242242

243243
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonpositive on
244244
`(a, b)` and nonnegative on `(b, ∞)`. Then `f` attains its minimum on `[a, ∞)` at `b`. -/
245-
lemma isMinOn_of_deriv_Ici {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
245+
lemma isMinOn_Ici_of_deriv {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a) (hb : ContinuousAt f b)
246246
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
247247
(h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x) :
248248
IsMinOn f (Ici a) b := by
@@ -252,7 +252,7 @@ lemma isMinOn_of_deriv_Ici {f : ℝ → ℝ} {a b : ℝ} (ha : ContinuousAt f a)
252252

253253
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `(-∞, b)` and
254254
nonnegative on `(b, c)`. Then `f` attains its minimum on `(-∞, c)` at `b`. -/
255-
lemma isMinOn_of_deriv_Iio {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
255+
lemma isMinOn_Iio_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
256256
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
257257
(h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
258258
IsMinOn f (Iio c) b := by
@@ -262,7 +262,7 @@ lemma isMinOn_of_deriv_Iio {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
262262

263263
/-- Suppose `f : ℝ → ℝ` is continuous at `b` and `c`, the derivative `f'` is nonpositive on
264264
`(-∞, b)` and nonnegative on `(b, c)`. Then `f` attains its minimum on `(-∞, c]` at `b`. -/
265-
lemma isMinOn_of_deriv_Iic {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
265+
lemma isMinOn_Iic_of_deriv {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b) (hc : ContinuousAt f c)
266266
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c))
267267
(h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) :
268268
IsMinOn f (Iic c) b := by
@@ -272,7 +272,7 @@ lemma isMinOn_of_deriv_Iic {f : ℝ → ℝ} {b c : ℝ} (hb : ContinuousAt f b)
272272

273273
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `(-∞, b)` and
274274
nonnegative on `(b, ∞)`. Then `f` attains its minimum on `ℝ` at `b`. -/
275-
lemma isMinOn_of_deriv_univ {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b)
275+
lemma isMinOn_univ_of_deriv {f : ℝ → ℝ} {b : ℝ} (hb : ContinuousAt f b)
276276
(hd₀ : DifferentiableOn ℝ f (Iio b)) (hd₁ : DifferentiableOn ℝ f (Ioi b))
277277
(h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0) (h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x) :
278278
IsMinOn f univ b := by
@@ -286,7 +286,7 @@ lemma isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g
286286
(h : ContinuousAt f b) (hd₀ : DifferentiableOn ℝ f (Ioo a b))
287287
(hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
288288
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b :=
289-
(isMinOn_of_deriv_Ioo h hd₀ hd₁ h₀ h₁).isLocalMin (Ioo_mem_nhds g₀ g₁)
289+
(isMinOn_Ioo_of_deriv h hd₀ hd₁ h₀ h₁).isLocalMin (Ioo_mem_nhds g₀ g₁)
290290

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

0 commit comments

Comments
 (0)