English
There exists a in (x,y) with deriv f(a) less than the secant slope (f(y)−f(x))/(y−x).
Русский
Существует a ∈ (x,y) такое, что deriv f(a) меньше секантного наклона (f(y)−f(x))/(y−x).
LaTeX
$$$$\\exists a\\in Ioo(x,y): deriv f(a) < \\frac{f(y)-f(x)}{y-x}. $$$$
Lean4
theorem exists_deriv_lt_slope {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Icc x y)) (hxy : x < y)
(hf'_mono : StrictMonoOn (deriv f) (Ioo x y)) : ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x) :=
by
by_cases h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
· apply StrictMonoOn.exists_deriv_lt_slope_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, deriv f a < (f w - f x) / (w - x) :=
by
apply StrictMonoOn.exists_deriv_lt_slope_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, deriv f b < (f y - f w) / (y - w) :=
by
apply StrictMonoOn.exists_deriv_lt_slope_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 ⟨a, ⟨hxa, haw.trans hwy⟩, ?_⟩
simp only [lt_div_iff₀, hxy, hxw, hwy, sub_pos] at ha hb ⊢
have : deriv f a * (y - w) < deriv f b * (y - w) :=
by
apply mul_lt_mul _ le_rfl (sub_pos.2 hwy) _
· 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
