English
Under the hypotheses of the classical MVT, extended to HasDerivAt form, there exists c ∈ (a,b) with (lgb−lga) f'(c) = (lfb−lfa) g'(c).
Русский
При указанных условиях теоремы о среднем значении с формой производной существует 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 `HasDerivAt` version. -/
theorem exists_ratio_hasDerivAt_eq_ratio_slope' {lfa lga lfb lgb : ℝ} (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
(hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) (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) * f' c = (lfb - lfa) * g' c :=
by
let h x := (lgb - lga) * f x - (lfb - lfa) * g x
have hha : Tendsto h (𝓝[>] a) (𝓝 <| lgb * lfa - lfb * lga) :=
by
have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
(tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
convert this using 2
ring
have hhb : Tendsto h (𝓝[<] b) (𝓝 <| lgb * lfa - lfb * lga) :=
by
have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
(tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
convert this using 2
ring
let h' x := (lgb - lga) * f' x - (lfb - lfa) * g' x
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
intro x hx
exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)
rcases exists_hasDerivAt_eq_zero' hab hha hhb hhh' with ⟨c, cmem, hc⟩
exact ⟨c, cmem, sub_eq_zero.1 hc⟩
