Theorems · Theorem · measure theory

exists_eq_interval_average

∀ {f : ℝ → ℝ} {a b : ℝ}, a ≠ b → ContinuousOn f (Set.uIcc a b) → ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in a..b, f x

The mean value theorem for integrals: There exists a point in an interval such that the mean of a continuous function over the interval equals the value of the function at the point.

Defined in

Mathlib.MeasureTheory.Integral.IntervalAverage

Cited by

0 results in Mathlib

Foundations

Depth 261 from the axioms · uses propext, Classical.choice, Quot.sound