First mean value theorem for interval integrals

We prove versions of the first mean value theorem for interval integrals.

Main results

• exists_eq_const_mul_intervalIntegral_of_ae_nonneg (a.e. nonnegativity of g on s): ∃ c ∈ uIcc a b, (∫ x in a..b, f x * g x ∂μ) = f c * (∫ x in a..b, g x ∂μ).
• exists_eq_const_mul_intervalIntegral_of_nonneg (pointwise nonnegativity of g on s): ∃ c ∈ uIcc a b, (∫ x in a..b, f x * g x ∂μ) = f c * (∫ x in a..b, g x ∂μ).

References

• [V. A. Zorich, Mathematical Analysis I][zorich2016], Thm. 5 (First mean-value theorem for the integral).
• https://proofwiki.org/wiki/Mean_Value_Theorem_for_Integrals/Generalization

Tags

mean value theorem, interval integral

theorem exists_eq_const_mul_intervalIntegral_of_ae_nonneg {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hg : IntervalIntegrable g μ a b) (hg0 : ∀ᵐ (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 ∂μ).

theorem exists_eq_const_mul_intervalIntegral_of_nonneg {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hg : IntervalIntegrable g μ a b) (hg0 : ∀ 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 ∂μ).