Theorems · Theorem · measure theory

exists_eq_const_mul_setIntegral_of_ae_nonneg

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {s : Set α} {f g : α → ℝ}
  {μ : MeasureTheory.Measure α},
  IsConnected s →
    MeasurableSet s →
      ContinuousOn f s →
        MeasureTheory.IntegrableOn g s μ →
          MeasureTheory.IntegrableOn (fun x => f x * g x) s μ →
            (∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x) → ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

First mean value theorem for set integrals (a.e. nonnegativity). Let s be a connected measurable set. If f is continuous on s, g is integrable on s, f * g is integrable on s, and g is nonnegative a.e. on s w.r.t. μ.restrict s, then ∃ c ∈ s, (∫ x in s, f x * g x ∂μ) = f c * (∫ x in s, g x ∂μ).

Defined in

Mathlib.MeasureTheory.Integral.MeanValue

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpace