Integral average of a function

In this file we define MeasureTheory.average μ f (notation: ⨍ x, f x ∂μ) to be the average value of f with respect to measure μ. It is defined as ∫ x, f x ∂((μ univ)⁻¹ • μ), so it is equal to zero if f is not integrable or if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, we use ⨍ x in s, f x ∂μ (notation for ⨍ x, f x ∂(μ.restrict s)). For average w.r.t. the volume, one can omit ∂volume.

Both have a version for the Lebesgue integral rather than Bochner.

We prove several versions of the first moment method: An integrable function is below/above its average on a set of positive measure:

• measure_le_setLAverage_pos for the Lebesgue integral
• measure_le_setAverage_pos for the Bochner integral

Implementation notes

The average is defined as an integral over (μ univ)⁻¹ • μ so that all theorems about Bochner integrals work for the average without modifications. For theorems that require integrability of a function, we provide a convenience lemma MeasureTheory.Integrable.to_average.

Tags

integral, center mass, average value, set average

Average value of a function w.r.t. a measure

The (Bochner, Lebesgue) average value of a function f w.r.t. a measure μ (notation: ⨍ x, f x ∂μ, ⨍⁻ x, f x ∂μ) is defined as the (Bochner, Lebesgue) integral divided by the total measure, so it is equal to zero if μ is an infinite measure, and (typically) equal to infinity if f is not integrable. If μ is a probability measure, then the average of any function is equal to its integral.

noncomputable def MeasureTheory.laverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) (f : α → ENNReal) : ENNReal

Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ, denoted ⨍⁻ x, f x ∂μ.

It is equal to (μ univ)⁻¹ * ∫⁻ x, f x ∂μ, so it takes value zero if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use ⨍⁻ x in s, f x ∂μ, defined as ⨍⁻ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

Equations

• MeasureTheory.laverage μ f = ∫⁻ (x : α), f x ∂(μ Set.univ)⁻¹ • μ

def MeasureTheory.«term⨍⁻_,_∂_» : Lean.ParserDescr

Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ.

It is equal to (μ univ)⁻¹ * ∫⁻ x, f x ∂μ, so it takes value zero if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use ⨍⁻ x in s, f x ∂μ, defined as ⨍⁻ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term⨍⁻_,_» : Lean.ParserDescr

Average value of an ℝ≥0∞-valued function f w.r.t. the standard measure.

It is equal to (volume univ)⁻¹ * ∫⁻ x, f x, so it takes value zero if the space has infinite measure. In a probability space, the average of any function is equal to its integral.

For the average on a set, use ⨍⁻ x in s, f x, defined as ⨍⁻ x, f x ∂(volume.restrict s).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term⨍⁻_In_,_∂_» : Lean.ParserDescr

Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ on a set s.

It is equal to (μ s)⁻¹ * ∫⁻ x, f x ∂μ, so it takes value zero if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

For the average w.r.t. the volume, one can omit ∂volume.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term⨍⁻_In_,_» : Lean.ParserDescr

Average value of an ℝ≥0∞-valued function f w.r.t. the standard measure on a set s.

It is equal to (volume s)⁻¹ * ∫⁻ x, f x, so it takes value zero if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.laverage_zero {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : ⨍⁻ (_x : α), 0 ∂μ = 0

@[simp]

theorem MeasureTheory.laverage_zero_measure {α : Type u_1} {m0 : MeasurableSpace α} (f : α → ENNReal) : ⨍⁻ (x : α), f x ∂0 = 0

theorem MeasureTheory.laverage_eq' {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) (f : α → ENNReal) : ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂(μ Set.univ)⁻¹ • μ

theorem MeasureTheory.laverage_eq {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) (f : α → ENNReal) : ⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ Set.univ

theorem MeasureTheory.laverage_eq_lintegral {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsProbabilityMeasure μ] (f : α → ENNReal) : ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

@[simp]

theorem MeasureTheory.measure_mul_laverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → ENNReal) : μ Set.univ * ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.setLAverage_eq {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) (f : α → ENNReal) (s : Set α) : ⨍⁻ (x : α) in s, f x ∂μ = (∫⁻ (x : α) in s, f x ∂μ) / μ s

theorem MeasureTheory.setLAverage_eq' {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) (f : α → ENNReal) (s : Set α) : ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s

theorem MeasureTheory.laverage_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (h : f =ᵐ[μ] g) : ⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ

theorem MeasureTheory.setLAverage_congr {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {f : α → ENNReal} (h : s =ᵐ[μ] t) : ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.setLAverage_congr_fun_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f g : α → ENNReal} (hs : MeasurableSet s) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) : ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ

theorem MeasureTheory.setLAverage_congr_fun {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f g : α → ENNReal} (hs : MeasurableSet s) (h : Set.EqOn f g s) : ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ

theorem MeasureTheory.laverage_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) : ⨍⁻ (x : α), f x ∂μ < ⊤

theorem MeasureTheory.setLAverage_lt_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ → ⨍⁻ (x : α) in s, f x ∂μ < ⊤

theorem MeasureTheory.laverage_add_measure {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} {f : α → ENNReal} : ⨍⁻ (x : α), f x ∂(μ + ν) = μ Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f x ∂μ + ν Set.univ / (μ Set.univ + ν Set.univ) * ⨍⁻ (x : α), f x ∂ν

theorem MeasureTheory.measure_mul_setLAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (f : α → ENNReal) (h : μ s ≠ ⊤) : μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

theorem MeasureTheory.laverage_union {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {f : α → ENNReal} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) : ⨍⁻ (x : α) in s ∪ t, f x ∂μ = μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f x ∂μ

theorem MeasureTheory.laverage_union_mem_openSegment {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {f : α → ENNReal} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hs₀ : μ s ≠ 0) (ht₀ : μ t ≠ 0) (hsμ : μ s ≠ ⊤) (htμ : μ t ≠ ⊤) : ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ENNReal (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)

theorem MeasureTheory.laverage_union_mem_segment {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s t : Set α} {f : α → ENNReal} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ⊤) (htμ : μ t ≠ ⊤) : ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ segment ENNReal (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)

theorem MeasureTheory.laverage_mem_openSegment_compl_self {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0) (hsc₀ : μ sᶜ ≠ 0) : ⨍⁻ (x : α), f x ∂μ ∈ openSegment ENNReal (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)

@[simp]

theorem MeasureTheory.laverage_const {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] [h : NeZero μ] (c : ENNReal) : ⨍⁻ (_x : α), c ∂μ = c

theorem MeasureTheory.setLAverage_const {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs₀ : μ s ≠ 0) (hs : μ s ≠ ⊤) (c : ENNReal) : ⨍⁻ (_x : α) in s, c ∂μ = c

theorem MeasureTheory.laverage_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] [NeZero μ] : ⨍⁻ (_x : α), 1 ∂μ = 1

theorem MeasureTheory.setLAverage_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} (hs₀ : μ s ≠ 0) (hs : μ s ≠ ⊤) : ⨍⁻ (_x : α) in s, 1 ∂μ = 1

@[simp]

theorem MeasureTheory.laverage_mul_measure_univ {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → ENNReal) : (⨍⁻ (a : α), f a ∂μ) * μ Set.univ = ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.lintegral_laverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → ENNReal) : ∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ

theorem MeasureTheory.setLIntegral_setLAverage {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → ENNReal) (s : Set α) : ∫⁻ (_x : α) in s, ⨍⁻ (a : α) in s, f a ∂μ ∂μ = ∫⁻ (x : α) in s, f x ∂μ

theorem MeasureTheory.laverage_mono_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (h : f ≤ᵐ[μ] g) : ⨍⁻ (a : α), f a ∂μ ≤ ⨍⁻ (a : α), g a ∂μ

theorem MeasureTheory.setLAverage_mono_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f g : α → ENNReal} (s : Set α) (h : f ≤ᵐ[μ] g) : ⨍⁻ (a : α) in s, f a ∂μ ≤ ⨍⁻ (a : α) in s, g a ∂μ

theorem MeasureTheory.setLAverage_le_essSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} (s : Set α) (f : α → ENNReal) : ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

theorem MeasureTheory.laverage_le_essSup {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} (f : α → ENNReal) : ⨍⁻ (x : α), f x ∂μ ≤ essSup f μ

noncomputable def MeasureTheory.average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) : E

Average value of a function f w.r.t. a measure μ, denoted ⨍ x, f x ∂μ.

It is equal to (μ.real univ)⁻¹ • ∫ x, f x ∂μ, so it takes value zero if f is not integrable or if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use ⨍ x in s, f x ∂μ, defined as ⨍ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

Equations

• MeasureTheory.average μ f = ∫ (x : α), f x ∂(μ Set.univ)⁻¹ • μ

def MeasureTheory.«term⨍_,_∂_» : Lean.ParserDescr

Average value of a function f w.r.t. a measure μ.

It is equal to (μ.real univ)⁻¹ • ∫ x, f x ∂μ, so it takes value zero if f is not integrable or if μ is an infinite measure. If μ is a probability measure, then the average of any function is equal to its integral.

For the average on a set, use ⨍ x in s, f x ∂μ, defined as ⨍ x, f x ∂(μ.restrict s). For the average w.r.t. the volume, one can omit ∂volume.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term⨍_,_» : Lean.ParserDescr

Average value of a function f w.r.t. the standard measure.

It is equal to (volume.real univ)⁻¹ * ∫ x, f x, so it takes value zero if f is not integrable or if the space has infinite measure. In a probability space, the average of any function is equal to its integral.

For the average on a set, use ⨍ x in s, f x, defined as ⨍ x, f x ∂(volume.restrict s).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term⨍_In_,_∂_» : Lean.ParserDescr

Average value of a function f w.r.t. a measure μ on a set s.

It is equal to (μ.real s)⁻¹ * ∫ x, f x ∂μ, so it takes value zero if f is not integrable on s or if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

For the average w.r.t. the volume, one can omit ∂volume.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term⨍_In_,_» : Lean.ParserDescr

Average value of a function f w.r.t. the standard measure on a set s.

It is equal to (volume.real s)⁻¹ * ∫ x, f x, so it takes value zero f is not integrable on s or if s has infinite measure. If s has measure 1, then the average of any function is equal to its integral.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasureTheory.average_zero {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) : ⨍ (x : α), 0 ∂μ = 0

@[simp]

theorem MeasureTheory.average_zero_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : α → E) : ⨍ (x : α), f x ∂0 = 0

@[simp]

theorem MeasureTheory.average_neg {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) : ⨍ (x : α), -f x ∂μ = -⨍ (x : α), f x ∂μ

theorem MeasureTheory.average_eq' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) : ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂(μ Set.univ)⁻¹ • μ

theorem MeasureTheory.average_eq {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) : ⨍ (x : α), f x ∂μ = (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ

theorem MeasureTheory.average_eq_integral {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) [IsProbabilityMeasure μ] (f : α → E) : ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

@[simp]

theorem MeasureTheory.measure_smul_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) : μ.real Set.univ • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

theorem MeasureTheory.setAverage_eq {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) (s : Set α) : ⨍ (x : α) in s, f x ∂μ = (μ.real s)⁻¹ • ∫ (x : α) in s, f x ∂μ

theorem MeasureTheory.setAverage_eq' {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure α) (f : α → E) (s : Set α) : ⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s

theorem MeasureTheory.average_congr {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f g : α → E} (h : f =ᵐ[μ] g) : ⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ

theorem MeasureTheory.setAverage_congr {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {s t : Set α} {f : α → E} (h : s =ᵐ[μ] t) : ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in t, f x ∂μ

theorem MeasureTheory.setAverage_congr_fun {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {s : Set α} {f g : α → E} (hs : MeasurableSet s) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) : ⨍ (x : α) in s, f x ∂μ = ⨍ (x : α) in s, g x ∂μ

theorem MeasureTheory.average_add_measure {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} [IsFiniteMeasure μ] {ν : Measure α} [IsFiniteMeasure ν] {f : α → E} (hμ : Integrable f μ) (hν : Integrable f ν) : ⨍ (x : α), f x ∂(μ + ν) = (μ.real Set.univ / (μ.real Set.univ + ν.real Set.univ)) • ⨍ (x : α), f x ∂μ + (ν.real Set.univ / (μ.real Set.univ + ν.real Set.univ)) • ⨍ (x : α), f x ∂ν

theorem MeasureTheory.average_pair {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {μ : Measure α} [CompleteSpace E] {f : α → E} {g : α → F} (hfi : Integrable f μ) (hgi : Integrable g μ) : ⨍ (x : α), (f x, g x) ∂μ = (⨍ (x : α), f x ∂μ, ⨍ (x : α), g x ∂μ)

theorem MeasureTheory.measure_smul_setAverage {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} (f : α → E) {s : Set α} (h : μ s ≠ ⊤) : μ.real s • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ

theorem MeasureTheory.average_union {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ⊤) (htμ : μ t ≠ ⊤) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) : ⨍ (x : α) in s ∪ t, f x ∂μ = (μ.real s / (μ.real s + μ.real t)) • ⨍ (x : α) in s, f x ∂μ + (μ.real t / (μ.real s + μ.real t)) • ⨍ (x : α) in t, f x ∂μ

theorem MeasureTheory.average_union_mem_openSegment {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hs₀ : μ s ≠ 0) (ht₀ : μ t ≠ 0) (hsμ : μ s ≠ ⊤) (htμ : μ t ≠ ⊤) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) : ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

theorem MeasureTheory.average_union_mem_segment {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) (hsμ : μ s ≠ ⊤) (htμ : μ t ≠ ⊤) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) : ⨍ (x : α) in s ∪ t, f x ∂μ ∈ segment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

theorem MeasureTheory.average_mem_openSegment_compl_self {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} [IsFiniteMeasure μ] {f : α → E} {s : Set α} (hs : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0) (hsc₀ : μ sᶜ ≠ 0) (hfi : Integrable f μ) : ⨍ (x : α), f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)

@[simp]

theorem MeasureTheory.average_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : Measure α) [IsFiniteMeasure μ] [h : NeZero μ] (c : E) : ⨍ (_x : α), c ∂μ = c

theorem MeasureTheory.setAverage_const {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} [CompleteSpace E] {s : Set α} (hs₀ : μ s ≠ 0) (hs : μ s ≠ ⊤) (c : E) : ⨍ (x : α) in s, c ∂μ = c

theorem MeasureTheory.integral_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) : ∫ (x : α), ⨍ (a : α), f a ∂μ ∂μ = ∫ (x : α), f x ∂μ

theorem MeasureTheory.setIntegral_setAverage {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) (s : Set α) : ∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ ∂μ = ∫ (x : α) in s, f x ∂μ

theorem MeasureTheory.integral_sub_average {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) : ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0

theorem MeasureTheory.setAverage_sub_setAverage {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {s : Set α} [CompleteSpace E] (hs : μ s ≠ ⊤) (f : α → E) : ∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ = 0

theorem MeasureTheory.integral_average_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f : α → E} [CompleteSpace E] [IsFiniteMeasure μ] (hf : Integrable f μ) : ∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ = 0

theorem MeasureTheory.setIntegral_setAverage_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {s : Set α} {f : α → E} [CompleteSpace E] (hs : μ s ≠ ⊤) (hf : IntegrableOn f s μ) : ∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ - f x ∂μ = 0

theorem MeasureTheory.ofReal_average {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : Integrable f μ) (hf₀ : 0 ≤ᵐ[μ] f) : ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ Set.univ

theorem MeasureTheory.ofReal_setAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ℝ} (hf : IntegrableOn f s μ) (hf₀ : 0 ≤ᵐ[μ.restrict s] f) : ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s

theorem MeasureTheory.toReal_laverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ

theorem MeasureTheory.toReal_setLAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} (hf : AEMeasurable f (μ.restrict s)) (hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤) : (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ

First moment method

theorem MeasureTheory.measure_le_setAverage_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ℝ} (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ⊤) (hf : IntegrableOn f s μ) : 0 < μ {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}

First moment method. An integrable function is smaller than its mean on a set of positive measure.

theorem MeasureTheory.measure_setAverage_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ℝ} (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ⊤) (hf : IntegrableOn f s μ) : 0 < μ {x : α | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x}

First moment method. An integrable function is greater than its mean on a set of positive measure.

theorem MeasureTheory.exists_le_setAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ℝ} (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ⊤) (hf : IntegrableOn f s μ) : ∃ x ∈ s, f x ≤ ⨍ (a : α) in s, f a ∂μ

First moment method. The minimum of an integrable function is smaller than its mean.

theorem MeasureTheory.exists_setAverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ℝ} (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ⊤) (hf : IntegrableOn f s μ) : ∃ x ∈ s, ⨍ (a : α) in s, f a ∂μ ≤ f x

First moment method. The maximum of an integrable function is greater than its mean.

theorem MeasureTheory.measure_le_average_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : Integrable f μ) : 0 < μ {x : α | f x ≤ ⨍ (a : α), f a ∂μ}

First moment method. An integrable function is smaller than its mean on a set of positive measure.

theorem MeasureTheory.measure_average_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : Integrable f μ) : 0 < μ {x : α | ⨍ (a : α), f a ∂μ ≤ f x}

First moment method. An integrable function is greater than its mean on a set of positive measure.

theorem MeasureTheory.exists_le_average {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : Integrable f μ) : ∃ (x : α), f x ≤ ⨍ (a : α), f a ∂μ

First moment method. The minimum of an integrable function is smaller than its mean.

theorem MeasureTheory.exists_average_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : Integrable f μ) : ∃ (x : α), ⨍ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of an integrable function is greater than its mean.

theorem MeasureTheory.exists_notMem_null_le_average {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ℝ} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : Integrable f μ) (hN : μ N = 0) : ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

First moment method. The minimum of an integrable function is smaller than its mean, while avoiding a null set.

theorem MeasureTheory.exists_notMem_null_average_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ℝ} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : Integrable f μ) (hN : μ N = 0) : ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of an integrable function is greater than its mean, while avoiding a null set.

theorem MeasureTheory.measure_le_integral_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsProbabilityMeasure μ] (hf : Integrable f μ) : 0 < μ {x : α | f x ≤ ∫ (a : α), f a ∂μ}

First moment method. An integrable function is smaller than its integral on a set of positive measure.

theorem MeasureTheory.measure_integral_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsProbabilityMeasure μ] (hf : Integrable f μ) : 0 < μ {x : α | ∫ (a : α), f a ∂μ ≤ f x}

First moment method. An integrable function is greater than its integral on a set of positive measure.

theorem MeasureTheory.exists_le_integral {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsProbabilityMeasure μ] (hf : Integrable f μ) : ∃ (x : α), f x ≤ ∫ (a : α), f a ∂μ

First moment method. The minimum of an integrable function is smaller than its integral.

theorem MeasureTheory.exists_integral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} [IsProbabilityMeasure μ] (hf : Integrable f μ) : ∃ (x : α), ∫ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of an integrable function is greater than its integral.

theorem MeasureTheory.exists_notMem_null_le_integral {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ℝ} [IsProbabilityMeasure μ] (hf : Integrable f μ) (hN : μ N = 0) : ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ

First moment method. The minimum of an integrable function is smaller than its integral, while avoiding a null set.

theorem MeasureTheory.exists_notMem_null_integral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ℝ} [IsProbabilityMeasure μ] (hf : Integrable f μ) (hN : μ N = 0) : ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of an integrable function is greater than its integral, while avoiding a null set.

theorem MeasureTheory.measure_le_setLAverage_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ⊤) (hf : AEMeasurable f (μ.restrict s)) : 0 < μ {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}

First moment method. A measurable function is smaller than its mean on a set of positive measure.

theorem MeasureTheory.measure_setLAverage_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} (hμ : μ s ≠ 0) (hs : NullMeasurableSet s μ) (hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤) : 0 < μ {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

First moment method. A measurable function is greater than its mean on a set of positive measure.

theorem MeasureTheory.exists_le_setLAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ⊤) (hf : AEMeasurable f (μ.restrict s)) : ∃ x ∈ s, f x ≤ ⨍⁻ (a : α) in s, f a ∂μ

First moment method. The minimum of a measurable function is smaller than its mean.

theorem MeasureTheory.exists_setLAverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} {f : α → ENNReal} (hμ : μ s ≠ 0) (hs : NullMeasurableSet s μ) (hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤) : ∃ x ∈ s, ⨍⁻ (a : α) in s, f a ∂μ ≤ f x

First moment method. The maximum of a measurable function is greater than its mean.

theorem MeasureTheory.measure_laverage_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hμ : μ ≠ 0) (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : 0 < μ {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x}

First moment method. A measurable function is greater than its mean on a set of positive measure.

theorem MeasureTheory.exists_laverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} (hμ : μ ≠ 0) (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : ∃ (x : α), ⨍⁻ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of a measurable function is greater than its mean.

theorem MeasureTheory.exists_notMem_null_laverage_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ENNReal} (hμ : μ ≠ 0) (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) (hN : μ N = 0) : ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of a measurable function is greater than its mean, while avoiding a null set.

theorem MeasureTheory.measure_le_laverage_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : AEMeasurable f μ) : 0 < μ {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ}

First moment method. A measurable function is smaller than its mean on a set of positive measure.

theorem MeasureTheory.exists_le_laverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : AEMeasurable f μ) : ∃ (x : α), f x ≤ ⨍⁻ (a : α), f a ∂μ

First moment method. The minimum of a measurable function is smaller than its mean.

theorem MeasureTheory.exists_notMem_null_le_laverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ENNReal} [IsFiniteMeasure μ] (hμ : μ ≠ 0) (hf : AEMeasurable f μ) (hN : μ N = 0) : ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

First moment method. The minimum of a measurable function is smaller than its mean, while avoiding a null set.

theorem MeasureTheory.measure_le_lintegral_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} [IsProbabilityMeasure μ] (hf : AEMeasurable f μ) : 0 < μ {x : α | f x ≤ ∫⁻ (a : α), f a ∂μ}

First moment method. A measurable function is smaller than its integral on a set f positive measure.

theorem MeasureTheory.measure_lintegral_le_pos {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} [IsProbabilityMeasure μ] (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : 0 < μ {x : α | ∫⁻ (a : α), f a ∂μ ≤ f x}

First moment method. A measurable function is greater than its integral on a set f positive measure.

theorem MeasureTheory.exists_le_lintegral {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} [IsProbabilityMeasure μ] (hf : AEMeasurable f μ) : ∃ (x : α), f x ≤ ∫⁻ (a : α), f a ∂μ

First moment method. The minimum of a measurable function is smaller than its integral.

theorem MeasureTheory.exists_lintegral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} [IsProbabilityMeasure μ] (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : ∃ (x : α), ∫⁻ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of a measurable function is greater than its integral.

theorem MeasureTheory.exists_notMem_null_le_lintegral {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ENNReal} [IsProbabilityMeasure μ] (hf : AEMeasurable f μ) (hN : μ N = 0) : ∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ

First moment method. The minimum of a measurable function is smaller than its integral, while avoiding a null set.

theorem MeasureTheory.exists_notMem_null_lintegral_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {N : Set α} {f : α → ENNReal} [IsProbabilityMeasure μ] (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) (hN : μ N = 0) : ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x

First moment method. The maximum of a measurable function is greater than its integral, while avoiding a null set.

theorem MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} [CompleteSpace E] {ι : Type u_4} {a : ι → Set α} {l : Filter ι} {f : α → E} {c : E} {g : ι → α → ℝ} (K : ℝ) (hf : Filter.Tendsto (fun (i : ι) => ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (nhds 0)) (f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ) (hg : Filter.Tendsto (fun (i : ι) => ∫ (y : α), g i y ∂μ) l (nhds 1)) (g_supp : ∀ᶠ (i : ι) in l, Function.support (g i) ⊆ a i) (g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)) : Filter.Tendsto (fun (i : ι) => ∫ (y : α), g i y • f y ∂μ) l (nhds c)

If the average of a function f along a sequence of sets aₙ converges to c (more precisely, we require that ⨍ y in a i, ‖f y - c‖ ∂μ tends to 0), then the integral of gₙ • f also tends to c if gₙ is supported in aₙ, has integral converging to one and supremum at most K / μ aₙ.

theorem MeasureTheory.exists_eq_setAverage {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α} [TopologicalSpace α] {f : α → ℝ} (hs : IsConnected s) (hf : ContinuousOn f s) (hint : IntegrableOn f s μ) (hμfin : μ s ≠ ⊤) (hμ0 : μ s ≠ 0) : ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ

If s is a connected set of finite, nonzero μ-measure and f : α → ℝ is continuous on s and integrable on s w.r.t. μ, then f attains its μ-average on s.