English
Let x<y and f be continuous on [x,y], strictly monotone on (x,y) via deriv, then there exists a in (x,y) with a slope condition related to the derivative.
Русский
Пусть x<y, f непрерывна на [x,y], и производная монотонна на (x,y); тогда существует a в (x,y) с определённым условием касательной/угла.
LaTeX
$$$$\\exists a\\in(x,y): \\text{(slope condition related to deriv f(a))}.$$$$
Lean4
theorem exists_slope_lt_deriv_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, (f y - f x) / (y - x) < deriv f a :=
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 hay with ⟨b, ⟨hab, hby⟩⟩
refine ⟨b, ⟨hxa.trans hab, hby⟩, ?_⟩
rw [← ha]
exact hf'_mono ⟨hxa, hay⟩ ⟨hxa.trans hab, hby⟩ hab
