mathlib documentation

measure_theory.measure_space

Measure spaces

Given a measurable space α, a measure on α is a function that sends measurable sets to the extended nonnegative reals that satisfies the following conditions:

  1. μ ∅ = 0;
  2. μ is countably additive. This means that the measure of a countable union of pairwise disjoint sets is equal to the measure of the individual sets.

Every measure can be canonically extended to an outer measure, so that it assigns values to all subsets, not just the measurable subsets. On the other hand, a measure that is countably additive on measurable sets can be restricted to measurable sets to obtain a measure. In this file a measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.

Measures on α form a complete lattice, and are closed under scalar multiplication with ennreal.

We introduce the following typeclasses for measures:

Given a measure, the null sets are the sets where μ s = 0, where μ denotes the corresponding outer measure (so s might not be measurable). We can then define the completion of μ as the measure on the least σ-algebra that also contains all null sets, by defining the measure to be 0 on the null sets.

Main statements

Implementation notes

Given μ : measure α, μ s is the value of the outer measure applied to s. This conveniently allows us to apply the measure to sets without proving that they are measurable. We get countable subadditivity for all sets, but only countable additivity for measurable sets.

You often don't want to define a measure via its constructor. Two ways that are sometimes more convenient:

To prove that two measures are equal, there are multiple options:

A measure_space is a class that is a measurable space with a canonical measure. The measure is denoted volume.

References

Tags

measure, almost everywhere, measure space, completion, null set, null measurable set

structure measure_theory.measure (α : Type u_1) [measurable_space α] :
Type u_1

A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.

@[instance]

Measure projections for a measure space.

For measurable sets this returns the measure assigned by the measure_of field in measure. But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and subadditivity for all sets.

Equations

General facts about measures

def measure_theory.measure.of_measurable {α : Type u_1} [measurable_space α] (m : Π (s : set α), is_measurable sennreal) :
m is_measurable.empty = 0(∀ ⦃f : set α⦄ (h : ∀ (i : ), is_measurable (f i)), pairwise (disjoint on f)(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _))measure_theory.measure α

Obtain a measure by giving a countably additive function that sends to 0.

Equations
theorem measure_theory.measure.of_measurable_apply {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable sennreal} {m0 : m is_measurable.empty = 0} {mU : ∀ ⦃f : set α⦄ (h : ∀ (i : ), is_measurable (f i)), pairwise (disjoint on f)(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _)} (s : set α) (hs : is_measurable s) :

@[ext]
theorem measure_theory.measure.ext {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} :
(∀ (s : set α), is_measurable sμ₁ s = μ₂ s)μ₁ = μ₂

theorem measure_theory.measure.ext_iff {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} :
μ₁ = μ₂ ∀ (s : set α), is_measurable sμ₁ s = μ₂ s

theorem measure_theory.measure_eq_trim {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (s : set α) :

theorem measure_theory.measure_eq_infi {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (s : set α) :
μ s = ⨅ (t : set α) (st : s t) (ht : is_measurable t), μ t

theorem measure_theory.measure_eq_extend {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
is_measurable sμ s = measure_theory.extend (λ (t : set α) (ht : is_measurable t), μ t) s

@[simp]
theorem measure_theory.measure_empty {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :
μ = 0

theorem measure_theory.nonempty_of_measure_ne_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
μ s 0 → s.nonempty

theorem measure_theory.measure_mono {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
s₁ s₂μ s₁ μ s₂

theorem measure_theory.measure_mono_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
s₁ s₂μ s₂ = 0μ s₁ = 0

theorem measure_theory.measure_mono_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
s₁ s₂μ s₁ = μ s₂ =

theorem measure_theory.exists_is_measurable_superset_of_measure_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
μ s = 0(∃ (t : set α), s t is_measurable t μ t = 0)

theorem measure_theory.exists_is_measurable_superset_iff_measure_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(∃ (t : set α), s t is_measurable t μ t = 0) μ s = 0

theorem measure_theory.measure_Union_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {β : Type u_2} [encodable β] (s : β → set α) :
μ (⋃ (i : β), s i) ∑' (i : β), μ (s i)

theorem measure_theory.measure_bUnion_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set β} (hs : s.countable) (f : β → set α) :
μ (⋃ (b : β) (H : b s), f b) ∑' (p : s), μ (f p)

theorem measure_theory.measure_bUnion_finset_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} (s : finset β) (f : β → set α) :
μ (⋃ (b : β) (H : b s), f b) ∑ (p : β) in s, μ (f p)

theorem measure_theory.measure_bUnion_lt_top {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set β} {f : β → set α} :
s.finite(∀ (i : β), i sμ (f i) < )μ (⋃ (i : β) (H : i s), f i) <

theorem measure_theory.measure_Union_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {β : Type u_2} [encodable β] {s : β → set α} :
(∀ (i : β), μ (s i) = 0)μ (⋃ (i : β), s i) = 0

theorem measure_theory.measure_Union_null_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {s : ι → set α} :
μ (⋃ (i : ι), s i) = 0 ∀ (i : ι), μ (s i) = 0

theorem measure_theory.measure_union_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (s₁ s₂ : set α) :
μ (s₁ s₂) μ s₁ + μ s₂

theorem measure_theory.measure_union_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
μ s₁ = 0μ s₂ = 0μ (s₁ s₂) = 0

theorem measure_theory.measure_union_null_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
μ (s₁ s₂) = 0 μ s₁ = 0 μ s₂ = 0

theorem measure_theory.measure_Union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {β : Type u_2} [encodable β] {f : β → set α} :
pairwise (disjoint on f)(∀ (i : β), is_measurable (f i))(μ (⋃ (i : β), f i) = ∑' (i : β), μ (f i))

theorem measure_theory.measure_union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
disjoint s₁ s₂is_measurable s₁is_measurable s₂μ (s₁ s₂) = μ s₁ + μ s₂

theorem measure_theory.measure_bUnion {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set β} {f : β → set α} :
s.countables.pairwise_on (disjoint on f)(∀ (b : β), b sis_measurable (f b))(μ (⋃ (b : β) (H : b s), f b) = ∑' (p : s), μ (f p))

theorem measure_theory.measure_sUnion {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {S : set (set α)} :
S.countableS.pairwise_on disjoint(∀ (s : set α), s Sis_measurable s)(μ (⋃₀S) = ∑' (s : S), μ s)

theorem measure_theory.measure_bUnion_finset {α : Type u_1} {ι : Type u_3} [measurable_space α] {μ : measure_theory.measure α} {s : finset ι} {f : ι → set α} :
s.pairwise_on (disjoint on f)(∀ (b : ι), b sis_measurable (f b))μ (⋃ (b : ι) (H : b s), f b) = ∑ (p : ι) in s, μ (f p)

theorem measure_theory.tsum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set β} (hs : s.countable) {f : α → β} :
(∀ (y : β), y sis_measurable (f ⁻¹' {y}))(∑' (b : s), μ (f ⁻¹' {b})) = μ (f ⁻¹' s)

If s is a countable set, then the measure of its preimage can be found as the sum of measures of the fibers f ⁻¹' {y}.

theorem measure_theory.sum_measure_preimage_singleton {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} (s : finset β) {f : α → β} :
(∀ (y : β), y sis_measurable (f ⁻¹' {y}))∑ (b : β) in s, μ (f ⁻¹' {b}) = μ (f ⁻¹' s)

If s is a finset, then the measure of its preimage can be found as the sum of measures of the fibers f ⁻¹' {y}.

theorem measure_theory.measure_diff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} :
s₂ s₁is_measurable s₁is_measurable s₂μ s₂ < μ (s₁ \ s₂) = μ s₁ - μ s₂

theorem measure_theory.measure_compl {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
is_measurable sμ s < μ s = μ set.univ - μ s

theorem measure_theory.sum_measure_le_measure_univ {α : Type u_1} {ι : Type u_3} [measurable_space α] {μ : measure_theory.measure α} {s : finset ι} {t : ι → set α} :
(∀ (i : ι), i sis_measurable (t i))s.pairwise_on (disjoint on t)∑ (i : ι) in s, μ (t i) μ set.univ

theorem measure_theory.tsum_measure_le_measure_univ {α : Type u_1} {ι : Type u_3} [measurable_space α] {μ : measure_theory.measure α} {s : ι → set α} :
(∀ (i : ι), is_measurable (s i))pairwise (disjoint on s)(∑' (i : ι), μ (s i)) μ set.univ

theorem measure_theory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure {α : Type u_1} {ι : Type u_3} [measurable_space α] (μ : measure_theory.measure α) {s : ι → set α} :
(∀ (i : ι), is_measurable (s i))(μ set.univ < ∑' (i : ι), μ (s i))(∃ (i j : ι) (h : i j), (s i s j).nonempty)

Pigeonhole principle for measure spaces: if ∑' i, μ (s i) > μ univ, then one of the intersections s i ∩ s j is not empty.

theorem measure_theory.exists_nonempty_inter_of_measure_univ_lt_sum_measure {α : Type u_1} {ι : Type u_3} [measurable_space α] (μ : measure_theory.measure α) {s : finset ι} {t : ι → set α} :
(∀ (i : ι), i sis_measurable (t i))μ set.univ < ∑ (i : ι) in s, μ (t i)(∃ (i : ι) (H : i s) (j : ι) (H : j s) (h : i j), (t i t j).nonempty)

Pigeonhole principle for measure spaces: if s is a finset and ∑ i in s, μ (t i) > μ univ, then one of the intersections t i ∩ t j is not empty.

theorem measure_theory.measure_Union_eq_supr {α : Type u_1} {ι : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} :
(∀ (i : ι), is_measurable (s i))directed has_subset.subset s(μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i))

Continuity from below: the measure of the union of a directed sequence of measurable sets is the supremum of the measures.

theorem measure_theory.measure_bUnion_eq_supr {α : Type u_1} {ι : Type u_3} [measurable_space α] {μ : measure_theory.measure α} {s : ι → set α} {t : set ι} :
t.countable(∀ (i : ι), i tis_measurable (s i))directed_on (has_subset.subset on s) t(μ (⋃ (i : ι) (H : i t), s i) = ⨆ (i : ι) (H : i t), μ (s i))

theorem measure_theory.measure_Inter_eq_infi {α : Type u_1} {ι : Type u_3} [measurable_space α] {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} :
(∀ (i : ι), is_measurable (s i))directed superset s(∃ (i : ι), μ (s i) < )(μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i))

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the infimum of the measures.

theorem measure_theory.measure_eq_inter_diff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable sis_measurable tμ s = μ (s t) + μ (s \ t)

theorem measure_theory.measure_union_add_inter {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable sis_measurable tμ (s t) + μ (s t) = μ s + μ t

theorem measure_theory.tendsto_measure_Union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(∀ (n : ), is_measurable (s n))monotone sfilter.tendsto (μ s) filter.at_top (𝓝 (μ (⋃ (n : ), s n)))

Continuity from below: the measure of the union of an increasing sequence of measurable sets is the limit of the measures.

theorem measure_theory.tendsto_measure_Inter {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(∀ (n : ), is_measurable (s n))(∀ ⦃n m : ⦄, n ms m s n)(∃ (i : ), μ (s i) < )filter.tendsto (μ s) filter.at_top (𝓝 (μ (⋂ (n : ), s n)))

Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.

theorem measure_theory.measure_limsup_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(∀ (i : ), is_measurable (s i))(∑' (i : ), μ (s i)) μ (filter.at_top.limsup s) = 0

One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of measurable sets such that ∑ μ sᵢ exists, then the limit superior of the sᵢ is a null set.

theorem measure_theory.measure_if {α : Type u_1} [measurable_space α] {β : Type u_2} {x : β} {t : set β} {s : set α} {μ : measure_theory.measure α} :
μ (ite (x t) s ) = t.indicator (λ (_x : β), μ s) x

Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.

Equations
@[simp]
theorem measure_theory.to_measure_apply {α : Type u_1} (m : measure_theory.outer_measure α) [ms : measurable_space α] (h : ms m.caratheodory) {s : set α} :
is_measurable s(m.to_measure h) s = m s

theorem measure_theory.le_to_measure_apply {α : Type u_1} (m : measure_theory.outer_measure α) [ms : measurable_space α] (h : ms m.caratheodory) (s : set α) :
m s (m.to_measure h) s

The ennreal-module of measures

@[simp]
theorem measure_theory.measure.coe_zero {α : Type u_1} [measurable_space α] :
0 = 0

@[simp]

@[simp]
theorem measure_theory.measure.coe_add {α : Type u_1} [measurable_space α] (μ₁ μ₂ : measure_theory.measure α) :
(μ₁ + μ₂) = μ₁ + μ₂

theorem measure_theory.measure.add_apply {α : Type u_1} [measurable_space α] (μ₁ μ₂ : measure_theory.measure α) (s : set α) :
(μ₁ + μ₂) s = μ₁ s + μ₂ s

@[simp]
theorem measure_theory.measure.coe_smul {α : Type u_1} [measurable_space α] (c : ennreal) (μ : measure_theory.measure α) :
(c μ) = c μ

theorem measure_theory.measure.smul_apply {α : Type u_1} [measurable_space α] (c : ennreal) (μ : measure_theory.measure α) (s : set α) :
(c μ) s = c * μ s

The complete lattice of measures

@[instance]

Equations
theorem measure_theory.measure.le_iff {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} :
μ₁ μ₂ ∀ (s : set α), is_measurable sμ₁ s μ₂ s

theorem measure_theory.measure.to_outer_measure_le {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} :
μ₁.to_outer_measure μ₂.to_outer_measure μ₁ μ₂

theorem measure_theory.measure.le_iff' {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} :
μ₁ μ₂ ∀ (s : set α), μ₁ s μ₂ s

theorem measure_theory.measure.lt_iff {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} :
μ < ν μ ν ∃ (s : set α), is_measurable s μ s < ν s

theorem measure_theory.measure.lt_iff' {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} :
μ < ν μ ν ∃ (s : set α), μ s < ν s

theorem measure_theory.measure.add_le_add_left {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} (ν : measure_theory.measure α) :
μ₁ μ₂ν + μ₁ ν + μ₂

theorem measure_theory.measure.add_le_add_right {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} (hμ : μ₁ μ₂) (ν : measure_theory.measure α) :
μ₁ + ν μ₂ + ν

theorem measure_theory.measure.add_le_add {α : Type u_1} [measurable_space α] {μ₁ μ₂ : measure_theory.measure α} (hμ : μ₁ μ₂) {ν₁ ν₂ : measure_theory.measure α} :
ν₁ ν₂μ₁ + ν₁ μ₂ + ν₂

theorem measure_theory.measure.le_add_left {α : Type u_1} [measurable_space α] {μ ν ν' : measure_theory.measure α} :
μ νμ ν' + ν

theorem measure_theory.measure.le_add_right {α : Type u_1} [measurable_space α] {μ ν ν' : measure_theory.measure α} :
μ νμ ν + ν'

@[instance]

Equations
theorem measure_theory.measure.zero_le {α : Type u_1} [measurable_space α] (μ : measure_theory.measure α) :
0 μ

theorem measure_theory.measure.le_zero_iff_eq' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :
μ 0 μ = 0

@[simp]

Pushforward and pullback

Lift a linear map between outer_measure spaces such that for each measure μ every measurable set is caratheodory-measurable w.r.t. f μ to a linear map between measure spaces.

Equations
def measure_theory.measure.map {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

The pushforward of a measure. It is defined to be 0 if f is not a measurable function.

Equations
@[simp]
theorem measure_theory.measure.map_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} :

theorem measure_theory.measure.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {g : β → γ} {f : α → β} :

def measure_theory.measure.comap {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] :

Pullback of a measure. If f sends each measurable set to a measurable set, then for each measurable set s we have comap f μ s = μ (f '' s).

Equations
theorem measure_theory.measure.comap_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] (f : α → β) (hfi : function.injective f) (hf : ∀ (s : set α), is_measurable sis_measurable (f '' s)) (μ : measure_theory.measure β) {s : set α} :

Restricting a measure

Restrict a measure μ to a set s.

Equations
@[simp]
theorem measure_theory.measure.restrict_apply {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable t(μ.restrict s) t = μ (t s)

theorem measure_theory.measure.le_restrict_apply {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (s t : set α) :
μ (t s) (μ.restrict s) t

@[simp]
theorem measure_theory.measure.restrict_add {α : Type u_1} [measurable_space α] (μ ν : measure_theory.measure α) (s : set α) :
+ ν).restrict s = μ.restrict s + ν.restrict s

@[simp]
theorem measure_theory.measure.restrict_zero {α : Type u_1} [measurable_space α] (s : set α) :
0.restrict s = 0

@[simp]
theorem measure_theory.measure.restrict_smul {α : Type u_1} [measurable_space α] (c : ennreal) (μ : measure_theory.measure α) (s : set α) :
(c μ).restrict s = c μ.restrict s

@[simp]
theorem measure_theory.measure.restrict_restrict {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable s(μ.restrict t).restrict s = μ.restrict (s t)

theorem measure_theory.measure.restrict_apply_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable t((μ.restrict s) t = 0 μ (t s) = 0)

theorem measure_theory.measure.restrict_apply_eq_zero' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable s((μ.restrict s) t = 0 μ (t s) = 0)

@[simp]
theorem measure_theory.measure.restrict_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
μ.restrict s = 0 μ s = 0

@[simp]

theorem measure_theory.measure.restrict_union_apply {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s s' t : set α} :
disjoint (t s) (t s')is_measurable sis_measurable s'is_measurable t(μ.restrict (s s')) t = (μ.restrict s) t + (μ.restrict s') t

theorem measure_theory.measure.restrict_union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
disjoint s tis_measurable sis_measurable tμ.restrict (s t) = μ.restrict s + μ.restrict t

theorem measure_theory.measure.restrict_union_add_inter {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
is_measurable sis_measurable tμ.restrict (s t) + μ.restrict (s t) = μ.restrict s + μ.restrict t

@[simp]

@[simp]

theorem measure_theory.measure.restrict_union_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (s s' : set α) :
μ.restrict (s s') μ.restrict s + μ.restrict s'

theorem measure_theory.measure.restrict_Union_apply {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {s : ι → set α} (hd : pairwise (disjoint on s)) (hm : ∀ (i : ι), is_measurable (s i)) {t : set α} :
is_measurable t((μ.restrict (⋃ (i : ι), s i)) t = ∑' (i : ι), (μ.restrict (s i)) t)

theorem measure_theory.measure.restrict_Union_apply_eq_supr {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {s : ι → set α} (hm : ∀ (i : ι), is_measurable (s i)) (hd : directed has_subset.subset s) {t : set α} :
is_measurable t((μ.restrict (⋃ (i : ι), s i)) t = ⨆ (i : ι), (μ.restrict (s i)) t)

theorem measure_theory.measure.restrict_map {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} :

theorem measure_theory.measure.restrict_mono {α : Type u_1} [measurable_space α] ⦃s s' : set α⦄ (hs : s s') ⦃μ ν : measure_theory.measure α⦄ :
μ νμ.restrict s ν.restrict s'

Restriction of a measure to a subset is monotone both in set and in measure.

theorem measure_theory.measure.restrict_le_self {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
μ.restrict s μ

theorem measure_theory.measure.restrict_congr_meas {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {s : set α} :
is_measurable s(μ.restrict s = ν.restrict s ∀ (t : set α), t sis_measurable tμ t = ν t)

theorem measure_theory.measure.restrict_congr_mono {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {s t : set α} :
s tis_measurable sμ.restrict t = ν.restrict tμ.restrict s = ν.restrict s

theorem measure_theory.measure.restrict_union_congr {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {s t : set α} :
is_measurable sis_measurable t(μ.restrict (s t) = ν.restrict (s t) μ.restrict s = ν.restrict s μ.restrict t = ν.restrict t)

If two measures agree on all measurable subsets of s and t, then they agree on all measurable subsets of s ∪ t.

theorem measure_theory.measure.restrict_finset_bUnion_congr {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {ι : Type u_4} {s : finset ι} {t : ι → set α} :
(∀ (i : ι), i sis_measurable (t i))(μ.restrict (⋃ (i : ι) (H : i s), t i) = ν.restrict (⋃ (i : ι) (H : i s), t i) ∀ (i : ι), i sμ.restrict (t i) = ν.restrict (t i))

theorem measure_theory.measure.restrict_Union_congr {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {ι : Type u_4} [encodable ι] {s : ι → set α} :
(∀ (i : ι), is_measurable (s i))(μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i) ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i))

theorem measure_theory.measure.restrict_bUnion_congr {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {ι : Type u_4} {s : set ι} {t : ι → set α} :
s.countable(∀ (i : ι), i sis_measurable (t i))(μ.restrict (⋃ (i : ι) (H : i s), t i) = ν.restrict (⋃ (i : ι) (H : i s), t i) ∀ (i : ι), i sμ.restrict (t i) = ν.restrict (t i))

theorem measure_theory.measure.restrict_sUnion_congr {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {S : set (set α)} :
S.countable(∀ (s : set α), s Sis_measurable s)(μ.restrict (⋃₀S) = ν.restrict (⋃₀S) ∀ (s : set α), s Sμ.restrict s = ν.restrict s)

This lemma shows that restrict and to_outer_measure commute. Note that the LHS has a restrict on measures and the RHS has a restrict on outer measures.

theorem measure_theory.measure.restrict_Inf_eq_Inf_restrict {α : Type u_1} [measurable_space α] {m : set (measure_theory.measure α)} {t : set α} :
m.nonemptyis_measurable t(Inf m).restrict t = Inf ((λ (μ : measure_theory.measure α), μ.restrict t) '' m)

This lemma shows that Inf and restrict commute for measures.

Extensionality results

theorem measure_theory.measure.ext_iff_of_Union_eq_univ {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {ι : Type u_4} [encodable ι] {s : ι → set α} :
(∀ (i : ι), is_measurable (s i))(⋃ (i : ι), s i) = set.univ= ν ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i))

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using Union).

theorem measure_theory.measure.ext_iff_of_bUnion_eq_univ {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {ι : Type u_4} {S : set ι} {s : ι → set α} :
S.countable(∀ (i : ι), i Sis_measurable (s i))(⋃ (i : ι) (H : i S), s i) = set.univ= ν ∀ (i : ι), i Sμ.restrict (s i) = ν.restrict (s i))

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using bUnion).

theorem measure_theory.measure.ext_iff_of_sUnion_eq_univ {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {S : set (set α)} :
S.countable(∀ (s : set α), s Sis_measurable s)⋃₀S = set.univ= ν ∀ (s : set α), s Sμ.restrict s = ν.restrict s)

Two measures are equal if they have equal restrictions on a spanning collection of sets (formulated using sUnion).

theorem measure_theory.measure.ext_of_generate_from_of_cover {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {S T : set (set α)} :
_inst_1 = measurable_space.generate_from ST.countableis_pi_system S(∀ (t : set α), t Tis_measurable t)⋃₀T = set.univ(∀ (t : set α), t Tμ t < )(∀ (t : set α), t T∀ (s : set α), s Sμ (s t) = ν (s t))(∀ (t : set α), t Tμ t = ν t)μ = ν

theorem measure_theory.measure.ext_of_generate_from_of_cover_subset {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {S T : set (set α)} :
_inst_1 = measurable_space.generate_from Sis_pi_system ST ST.countable⋃₀T = set.univ(∀ (s : set α), s Tμ s < )(∀ (s : set α), s Sμ s = ν s)μ = ν

Two measures are equal if they are equal on the π-system generating the σ-algebra, and they are both finite on a increasing spanning sequence of sets in the π-system. This lemma is formulated using sUnion.

theorem measure_theory.measure.ext_of_generate_from_of_Union {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} (C : set (set α)) (B : set α) :
_inst_1 = measurable_space.generate_from Cis_pi_system C(⋃ (i : ), B i) = set.univ(∀ (i : ), B i C)(∀ (i : ), μ (B i) < )(∀ (s : set α), s Cμ s = ν s)μ = ν

Two measures are equal if they are equal on the π-system generating the σ-algebra, and they are both finite on a increasing spanning sequence of sets in the π-system. This lemma is formulated using Union. finite_spanning_sets_in.ext is a reformulation of this lemma.

theorem measure_theory.measure.dirac_apply' {α : Type u_1} [measurable_space α] (a : α) {s : set α} :
is_measurable s((measure_theory.measure.dirac a) s = ⨆ (h : a s), 1)

@[simp]
theorem measure_theory.measure.dirac_apply {α : Type u_1} [measurable_space α] (a : α) {s : set α} :

theorem measure_theory.measure.dirac_apply_of_mem {α : Type u_1} [measurable_space α] {a : α} {s : set α} :

def measure_theory.measure.sum {α : Type u_1} [measurable_space α] {ι : Type u_2} :

Sum of an indexed family of measures.

Equations
@[simp]
theorem measure_theory.measure.sum_apply {α : Type u_1} [measurable_space α] {ι : Type u_2} (f : ι → measure_theory.measure α) {s : set α} :
is_measurable s((measure_theory.measure.sum f) s = ∑' (i : ι), (f i) s)

theorem measure_theory.measure.le_sum {α : Type u_1} [measurable_space α] {ι : Type u_2} (μ : ι → measure_theory.measure α) (i : ι) :

theorem measure_theory.measure.restrict_Union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {s : ι → set α} :
pairwise (disjoint on s)(∀ (i : ι), is_measurable (s i))μ.restrict (⋃ (i : ι), s i) = measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))

theorem measure_theory.measure.restrict_Union_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {s : ι → set α} :
μ.restrict (⋃ (i : ι), s i) measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))

@[simp]
theorem measure_theory.measure.sum_cond {α : Type u_1} [measurable_space α] (μ ν : measure_theory.measure α) :
measure_theory.measure.sum (λ (b : bool), cond b μ ν) = μ + ν

@[simp]
theorem measure_theory.measure.restrict_sum {α : Type u_1} [measurable_space α] {ι : Type u_2} (μ : ι → measure_theory.measure α) {s : set α} :

theorem measure_theory.measure.count_apply {α : Type u_1} [measurable_space α] {s : set α} :

count measure evaluates to infinity at infinite sets.

The almost everywhere filter

The “almost everywhere” filter of co-null sets.

Equations

The filter of sets s such that sᶜ has finite measure.

Equations
theorem measure_theory.measure.mem_cofinite {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :

theorem measure_theory.measure.eventually_cofinite {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : α → Prop} :
(∀ᶠ (x : α) in μ.cofinite, p x) μ {x : α | ¬p x} <

theorem measure_theory.mem_ae_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
s μ.ae μ s = 0

theorem measure_theory.ae_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : α → Prop} :
(∀ᵐ (a : α) ∂μ, p a) μ {a : α | ¬p a} = 0

theorem measure_theory.compl_mem_ae_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
s μ.ae μ s = 0

theorem measure_theory.measure_zero_iff_ae_nmem {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
μ s = 0 ∀ᵐ (a : α) ∂μ, a s

@[simp]
theorem measure_theory.ae_eq_bot {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :
μ.ae = μ = 0

theorem measure_theory.ae_of_all {α : Type u_1} [measurable_space α] {p : α → Prop} (μ : measure_theory.measure α) :
(∀ (a : α), p a)(∀ᵐ (a : α) ∂μ, p a)

theorem measure_theory.ae_mono {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} :
μ νμ.ae ν.ae

theorem measure_theory.ae_all_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} [encodable ι] {p : α → ι → Prop} :
(∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i

theorem measure_theory.ae_ball_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Type u_2} {S : set ι} (hS : S.countable) {p : α → Π (i : ι), i S → Prop} :
(∀ᵐ (x : α) ∂μ, ∀ (i : ι) (H : i S), p x i H) ∀ (i : ι) (H : i S), ∀ᵐ (x : α) ∂μ, p x i H

theorem measure_theory.ae_eq_refl {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} (f : α → β) :
f =ᵐ[μ] f

theorem measure_theory.ae_eq_symm {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {f g : α → β} :
f =ᵐ[μ] gg =ᵐ[μ] f

theorem measure_theory.ae_eq_trans {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {f g h : α → β} :
f =ᵐ[μ] gg =ᵐ[μ] hf =ᵐ[μ] h

theorem measure_theory.ae_eq_empty {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
s =ᵐ[μ] μ s = 0

theorem measure_theory.ae_le_set {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s ≤ᵐ[μ] t μ (s \ t) = 0

theorem measure_theory.union_ae_eq_right {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s t =ᵐ[μ] t μ (s \ t) = 0

theorem measure_theory.diff_ae_eq_self {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s \ t =ᵐ[μ] s μ (s t) = 0

theorem measure_theory.mem_ae_map_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] {f : α → β} (hf : measurable f) {s : set β} :

theorem measure_theory.ae_map_iff {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [measurable_space β] {f : α → β} (hf : measurable f) {p : β → Prop} :
is_measurable {x : β | p x}((∀ᵐ (y : β) ∂(measure_theory.measure.map f) μ, p y) ∀ᵐ (x : α) ∂μ, p (f x))

theorem measure_theory.ae_restrict_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} {p : α → Prop} :
is_measurable {x : α | p x}((∀ᵐ (x : α) ∂μ.restrict s, p x) ∀ᵐ (x : α) ∂μ, x sp x)

theorem measure_theory.ae_smul_measure {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : α → Prop} (h : ∀ᵐ (x : α) ∂μ, p x) (c : ennreal) :
∀ᵐ (x : α) ∂c μ, p x

theorem measure_theory.ae_add_measure_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : α → Prop} {ν : measure_theory.measure α} :
(∀ᵐ (x : α) ∂μ + ν, p x) (∀ᵐ (x : α) ∂μ, p x) ∀ᵐ (x : α) ∂ν, p x

@[simp]
theorem measure_theory.ae_restrict_eq {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
is_measurable s(μ.restrict s).ae = μ.ae 𝓟 s

@[simp]
theorem measure_theory.ae_restrict_eq_bot {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(μ.restrict s).ae = μ s = 0

@[simp]
theorem measure_theory.ae_restrict_ne_bot {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(μ.restrict s).ae.ne_bot 0 < μ s

theorem measure_theory.ae_eventually_not_mem {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(∀ (i : ), is_measurable (s i))(∑' (i : ), μ (s i)) (∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ) in filter.at_top, x s n)

A version of the Borel-Cantelli lemma: if sᵢ is a sequence of measurable sets such that ∑ μ sᵢ exists, then for almost all x, x does not belong to almost all sᵢ.

theorem measure_theory.mem_dirac_ae_iff {α : Type u_1} [measurable_space α] {a : α} {s : set α} :

theorem measure_theory.eventually_dirac {α : Type u_1} [measurable_space α] {a : α} {p : α → Prop} :
is_measurable {x : α | p x}((∀ᵐ (x : α) ∂measure_theory.measure.dirac a, p x) p a)

theorem measure_theory.eventually_eq_dirac {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] [measurable_singleton_class β] {a : α} {f : α → β} :

theorem measure_theory.eventually_eq_dirac' {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_singleton_class α] {a : α} (f : α → β) :

theorem measure_theory.measure_diff_of_ae_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s ≤ᵐ[μ] tμ (s \ t) = 0

theorem measure_theory.measure_mono_ae {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s ≤ᵐ[μ] tμ s μ t

If s ⊆ t modulo a set of measure 0, then μ s ≤ μ t.

theorem measure_theory.measure_congr {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s =ᵐ[μ] tμ s = μ t

If two sets are equal modulo a set of measure zero, then μ s = μ t.

theorem measure_theory.restrict_mono_ae {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s ≤ᵐ[μ] tμ.restrict s μ.restrict t

theorem measure_theory.restrict_congr_set {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
s =ᵐ[μ] tμ.restrict s = μ.restrict t

@[class]
structure measure_theory.probability_measure {α : Type u_1} [measurable_space α] :

A measure μ is called a probability measure if μ univ = 1.

Instances
@[class]
structure measure_theory.finite_measure {α : Type u_1} [measurable_space α] :

A measure μ is called finite if μ univ < ⊤.

Instances
@[instance]

@[class]
structure measure_theory.has_no_atoms {α : Type u_1} [measurable_space α] :
  • measure_singleton : ∀ (x : α), μ {x} = 0

Measure μ has no atoms if the measure of each singleton is zero.

NB: Wikipedia assumes that for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0, the converse is not true.

Instances
theorem measure_theory.measure.le_of_add_le_add_left {α : Type u_1} [measurable_space α] {μ ν₁ ν₂ : measure_theory.measure α} [measure_theory.finite_measure μ] :
μ + ν₁ μ + ν₂ν₁ ν₂

le_of_add_le_add_left is normally applicable to ordered_cancel_add_comm_monoid, but it holds for measures with the additional assumption that μ is finite.

theorem measure_theory.measure_finite {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} [measure_theory.has_no_atoms μ] {s : set α} :
s.finiteμ s = 0

theorem measure_theory.insert_ae_eq_self {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} [measure_theory.has_no_atoms μ] (a : α) (s : set α) :
insert a s =ᵐ[μ] s

A measure is called finite at filter f if it is finite at some set s ∈ f. Equivalently, it is eventually finite at s in f.lift' powerset.

Equations
@[nolint]
structure measure_theory.measure.finite_spanning_sets_in {α : Type u_1} [measurable_space α] :
measure_theory.measure αset (set α)Type u_1

μ has finite spanning sets in C if there is a countable sequence of sets in C that have finite measures. This structure is a type, which is useful if we want to record extra properties about the sets, such as that they are monotone. sigma_finite is defined in terms of this: μ is σ-finite if there exists a sequence of finite spanning sets in the collection of all measurable sets.

@[class]
def measure_theory.sigma_finite {α : Type u_1} [measurable_space α] :

A measure μ is called σ-finite if there is a countable collection of sets { A i | i ∈ ℕ } such that μ (A i) < ⊤ and ⋃ i, A i = s.

Equations
Instances

If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.

Equations

A noncomputable way to get a monotone collection of sets that span univ and have finite measure using classical.some. This definition satisfies monotonicity in addition to all other properties in sigma_finite.

Equations

If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.

Equations

If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.

theorem measure_theory.measure.finite_spanning_sets_in.ext {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {C : set (set α)} :
_inst_1 = measurable_space.generate_from Cis_pi_system Cμ.finite_spanning_sets_in C(∀ (s : set α), s Cμ s = ν s)μ = ν

An extensionality for measures. It is ext_of_generate_from_of_Union formulated in terms of finite_spanning_sets_in.

@[instance]

Every finite measure is σ-finite.

@[instance]

@[class]

A measure is called locally finite if it is finite in some neighborhood of each point.

Instances
theorem measure_theory.ext_of_generate_finite {α : Type u_1} [measurable_space α] (C : set (set α)) (hA : _inst_1 = measurable_space.generate_from C) (hC : is_pi_system C) {μ ν : measure_theory.measure α} [measure_theory.finite_measure μ] [measure_theory.finite_measure ν] :
(∀ (s : set α), s Cμ s = ν s)μ set.univ = ν set.univμ = ν

Two finite measures are equal if they are equal on the π-system generating the σ-algebra (and univ).

theorem measure_theory.measure.finite_at_filter.mono {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {f g : filter α} :
f gμ νν.finite_at_filter gμ.finite_at_filter f

theorem measure_theory.measure.finite_at_filter.eventually {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f : filter α} :
μ.finite_at_filter f(∀ᶠ (s : set α) in f.lift' set.powerset, μ s < )

@[simp]

Subtraction of measures

@[instance]

The measure μ - ν is defined to be the least measure τ such that μ ≤ τ + ν. It is the equivalent of (μ - ν) ⊔ 0 if μ and ν were signed measures. Compare with ennreal.has_sub. Specifically, note that if you have α = {1,2}, and μ {1} = 2, μ {2} = 0, and ν {2} = 2, ν {1} = 0, then (μ - ν) {1, 2} = 2. However, if μ ≤ ν, and ν univ ≠ ⊤, then (μ - ν) + ν = μ.

Equations
theorem measure_theory.measure.sub_def {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} :
μ - ν = Inf {d : measure_theory.measure α | μ d + ν}

theorem measure_theory.measure.sub_eq_zero_of_le {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} :
μ νμ - ν = 0

theorem measure_theory.measure.sub_apply {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} {s : set α} [measure_theory.finite_measure ν] :
is_measurable sν μ- ν) s = μ s - ν s

This application lemma only works in special circumstances. Given knowledge of when μ ≤ ν and ν ≤ μ, a more general application lemma can be written.

theorem measure_theory.measure.sub_add_cancel_of_le {α : Type u_1} [measurable_space α] {μ ν : measure_theory.measure α} [measure_theory.finite_measure ν] :
ν μμ - ν + ν = μ

@[class]
def measure_theory.measure.is_complete {α : Type u_1} {_x : measurable_space α} :

A measure is complete if every null set is also measurable. A null set is a subset of a measurable set with measure 0. Since every measure is defined as a special case of an outer measure, we can more simply state that a set s is null if μ s = 0.

Equations
Instances
def is_null_measurable {α : Type u_1} [measurable_space α] :
measure_theory.measure αset α → Prop

A set is null measurable if it is the union of a null set and a measurable set.

Equations
theorem is_null_measurable_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
is_null_measurable μ s ∃ (t : set α), t s is_measurable t μ (s \ t) = 0

theorem is_null_measurable_measure_eq {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} :
t sμ (s \ t) = 0μ s = μ t

theorem is_null_measurable.union_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s z : set α} :
is_null_measurable μ sμ z = 0is_null_measurable μ (s z)

theorem null_is_null_measurable {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {z : set α} :
μ z = 0is_null_measurable μ z

theorem is_null_measurable.Union_nat {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
(∀ (i : ), is_null_measurable μ (s i))is_null_measurable μ (set.Union s)

theorem is_measurable.diff_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s z : set α} :
is_measurable sμ z = 0is_null_measurable μ (s \ z)

theorem is_null_measurable.diff_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s z : set α} :
is_null_measurable μ sμ z = 0is_null_measurable μ (s \ z)

The measurable space of all null measurable sets.

Equations

Given a measure we can complete it to a (complete) measure on all null measurable sets.

Equations
@[instance]

@[class]
structure measure_theory.measure_space  :
Type u_1Type u_1

A measure space is a measurable space equipped with a measure, referred to as volume.

Instances

The tactic exact volume, to be used in optional (auto_param) arguments.

theorem is_compact.finite_measure_of_nhds_within {α : Type u_1} [topological_space α] [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
is_compact s(∀ (a : α), a sμ.finite_at_filter (𝓝[s] a))μ s <

theorem is_compact.measure_zero_of_nhds_within {α : Type u_1} [topological_space α] [measurable_space α] {μ : measure_theory.measure α} {s : set α} :
is_compact s(∀ (a : α), a s(∃ (t : set α) (H : t 𝓝[s] a), μ t = 0))μ s = 0