English
Let f, g be functions on [a,b] with appropriate continuity and differentiability as in the hypotheses. Then there exists c ∈ (a,b) such that (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 (a,b), (g(b)-g(a))\\, f'(c) = (f(b)-f(a))\\, g'(c)$$$
Lean4
/-- Cauchy's **Mean Value Theorem**, `HasDerivAt` version. -/
theorem exists_ratio_hasDerivAt_eq_ratio_slope : ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c :=
by
let h x := (g b - g a) * f x - (f b - f a) * g x
have hI : h a = h b := by simp only [h]; ring
let h' x := (g b - g a) * f' x - (f b - f a) * g' x
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := fun x hx =>
((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
have hhc : ContinuousOn h (Icc a b) := (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
rcases exists_hasDerivAt_eq_zero hab hhc hI hhh' with ⟨c, cmem, hc⟩
exact ⟨c, cmem, sub_eq_zero.1 hc⟩
