English
Under analogous conditions, there exists b ∈ (y,z) with a similar slope-derivative relation; this is an auxiliary step in convexity proofs from derivative information.
Русский
При аналогичных условиях существует b ∈ (y,z) с аналогичным отношением наклона к производной; это вспомогательный шаг в доказательствах выпуклости через производную.
LaTeX
$$$$\\exists b\\in Ioo(y,z): \\frac{f(z)-f(y)}{z-y} < f'(b). $$$$
Lean4
theorem exists_deriv_lt_slope_aux {x y : ℝ} {f : ℝ → ℝ} (hf : ContinuousOn f (Icc x y)) (hxy : x < y)
(hf'_mono : StrictMonoOn (deriv f) (Ioo x y)) (h : ∀ w ∈ Ioo x y, deriv f w ≠ 0) :
∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x) :=
by
have A : DifferentiableOn ℝ f (Ioo x y) := fun w wmem =>
(differentiableAt_of_deriv_ne_zero (h w wmem)).differentiableWithinAt
obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) := exists_deriv_eq_slope f hxy hf A
rcases nonempty_Ioo.2 hxa with ⟨b, ⟨hxb, hba⟩⟩
refine ⟨b, ⟨hxb, hba.trans hay⟩, ?_⟩
rw [← ha]
exact hf'_mono ⟨hxb, hba.trans hay⟩ ⟨hxa, hay⟩ hba
