mathlib3 documentation

measure_theory.integral.average

Integral average of a function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

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

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 (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 measure_theory.laverage {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α 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
@[simp]
theorem measure_theory.laverage_zero {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) :
⨍⁻ (x : α), 0 μ = 0
@[simp]
theorem measure_theory.laverage_zero_measure {α : Type u_1} {m0 : measurable_space α} (f : α ennreal) :
⨍⁻ (x : α), f x 0 = 0
theorem measure_theory.laverage_eq' {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :
⨍⁻ (x : α), f x μ = ∫⁻ (x : α), f x (μ set.univ)⁻¹ μ
theorem measure_theory.laverage_eq {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :
⨍⁻ (x : α), f x μ = ∫⁻ (x : α), f x μ / μ set.univ
@[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 μ
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
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
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 μ
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 μ
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 μ
theorem measure_theory.laverage_lt_top {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {f : α ennreal} (hf : ∫⁻ (x : α), f x μ ) :
⨍⁻ (x : α), f x μ <
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 μ <
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 ν
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 μ
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 μ
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 μ)
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 μ)
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 μ)
@[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
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
@[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
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
@[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 μ
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 μ
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
@[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.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 μ
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 μ
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
@[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 μ
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 μ
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
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
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
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
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
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
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 μ
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 μ

First moment method #

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.