Theorems · Theorem · real analysis

exists_eq_const_mul_intervalIntegral_of_ae_nonneg

∀ {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  ContinuousOn f (Set.uIcc a b) →
    IntervalIntegrable g μ a b →
      (∀ᵐ (x : ℝ) ∂μ.restrict (Set.uIoc a b), 0 ≤ g x) →
        ∃ c ∈ Set.uIcc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

First mean value theorem for interval integrals (arbitrary measure, a.e. nonnegativity). Let f g : ℝ → ℝ and let μ be a measure on ℝ. Assume that f is continuous on uIcc a b, that g is interval integrable on a..b w.r.t. μ, and that g ≥ 0 a.e. on Ι a b w.r.t. μ.restrict (Ι a b). Then ∃ c ∈ uIcc a b, (∫ x in a..b, f x * g x ∂μ) = f c * (∫ x in a..b, g x ∂μ).

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue

Cited by

1 results in Mathlib

Foundations

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