Documentation

Mathlib.MeasureTheory.Integral.IntervalAverage

Integral average over an interval #

In this file we introduce notation ⨍ x in a..b, f x for the average ⨍ x in Ι a b, f x of f over the interval Ι a b = Set.Ioc (min a b) (max a b) w.r.t. the Lebesgue measure, then prove formulas for this average:

We also prove that ⨍ x in a..b, f x = ⨍ x in b..a, f x, see interval_average_symm.

Notation #

⨍ x in a..b, f x: average of f over the interval Ι a b w.r.t. the Lebesgue measure.

⨍ x in a..b, f x is the average of f over the interval `Ι a w.r.t. the Lebesgue measure.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem interval_average_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (a b : ) :
    (x : ) in a..b, f x = (x : ) in b..a, f x
    theorem interval_average_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (a b : ) :
    (x : ) in a..b, f x = (b - a)⁻¹ (x : ) in a..b, f x
    theorem interval_average_eq_div (f : ) (a b : ) :
    (x : ) in a..b, f x = ( (x : ) in a..b, f x) / (b - a)
    theorem intervalAverage_congr_codiscreteWithin {a b : } {f₁ f₂ : } (hf : f₁ =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] f₂) :
    (x : ) in a..b, f₁ x = (x : ) in a..b, f₂ x

    Interval averages are invariant when functions change along discrete sets.

    theorem exists_eq_interval_average {f : } {a b : } (hab : a b) (hf : ContinuousOn f (Set.uIcc a b)) :
    cSet.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.