First and second mean value theorems for interval integrals

We prove versions of the first and second mean value theorems for interval integrals.

Main results

First mean value theorem

• 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 ∂μ).

Second mean value theorem

• exists_eq_const_mul_intervalIntegral_of_nonneg_of_antitoneOn For nonnegative and nonincreasing f : ℝ → ℝ and integrable g : ℝ → ℝ on Icc a b: ∃ ξ ∈ Icc a b, ∫ x in a..b, f x * g x = f a * ∫ x in a..ξ, g x
• exists_eq_const_mul_intervalIntegral_of_nonneg_of_monotoneOn (nondecreasing variant)

A vector-valued inequality variant of the second mean value theorem

• exists_le_const_mul_norm_intervalIntegral_of_nonneg_of_antitoneOn Let E be a real Banach space. For nonnegative and nonincreasing f : ℝ → ℝ and integrable g : ℝ → E on Icc a b: ∃ ξ ∈ Icc a b, ‖∫ x in a..b, f x • g x‖ ≤ f a * ‖∫ x in a..ξ, g x‖
• exists_le_const_mul_norm_intervalIntegral_of_nonneg_of_monotoneOn (nondecreasing variant)

References

• V. A. Zorich, Mathematical Analysis I, Thm. 5 (First mean-value theorem for the integral).
• https://proofwiki.org/wiki/Mean_Value_Theorem_for_Integrals/Generalization
• E. T. Whittaker, G. N. Watson, A Course of Modern Analysis, 5th edition p. 63

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 ∂μ).

theorem exists_eq_const_mul_intervalIntegral_of_nonneg_of_antitoneOn {a b : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : 0 ≤ f b) (hf_mon : AntitoneOn f (Set.Icc a b)) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ∃ ξ ∈ Set.Icc a b, ∫ (x : ℝ) in a..b, f x * g x = f a * ∫ (x : ℝ) in a..ξ, g x

Second mean value theorem for interval integrals with a nonnegative antitone weight.

theorem exists_eq_const_mul_intervalIntegral_of_nonneg_of_monotoneOn {a b : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hf : 0 ≤ f a) (hf_mon : MonotoneOn f (Set.Icc a b)) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ∃ ξ ∈ Set.Icc a b, ∫ (x : ℝ) in a..b, f x * g x = f b * ∫ (x : ℝ) in ξ..b, g x

Second mean value theorem for interval integrals with a nonnegative monotone weight.

theorem exists_le_const_mul_norm_intervalIntegral_of_nonneg_of_antitoneOn {a b : ℝ} {f : ℝ → ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} (hab : a ≤ b) (hf : 0 ≤ f b) (hf_mon : AntitoneOn f (Set.Icc a b)) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ∃ ξ ∈ Set.Icc a b, ‖∫ (x : ℝ) in a..b, f x • g x‖ ≤ f a * ‖∫ (x : ℝ) in a..ξ, g x‖

An inequality version of the second mean value theorem for interval integrals for vector-valued functions with a nonnegative antitone weight.

theorem exists_le_const_mul_norm_intervalIntegral_of_nonneg_of_monotoneOn {a b : ℝ} {f : ℝ → ℝ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : ℝ → E} (hab : a ≤ b) (hf : 0 ≤ f a) (hf_mon : MonotoneOn f (Set.Icc a b)) (hg : IntervalIntegrable g MeasureTheory.volume a b) : ∃ ξ ∈ Set.Icc a b, ‖∫ (x : ℝ) in a..b, f x • g x‖ ≤ f b * ‖∫ (x : ℝ) in ξ..b, g x‖

An inequality version of the second mean value theorem for interval integrals for vector-valued functions with a nonnegative monotone weight. Monotone variant of exists_le_const_mul_norm_intervalIntegral_of_nonneg_of_antitoneOn.