Theorems · Theorem · real analysis

exists_eq_const_mul_intervalIntegral_of_nonneg

∀ {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ},
  ContinuousOn f (Set.uIcc a b) →
    IntervalIntegrable g μ a b →
      (∀ x ∈ 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, 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 on Ι 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

0 results in Mathlib

Foundations

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