Theorems · Theorem · measure theory

exists_eq_interval_average_of_nullSingletonClass

∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  ContinuousOn f (Set.uIcc a b) →
    μ (Set.uIoc a b) ≠ ⊤ → μ (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 ∂μ.

Defined in

Mathlib.MeasureTheory.Integral.IntervalAverage

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.NullSingletonClass