mathlib documentation

measure_theory.integral.average

Integral average of a function #

In this file we define measure_theory.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.

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 measure_theory.integrable.to_average.

Tags #

integral, center mass, average value

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

The average value of a function f w.r.t. a measure μ (notation: ⨍ x, f x ∂μ) is defined as (μ univ).to_real⁻¹ • ∫ x, f x ∂μ, 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.

noncomputable def measure_theory.average {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) :

E

Average value of a function f w.r.t. a measure μ, notation: ⨍ x, f x ∂μ. It is defined as (μ univ).to_real⁻¹ • ∫ x, f x ∂μ, 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, use ⨍ x in s, f x ∂μ (defined as ⨍ x, f x ∂(μ.restrict s)). For average w.r.t. the volume, one can omit ∂volume.

Equations

measure_theory.average μ f = ∫ (x : α), f x ∂(⇑μ set.univ)⁻¹ • μ

@[simp]

theorem measure_theory.average_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) :

⨍ (x : α), 0 ∂μ = 0

@[simp]

theorem measure_theory.average_zero_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (f : α → E) :

⨍ (x : α), f x ∂0 = 0

@[simp]

theorem measure_theory.average_neg {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) :

⨍ (x : α), -f x ∂μ = -⨍ (x : α), f x ∂μ

theorem measure_theory.average_eq' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) :

⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂(⇑μ set.univ)⁻¹ • μ

theorem measure_theory.average_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) :

⨍ (x : α), f x ∂μ = ((⇑μ set.univ).to_real)⁻¹ • ∫ (x : α), f x ∂μ

theorem measure_theory.average_eq_integral {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] (f : α → E) :

⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

@[simp]

theorem measure_theory.measure_smul_average {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) [measure_theory.is_finite_measure μ] (f : α → E) :

(⇑μ set.univ).to_real • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

theorem measure_theory.set_average_eq {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) (s : set α) :

⨍ (x : α) in s, f x ∂μ = ((⇑μ s).to_real)⁻¹ • ∫ (x : α) in s, f x ∂μ

theorem measure_theory.set_average_eq' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) (s : set α) :

⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(⇑μ s)⁻¹ • μ.restrict s

theorem measure_theory.average_congr {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} {f g : α → E} (h : f =ᵐ[μ] g) :

⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ

theorem measure_theory.average_add_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {ν : measure_theory.measure α} [measure_theory.is_finite_measure ν] {f : α → E} (hμ : measure_theory.integrable f μ) (hν : measure_theory.integrable f ν) :

⨍ (x : α), f x ∂(μ + ν) = ((⇑μ set.univ).to_real / ((⇑μ set.univ).to_real + (⇑ν set.univ).to_real)) • ⨍ (x : α), f x ∂μ + ((⇑ν set.univ).to_real / ((⇑μ set.univ).to_real + (⇑ν set.univ).to_real)) • ⨍ (x : α), f x ∂ν

theorem measure_theory.average_pair {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] [normed_add_comm_group F] [normed_space ℝ F] [complete_space F] {μ : measure_theory.measure α} {f : α → E} {g : α → F} (hfi : measure_theory.integrable f μ) (hgi : measure_theory.integrable g μ) :

⨍ (x : α), (f x, g x) ∂μ = (⨍ (x : α), f x ∂μ, ⨍ (x : α), g x ∂μ)

theorem measure_theory.measure_smul_set_average {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} (f : α → E) {s : set α} (h : ⇑μ s ≠ ⊤) :

(⇑μ s).to_real • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ

theorem measure_theory.average_union {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} {f : α → E} {s t : set α} (hd : measure_theory.ae_disjoint μ s t) (ht : measure_theory.null_measurable_set t μ) (hsμ : ⇑μ s ≠ ⊤) (htμ : ⇑μ t ≠ ⊤) (hfs : measure_theory.integrable_on f s μ) (hft : measure_theory.integrable_on f t μ) :

⨍ (x : α) in s ∪ t, f x ∂μ = ((⇑μ s).to_real / ((⇑μ s).to_real + (⇑μ t).to_real)) • ⨍ (x : α) in s, f x ∂μ + ((⇑μ t).to_real / ((⇑μ s).to_real + (⇑μ t).to_real)) • ⨍ (x : α) in t, f x ∂μ

theorem measure_theory.average_union_mem_open_segment {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} {f : α → E} {s t : set α} (hd : measure_theory.ae_disjoint μ s t) (ht : measure_theory.null_measurable_set t μ) (hs₀ : ⇑μ s ≠ 0) (ht₀ : ⇑μ t ≠ 0) (hsμ : ⇑μ s ≠ ⊤) (htμ : ⇑μ t ≠ ⊤) (hfs : measure_theory.integrable_on f s μ) (hft : measure_theory.integrable_on f t μ) :

⨍ (x : α) in s ∪ t, f x ∂μ ∈ open_segment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

theorem measure_theory.average_union_mem_segment {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} {f : α → E} {s t : set α} (hd : measure_theory.ae_disjoint μ s t) (ht : measure_theory.null_measurable_set t μ) (hsμ : ⇑μ s ≠ ⊤) (htμ : ⇑μ t ≠ ⊤) (hfs : measure_theory.integrable_on f s μ) (hft : measure_theory.integrable_on f t μ) :

⨍ (x : α) in s ∪ t, f x ∂μ ∈ segment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

theorem measure_theory.average_mem_open_segment_compl_self {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {f : α → E} {s : set α} (hs : measure_theory.null_measurable_set s μ) (hs₀ : ⇑μ s ≠ 0) (hsc₀ : ⇑μ sᶜ ≠ 0) (hfi : measure_theory.integrable f μ) :

⨍ (x : α), f x ∂μ ∈ open_segment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ , f x ∂μ)

@[simp]

theorem measure_theory.average_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] [h : μ.ae.ne_bot] (c : E) :

⨍ (x : α), c ∂μ = c

theorem measure_theory.set_average_const {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {μ : measure_theory.measure α} {s : set α} (hs₀ : ⇑μ s ≠ 0) (hs : ⇑μ s ≠ ⊤) (c : E) :

⨍ (x : α) in s, c ∂μ = c