# mathlib3documentation

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 μ /
theorem measure_theory.laverage_eq_lintegral {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :
⨍⁻ (x : α), f x μ = ∫⁻ (x : α), f x μ
@[simp]
theorem measure_theory.measure_mul_laverage {α : Type u_1} {m0 : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :
* ⨍⁻ (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 + ν) = / + * ⨍⁻ (x : α), f x μ + / + * ⨍⁻ (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 : t) (ht : μ) :
⨍⁻ (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 : t) (ht : μ) (hs₀ : μ s 0) (ht₀ : μ t 0) (hsμ : μ s ) (htμ : μ t ) :
⨍⁻ (x : α) in s t, f x μ (⨍⁻ (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 : t) (ht : μ) (hsμ : μ s ) (htμ : μ t ) :
⨍⁻ (x : α) in s t, f x μ (⨍⁻ (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} (hs : μ) (hs₀ : μ s 0) (hsc₀ : μ s 0) :
⨍⁻ (x : α), f x μ (⨍⁻ (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 α) [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 α} [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 α) (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 α) (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 α} [ 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 α} [ E] (μ : measure_theory.measure α) :
(x : α), 0 μ = 0
@[simp]
theorem measure_theory.average_zero_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_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 α} [ 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 α} [ 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 α} [ 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 α} [ E] (μ : measure_theory.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 α} [ E] (μ : measure_theory.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 α} [ 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 α} [ 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 α} [ 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 α} [ 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 α} [ 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_add_measure {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} [ E] {μ : measure_theory.measure α} {ν : measure_theory.measure α} {f : α E} (hμ : μ) (hν : ν) :
(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 α} [ E] [ F] {μ : measure_theory.measure α} {f : α E} {g : α F} (hfi : μ) (hgi : μ) :
(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 α} [ 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 α} [ E] {μ : measure_theory.measure α} {f : α E} {s t : set α} (hd : t) (ht : μ) (hsμ : μ s ) (htμ : μ t ) (hfs : μ) (hft : μ) :
(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 α} [ E] {μ : measure_theory.measure α} {f : α E} {s t : set α} (hd : t) (ht : μ) (hs₀ : μ s 0) (ht₀ : μ t 0) (hsμ : μ s ) (htμ : μ t ) (hfs : μ) (hft : μ) :
(x : α) in s t, f x μ ( (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 α} [ E] {μ : measure_theory.measure α} {f : α E} {s t : set α} (hd : t) (ht : μ) (hsμ : μ s ) (htμ : μ t ) (hfs : μ) (hft : μ) :
(x : α) in s t, f x μ ( (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 α} [ E] {μ : measure_theory.measure α} {f : α E} {s : set α} (hs : μ) (hs₀ : μ s 0) (hsc₀ : μ s 0) (hfi : μ) :
(x : α), f x μ ( (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 α} [ E] (μ : measure_theory.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 α} [ 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 α} [ E] (μ : measure_theory.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 α} [ E] (μ : measure_theory.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 α} [ E] (μ : measure_theory.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 α} [ 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 α} [ E] {μ : measure_theory.measure α} {f : α E} (hf : μ) :
(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 α} [ E] {μ : measure_theory.measure α} {s : set α} {f : α E} (hs : μ s ) (hf : μ) :
(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 : μ) (hf₀ : 0 ≤ᵐ[μ] f) :
ennreal.of_real ( (x : α), f x μ) = ∫⁻ (x : α), ennreal.of_real (f x) μ /
theorem measure_theory.of_real_set_average {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {s : set α} {f : α } (hf : μ) (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 : μ) (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 : (μ.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 : μ) :
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 : μ) :
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 : μ) :
(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 : μ) :
(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 : α } (hμ : μ 0) (hf : μ) :
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 : α } (hμ : μ 0) (hf : μ) :
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 : α } (hμ : μ 0) (hf : μ) :
(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 : α } (hμ : μ 0) (hf : μ) :
(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 : α } (hμ : μ 0) (hf : μ) (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 : α } (hμ : μ 0) (hf : μ) (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 : α } (hf : μ) :
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 : α } (hf : μ) :
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 : α } (hf : μ) :
(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 : α } (hf : μ) :
(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 : α } (hf : μ) (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 : α } (hf : μ) (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 : (μ.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 : μ) (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 : (μ.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 : μ) (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} (hμ : μ 0) (hf : μ) :
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} (hμ : μ 0) (hf : μ) :
(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} (hμ : μ 0) (hf : μ) (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} (hf : μ) :
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} (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} (hf : μ) :
(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} (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} (hf : μ) (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} (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.