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:

• interval_average_eq: ⨍ x in a..b, f x = (b - a)⁻¹ • ∫ x in a..b, f x;
• interval_average_eq_div: ⨍ x in a..b, f x = (∫ x in a..b, f x) / (b - a);
• exists_eq_interval_average_of_measure: ∃ c ∈ Ι a b, f c = ⨍ x in Ι a b, f x ∂μ.
• exists_eq_interval_average_of_nullSingletonClass: ∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ.
• exists_eq_interval_average: ∃ c ∈ uIoo a b, f c = ⨍ x in a..b, f x.

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.

def «term⨍_In_.._,_» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

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_of_measure {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hμfin : μ (Set.uIoc a b) ≠ ⊤) (hμ0 : μ (Set.uIoc a b) ≠ 0) : ∃ c ∈ Set.uIoc a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ

If f : ℝ → ℝ is continuous on uIcc a b, the interval has finite and nonzero μ-measure, then ∃ c ∈ Ι a b, f c = ⨍ x in Ι a b, f x ∂μ.

theorem exists_eq_interval_average_of_nullSingletonClass {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] (hf : ContinuousOn f (Set.uIcc a b)) (hμfin : μ (Set.uIoc a b) ≠ ⊤) (hμ0 : μ (Set.uIoc a b) ≠ 0) : ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ

If f : ℝ → ℝ is continuous on uIcc a b, the interval has finite and nonzero μ-measure, and μ has value zero on singletons, then ∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ.

@[deprecated exists_eq_interval_average_of_nullSingletonClass (since := "2026-06-09")]

theorem exists_eq_interval_average_of_noAtoms {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] (hf : ContinuousOn f (Set.uIcc a b)) (hμfin : μ (Set.uIoc a b) ≠ ⊤) (hμ0 : μ (Set.uIoc a b) ≠ 0) : ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ

Alias of exists_eq_interval_average_of_nullSingletonClass.

---

If f : ℝ → ℝ is continuous on uIcc a b, the interval has finite and nonzero μ-measure, and μ has value zero on singletons, then ∃ c ∈ uIoo a b, f c = ⨍ x in Ι a b, f x ∂μ.

theorem exists_eq_interval_average {f : ℝ → ℝ} {a b : ℝ} (hab : a ≠ b) (hf : 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.