measure_theory.integral.average

source

noncomputable def measure_theory.laverage {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) :

ennreal

Average value of an ℝ≥0∞-valued function f w.r.t. a measure μ, notation: ⨍⁻ x, f x ∂μ. It is defined as μ univ⁻¹ * ∫⁻ x, f x ∂μ, so it is equal to 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 average w.r.t. the volume, one can omit ∂volume.

Equations

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

source

@[simp]

theorem measure_theory.laverage_zero {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) :

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

source

@[simp]

theorem measure_theory.laverage_zero_measure {α : Type u_1} {m0 : measurable_space α} (f : α → ennreal) :

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

source

theorem measure_theory.laverage_eq' {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) :

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

source

theorem measure_theory.laverage_eq {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) :

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

source

theorem measure_theory.laverage_eq_lintegral {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) [measure_theory.is_probability_measure μ] (f : α → ennreal) :

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

source

@[simp]

theorem measure_theory.measure_mul_laverage {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) [measure_theory.is_finite_measure μ] (f : α → ennreal) :

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

source

theorem measure_theory.set_laverage_eq {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) (s : set α) :

⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ / ⇑μ s

source

theorem measure_theory.set_laverage_eq' {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α → ennreal) (s : set α) :

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

source

theorem measure_theory.laverage_congr {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f g : α → ennreal} (h : f =ᵐ[μ] g) :

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

source

theorem measure_theory.set_laverage_congr {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {f : α → ennreal} (h : s =ᵐ[μ] t) :

⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ

source

theorem measure_theory.set_laverage_congr_fun {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f g : α → ennreal} (hs : measurable_set s) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) :

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

source

theorem measure_theory.laverage_lt_top {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤) :

⨍⁻ (x : α), f x ∂μ < ⊤

source

theorem measure_theory.set_laverage_lt_top {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} :

∫⁻ (x : α) in s, f x ∂μ ≠ ⊤ → ⨍⁻ (x : α) in s, f x ∂μ < ⊤

source

theorem measure_theory.laverage_add_measure {α : Type u_1} {m0 : measurable_space α} {μ ν : measure_theory.measure α} {f : α → ennreal} :

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

source

theorem measure_theory.measure_mul_set_laverage {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (f : α → ennreal) (h : ⇑μ s ≠ ⊤) :

⇑μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ

source

theorem measure_theory.laverage_union {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {f : α → ennreal} (hd : measure_theory.ae_disjoint μ s t) (ht : measure_theory.null_measurable_set t μ) :

⨍⁻ (x : α) in s ∪ t, f x ∂μ = ⇑μ s / (⇑μ s + ⇑μ t) * ⨍⁻ (x : α) in s, f x ∂μ + ⇑μ t / (⇑μ s + ⇑μ t) * ⨍⁻ (x : α) in t, f x ∂μ

source

theorem measure_theory.laverage_union_mem_open_segment {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {f : α → ennreal} (hd : measure_theory.ae_disjoint μ s t) (ht : measure_theory.null_measurable_set t μ) (hs₀ : ⇑μ s ≠ 0) (ht₀ : ⇑μ t ≠ 0) (hsμ : ⇑μ s ≠ ⊤) (htμ : ⇑μ t ≠ ⊤) :

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

source

theorem measure_theory.laverage_union_mem_segment {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s t : set α} {f : α → ennreal} (hd : measure_theory.ae_disjoint μ s t) (ht : measure_theory.null_measurable_set t μ) (hsμ : ⇑μ s ≠ ⊤) (htμ : ⇑μ t ≠ ⊤) :

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

source

theorem measure_theory.laverage_mem_open_segment_compl_self {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} [measure_theory.is_finite_measure μ] (hs : measure_theory.null_measurable_set s μ) (hs₀ : ⇑μ s ≠ 0) (hsc₀ : ⇑μ sᶜ ≠ 0) :

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

source

@[simp]

theorem measure_theory.laverage_const {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) [measure_theory.is_finite_measure μ] [h : μ.ae.ne_bot] (c : ennreal) :

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

source

theorem measure_theory.set_laverage_const {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs₀ : ⇑μ s ≠ 0) (hs : ⇑μ s ≠ ⊤) (c : ennreal) :

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

source

@[simp]

theorem measure_theory.laverage_one {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] [h : μ.ae.ne_bot] :

⨍⁻ (x : α), 1 ∂μ = 1

source

theorem measure_theory.set_laverage_one {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} (hs₀ : ⇑μ s ≠ 0) (hs : ⇑μ s ≠ ⊤) :

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

source

@[simp]

theorem measure_theory.lintegral_laverage {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) [measure_theory.is_finite_measure μ] (f : α → ennreal) :

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

source

theorem measure_theory.set_lintegral_set_laverage {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) [measure_theory.is_finite_measure μ] (f : α → ennreal) (s : set α) :

∫⁻ (x : α) in s, ⨍⁻ (a : α) in s, f a ∂μ ∂μ = ∫⁻ (x : α) in s, f x ∂μ

source

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)⁻¹ • μ

source

@[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

source

@[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

source

@[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 ∂μ

source

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)⁻¹ • μ

source

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

source

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

source

@[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 ∂μ

source

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

source

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

source

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

source

theorem measure_theory.set_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 α} {s t : set α} {f : α → E} (h : s =ᵐ[μ] t) :

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

source

theorem measure_theory.set_average_congr_fun {α : 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 α} {f g : α → E} (hs : measurable_set s) (h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x) :

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

source

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 ∂ν

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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

source

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

source

@[simp]

theorem measure_theory.integral_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) :

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

source

theorem measure_theory.set_integral_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 α) [measure_theory.is_finite_measure μ] (f : α → E) (s : set α) :

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

source

theorem measure_theory.integral_sub_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) :

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

source

theorem measure_theory.set_integral_sub_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 α} {s : set α} (hs : ⇑μ s ≠ ⊤) (f : α → E) :

∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ = 0

source

theorem measure_theory.integral_average_sub {α : 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} [measure_theory.is_finite_measure μ] (hf : measure_theory.integrable f μ) :

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

source

theorem measure_theory.set_integral_set_average_sub {α : 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 α} {f : α → E} (hs : ⇑μ s ≠ ⊤) (hf : measure_theory.integrable_on f s μ) :

∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ - f x ∂μ = 0

source

theorem measure_theory.of_real_average {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} (hf : measure_theory.integrable f μ) (hf₀ : 0 ≤ᵐ[μ] f) :

ennreal.of_real (⨍ (x : α), f x ∂μ) = ∫⁻ (x : α), ennreal.of_real (f x) ∂μ / ⇑μ set.univ

source

theorem measure_theory.of_real_set_average {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ℝ} (hf : measure_theory.integrable_on f s μ) (hf₀ : 0 ≤ᵐ[μ.restrict s] f) :

ennreal.of_real (⨍ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in s, ennreal.of_real (f x) ∂μ / ⇑μ s

source

theorem measure_theory.to_real_laverage {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} (hf : ae_measurable f μ) (hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) :

(⨍⁻ (x : α), f x ∂μ).to_real = ⨍ (x : α), (f x).to_real ∂μ

source

theorem measure_theory.to_real_set_laverage {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} (hf : ae_measurable f (μ.restrict s)) (hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤) :

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

source

theorem measure_theory.measure_le_set_average_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ℝ} (hμ : ⇑μ s ≠ 0) (hμ₁ : ⇑μ s ≠ ⊤) (hf : measure_theory.integrable_on f s μ) :

0 < ⇑μ {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.

source

theorem measure_theory.measure_set_average_le_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ℝ} (hμ : ⇑μ s ≠ 0) (hμ₁ : ⇑μ s ≠ ⊤) (hf : measure_theory.integrable_on f s μ) :

0 < ⇑μ {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.

source

theorem measure_theory.exists_le_set_average {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ℝ} (hμ : ⇑μ s ≠ 0) (hμ₁ : ⇑μ s ≠ ⊤) (hf : measure_theory.integrable_on f s μ) :

∃ (x : α) (H : x ∈ s), f x ≤ ⨍ (a : α) in s, f a ∂μ

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

source

theorem measure_theory.exists_set_average_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ℝ} (hμ : ⇑μ s ≠ 0) (hμ₁ : ⇑μ s ≠ ⊤) (hf : measure_theory.integrable_on f s μ) :

∃ (x : α) (H : x ∈ s), ⨍ (a : α) in s, f a ∂μ ≤ f x

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

source

theorem measure_theory.measure_le_average_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : measure_theory.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.

source

theorem measure_theory.measure_average_le_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : measure_theory.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.

source

theorem measure_theory.exists_le_average {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : measure_theory.integrable f μ) :

∃ (x : α), f x ≤ ⨍ (a : α), f a ∂μ

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

source

theorem measure_theory.exists_average_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : measure_theory.integrable f μ) :

∃ (x : α), ⨍ (a : α), f a ∂μ ≤ f x

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

source

theorem measure_theory.exists_not_mem_null_le_average {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ℝ} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : measure_theory.integrable f μ) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.exists_not_mem_null_average_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ℝ} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : measure_theory.integrable f μ) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.measure_le_integral_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_probability_measure μ] (hf : measure_theory.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.

source

theorem measure_theory.measure_integral_le_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_probability_measure μ] (hf : measure_theory.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.

source

theorem measure_theory.exists_le_integral {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_probability_measure μ] (hf : measure_theory.integrable f μ) :

∃ (x : α), f x ≤ ∫ (a : α), f a ∂μ

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

source

theorem measure_theory.exists_integral_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ℝ} [measure_theory.is_probability_measure μ] (hf : measure_theory.integrable f μ) :

∃ (x : α), ∫ (a : α), f a ∂μ ≤ f x

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

source

theorem measure_theory.exists_not_mem_null_le_integral {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ℝ} [measure_theory.is_probability_measure μ] (hf : measure_theory.integrable f μ) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.exists_not_mem_null_integral_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ℝ} [measure_theory.is_probability_measure μ] (hf : measure_theory.integrable f μ) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.measure_le_set_laverage_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} (hμ : ⇑μ s ≠ 0) (hμ₁ : ⇑μ s ≠ ⊤) (hf : ae_measurable f (μ.restrict s)) :

0 < ⇑μ {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.

source

theorem measure_theory.measure_set_laverage_le_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} (hμ : ⇑μ s ≠ 0) (hs : measure_theory.null_measurable_set s μ) (hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤) :

0 < ⇑μ {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.

source

theorem measure_theory.exists_le_set_laverage {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} (hμ : ⇑μ s ≠ 0) (hμ₁ : ⇑μ s ≠ ⊤) (hf : ae_measurable f (μ.restrict s)) :

∃ (x : α) (H : x ∈ s), f x ≤ ⨍⁻ (a : α) in s, f a ∂μ

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

source

theorem measure_theory.exists_set_laverage_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α → ennreal} (hμ : ⇑μ s ≠ 0) (hs : measure_theory.null_measurable_set s μ) (hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤) :

∃ (x : α) (H : x ∈ s), ⨍⁻ (a : α) in s, f a ∂μ ≤ f x

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

source

theorem measure_theory.measure_laverage_le_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.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.

source

theorem measure_theory.exists_laverage_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.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.

source

theorem measure_theory.exists_not_mem_null_laverage_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ennreal} (hμ : μ ≠ 0) (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.measure_le_laverage_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : ae_measurable 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.

source

theorem measure_theory.exists_le_laverage {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : ae_measurable f μ) :

∃ (x : α), f x ≤ ⨍⁻ (a : α), f a ∂μ

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

source

theorem measure_theory.exists_not_mem_null_le_laverage {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ennreal} [measure_theory.is_finite_measure μ] (hμ : μ ≠ 0) (hf : ae_measurable f μ) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.measure_le_lintegral_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} [measure_theory.is_probability_measure μ] (hf : ae_measurable f μ) :

0 < ⇑μ {x : α | f x ≤ ∫⁻ (a : α), f a ∂μ}

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

source

theorem measure_theory.measure_lintegral_le_pos {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} [measure_theory.is_probability_measure μ] (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 of positive measure.

source

theorem measure_theory.exists_le_lintegral {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} [measure_theory.is_probability_measure μ] (hf : ae_measurable f μ) :

∃ (x : α), f x ≤ ∫⁻ (a : α), f a ∂μ

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

source

theorem measure_theory.exists_lintegral_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α → ennreal} [measure_theory.is_probability_measure μ] (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) :

∃ (x : α), ∫⁻ (a : α), f a ∂μ ≤ f x

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

source

theorem measure_theory.exists_not_mem_null_le_lintegral {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ennreal} [measure_theory.is_probability_measure μ] (hf : ae_measurable f μ) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

source

theorem measure_theory.exists_not_mem_null_lintegral_le {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {N : set α} {f : α → ennreal} [measure_theory.is_probability_measure μ] (hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤) (hN : ⇑μ N = 0) :

∃ (x : α) (H : 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.

mathlib3 documentation

Integral average of a function #

Implementation notes #

Tags #

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

First moment method #