English
If f and g are differentiable on (a,b) and continuous on [a,b], then there exists c ∈ (a,b) with (g(b)−g(a)) f′(c) = (f(b)−f(a)) g′(c).
Русский
Если f и g дифференцируемы на (a,b) и непрерывны на [a,b], существует c ∈ (a,b) такое, что (g(b)−g(a)) f′(c) = (f(b)−f(a)) g′(c).
LaTeX
$$$\\exists c\\in I^{oo}_{a,b}, (g(b)-g(a)) f'(c) = (f(b)-f(a)) g'(c)$$$
Lean4
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f' < C`, then
`f` grows slower than `C * x` on `D`, i.e., `f y - f x < C * (y - x)` whenever `x, y ∈ D`,
`x < y`. -/
theorem image_sub_lt_mul_sub_of_deriv_lt {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
(hf' : DifferentiableOn ℝ f (interior D)) {C} (lt_hf' : ∀ x ∈ interior D, deriv f x < C) (x : ℝ) (hx : x ∈ D)
(y : ℝ) (hy : y ∈ D) (hxy : x < y) : f y - f x < C * (y - x) :=
have hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x := fun x hx =>
by
rw [deriv.fun_neg, neg_lt_neg_iff]
exact lt_hf' x hx
by linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]
