English
Let f be differentiable on Ioo(a,b) and g differentiable on Ioo(a,b). There exists c ∈ Ioo(a,b) with (lgb-lga) f'(c) = (lfb-lfa) g'(c) for corresponding limit values lfa,lga,lfb,lgb.
Русский
Пусть f и g дифференцируемы на (a,b). Существует c ∈ (a,b) такое, что (lgb−lga) f'(c) = (lfb−lfa) g'(c).
LaTeX
$$$\\exists c\\in I^{oo}_{a,b}, (lgb-lga) f'(c) = (lfb-lfa) g'(c)$$$
Lean4
/-- Cauchy's Mean Value Theorem, extended `deriv` version. -/
theorem exists_ratio_deriv_eq_ratio_slope' {lfa lga lfb lgb : ℝ} (hdf : DifferentiableOn ℝ f <| Ioo a b)
(hdg : DifferentiableOn ℝ g <| Ioo a b) (hfa : Tendsto f (𝓝[>] a) (𝓝 lfa)) (hga : Tendsto g (𝓝[>] a) (𝓝 lga))
(hfb : Tendsto f (𝓝[<] b) (𝓝 lfb)) (hgb : Tendsto g (𝓝[<] b) (𝓝 lgb)) :
∃ c ∈ Ioo a b, (lgb - lga) * deriv f c = (lfb - lfa) * deriv g c :=
exists_ratio_hasDerivAt_eq_ratio_slope' _ _ hab _ _
(fun x hx => ((hdf x hx).differentiableAt <| Ioo_mem_nhds hx.1 hx.2).hasDerivAt)
(fun x hx => ((hdg x hx).differentiableAt <| Ioo_mem_nhds hx.1 hx.2).hasDerivAt) hfa hga hfb hgb
