Cauchy_Mean_Value_Theorem

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysiscalculusmean-value-theoremproofwiki

Let f, g be continuous on [a,b] and differentiable on (a,b). Then there exists xi in (a,b) with (f(b)-f(a))*g'(xi) = (g(b)-g(a))*f'(xi).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.MeanValue

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.MeanValue

theorem Cauchy_Mean_Value_Theorem (f g : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hgc : ContinuousOn g (Set.Icc a b)) (hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x) (hgd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ g x) : ∃ ξ ∈ Set.Ioo a b, (f b - f a) * deriv g ξ = (g b - g a) * deriv f ξ := by sorry

Source

https://proofwiki.org/wiki/Cauchy_Mean_Value_Theorem

View graph