Mean_Value_Theorem
Provedanalysiscalculusmean-value-theoremproofwiki
If f is continuous on [a,b] and differentiable on (a,b), then there exists xi in (a,b) with f'(xi) = (f(b)-f(a))/(b-a).
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue theorem Mean_Value_Theorem (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x) : ∃ ξ ∈ Set.Ioo a b, deriv f ξ = (f b - f a) / (b - a) := by sorry
Source