exists_ratio_deriv_eq_ratio_slope

English

Under the MVT assumptions, there exists c ∈ (a,b) with (g b − g a) f'(c) = (f b − f a) g'(c) where f′ and g′ denote derivatives of f and g respectively.

Русский

При условиях MVT существует c ∈ (a,b), такое что (g(b)−g(a)) f′(c) = (f(b)−f(a)) g′(c).

LaTeX

$$$\\exists c\\in I^{o}_{a,b}, (g(b)-g(a))\\, f'(c) = (f(b)-f(a))\\, g'(c)$$$

Lean4

/-- Cauchy's Mean Value Theorem, `deriv` version. -/
theorem exists_ratio_deriv_eq_ratio_slope : ∃ c ∈ Ioo a b, (g b - g a) * deriv f c = (f b - f a) * deriv g c :=
  exists_ratio_hasDerivAt_eq_ratio_slope f (deriv f) hab hfc
    (fun x hx => ((hfd x hx).differentiableAt <| IsOpen.mem_nhds isOpen_Ioo hx).hasDerivAt) g (deriv g) hgc fun x hx =>
    ((hgd x hx).differentiableAt <| IsOpen.mem_nhds isOpen_Ioo hx).hasDerivAt

Похожие утверждения