First mean value theorem for set integrals

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

Main results

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

Tags

first mean value theorem, set integral

theorem exists_eq_const_mul_setIntegral_of_ae_nonneg {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {s : Set α} {f g : α → ℝ} {μ : MeasureTheory.Measure α} (hs_conn : IsConnected s) (hs_meas : MeasurableSet s) (hf : ContinuousOn f s) (hg : MeasureTheory.IntegrableOn g s μ) (hfg : MeasureTheory.IntegrableOn (fun (x : α) => f x * g x) s μ) (hg0 : ∀ᵐ (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 ∂μ).

theorem exists_eq_const_mul_setIntegral_of_nonneg {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {s : Set α} {f g : α → ℝ} {μ : MeasureTheory.Measure α} (hs_conn : IsConnected s) (hs_meas : MeasurableSet s) (hf : ContinuousOn f s) (hg : MeasureTheory.IntegrableOn g s μ) (hfg : MeasureTheory.IntegrableOn (fun (x : α) => f x * g x) s μ) (hg0 : ∀ x ∈ 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 (pointwise 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 on s, then ∃ c ∈ s, (∫ x in s, f x * g x ∂μ) = f c * (∫ x in s, g x ∂μ)