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_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
@[simp]
theorem measure_theory.average_zero {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_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_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_group E] [normed_space E] [complete_space E] (μ : measure_theory.measure α) (f : α → E) :
(x : α), -f x μ = - (x : α), f x μ
theorem measure_theory.average_def {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_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_def' {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_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_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_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_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.average_congr {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [normed_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_pair {α : Type u_1} {E : Type u_2} {F : Type u_3} {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] [normed_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_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_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_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_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_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 μ)