English
There exists a point a ∈ (x,y) such that deriv f(a) is greater than the secant slope (f(y)−f(x))/(y−x) for real-valued f on [x,y] with appropriate monotonicity assumptions.
Русский
Существует точка a ∈ (x,y), такая что производная f(a) превышает секантский наклон (f(y)−f(x))/(y−x) при заданных условиях монотонности производной.
LaTeX
$$$$\\exists a\\in Ioo(x,y): \\frac{f(y)-f(x)}{y-x} < f'(a). $$$$
Lean4
theorem exists_slope_lt_deriv {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Icc x y)) (hxy : x < y)
(hf'_mono : StrictMonoOn (deriv f) (Ioo x y)) : ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a :=
by
by_cases h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
· apply StrictMonoOn.exists_slope_lt_deriv_aux hf hxy hf'_mono h
· push_neg at h
rcases h with ⟨w, ⟨hxw, hwy⟩, hw⟩
obtain ⟨a, ⟨hxa, haw⟩, ha⟩ : ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a :=
by
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
· exact hf.mono (Icc_subset_Icc le_rfl hwy.le)
· exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)
· intro z hz
rw [← hw]
apply ne_of_lt
exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2
obtain ⟨b, ⟨hwb, hby⟩, hb⟩ : ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b :=
by
apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _
· refine hf.mono (Icc_subset_Icc hxw.le le_rfl)
· exact hf'_mono.mono (Ioo_subset_Ioo hxw.le le_rfl)
· intro z hz
rw [← hw]
apply ne_of_gt
exact hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hz.1, hz.2⟩ hz.1
refine ⟨b, ⟨hxw.trans hwb, hby⟩, ?_⟩
simp only [div_lt_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢
have : deriv f a * (w - x) < deriv f b * (w - x) :=
by
apply mul_lt_mul _ le_rfl (sub_pos.2 hxw) _
· exact hf'_mono ⟨hxa, haw.trans hwy⟩ ⟨hxw.trans hwb, hby⟩ (haw.trans hwb)
· rw [← hw]
exact (hf'_mono ⟨hxw, hwy⟩ ⟨hxw.trans hwb, hby⟩ hwb).le
linarith
