# mathlibdocumentation

measure_theory.measure_space

# Measure spaces #

The definition of a measure and a measure space are in `measure_theory.measure_space_def`, with only a few basic properties. This file provides many more properties of these objects. This separation allows the measurability tactic to import only the file `measure_space_def`, and to be available in `measure_space` (through `measurable_space`).

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 `ℝ≥0∞`.

We introduce the following typeclasses for measures:

• `probability_measure μ`: `μ univ = 1`;
• `finite_measure μ`: `μ univ < ∞`;
• `sigma_finite μ`: there exists a countable collection of measurable sets that cover `univ` where `μ` is finite;
• `locally_finite_measure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ∞`;
• `has_no_atoms μ` : `∀ x, μ {x} = 0`; possibly should be redefined as `∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s`.

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 #

• `completion` is the completion of a measure to all null measurable sets.
• `measure.of_measurable` and `outer_measure.to_measure` are two important ways to define a measure.

## 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:

• `measure.of_measurable` is a way to define a measure by only giving its value on measurable sets and proving the properties (1) and (2) mentioned above.
• `outer_measure.to_measure` is a way of obtaining a measure from an outer measure by showing that all measurable sets in the measurable space are Carathéodory measurable.

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

• `ext`: two measures are equal if they are equal on all measurable sets.
• `ext_of_generate_from_of_Union`: two measures are equal if they are equal on a π-system generating the measurable sets, if the π-system contains a spanning increasing sequence of sets where the measures take finite value (in particular the measures are σ-finite). This is a special case of the more general `ext_of_generate_from_of_cover`
• `ext_of_generate_finite`: two finite measures are equal if they are equal on a π-system generating the measurable sets. This is a special case of `ext_of_generate_from_of_Union` using `C ∪ {univ}`, but is easier to work with.

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

## Tags #

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

@[instance]
theorem measure_theory.measure_Union {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [encodable β] {f : β → set α} (hn : pairwise (disjoint on f)) (h : ∀ (i : β), measurable_set (f i)) :
μ (⋃ (i : β), f i) = ∑' (i : β), μ (f i)
theorem measure_theory.measure_union {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ : set α} (hd : disjoint s₁ s₂) (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
μ (s₁ s₂) = μ s₁ + μ s₂
theorem measure_theory.measure_add_measure_compl {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (h : measurable_set s) :
μ s + μ s =
theorem measure_theory.measure_bUnion {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {s : set β} {f : β → set α} (hs : s.countable) (hd : s.pairwise_on (disjoint on f)) (h : ∀ (b : β), b smeasurable_set (f b)) :
μ (⋃ (b : β) (H : b s), f b) = ∑' (p : s), μ (f p)
theorem measure_theory.measure_sUnion {α : Type u_1} {μ : measure_theory.measure α} {S : set (set α)} (hs : S.countable) (hd : S.pairwise_on disjoint) (h : ∀ (s : set α), s S) :
μ (⋃₀S) = ∑' (s : S), μ s
theorem measure_theory.measure_bUnion_finset {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} {s : finset ι} {f : ι → set α} (hd : s.pairwise_on (disjoint on f)) (hm : ∀ (b : ι), b smeasurable_set (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} {μ : measure_theory.measure α} {s : set β} (hs : s.countable) {f : α → β} (hf : ∀ (y : β), y smeasurable_set (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} {μ : measure_theory.measure α} (s : finset β) {f : α → β} (hf : ∀ (y : β), y smeasurable_set (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_null' {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ : set α} (h : μ (s₁ s₂) = 0) :
μ (s₁ \ s₂) = μ s₁
theorem measure_theory.measure_diff_null {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ : set α} (h : μ s₂ = 0) :
μ (s₁ \ s₂) = μ s₁
theorem measure_theory.measure_diff {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ : set α} (h : s₂ s₁) (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) (h_fin : μ s₂ < ) :
μ (s₁ \ s₂) = μ s₁ - μ s₂
theorem measure_theory.meas_eq_meas_of_null_diff {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hst : s t) (h_nulldiff : μ (t.diff s) = 0) :
μ s = μ t
theorem measure_theory.meas_eq_meas_of_between_null_diff {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ s₃ : set α} (h12 : s₁ s₂) (h23 : s₂ s₃) (h_nulldiff : μ (s₃ \ s₁) = 0) :
μ s₁ = μ s₂ μ s₂ = μ s₃
theorem measure_theory.meas_eq_meas_smaller_of_between_null_diff {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ s₃ : set α} (h12 : s₁ s₂) (h23 : s₂ s₃) (h_nulldiff : μ (s₃.diff s₁) = 0) :
μ s₁ = μ s₂
theorem measure_theory.meas_eq_meas_larger_of_between_null_diff {α : Type u_1} {μ : measure_theory.measure α} {s₁ s₂ s₃ : set α} (h12 : s₁ s₂) (h23 : s₂ s₃) (h_nulldiff : μ (s₃.diff s₁) = 0) :
μ s₂ = μ s₃
theorem measure_theory.measure_compl {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (h₁ : measurable_set s) (h_fin : μ s < ) :
μ s = - μ s
theorem measure_theory.sum_measure_le_measure_univ {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} {s : finset ι} {t : ι → set α} (h : ∀ (i : ι), i smeasurable_set (t i)) (H : s.pairwise_on (disjoint on t)) :
∑ (i : ι) in s, μ (t i)
theorem measure_theory.tsum_measure_le_measure_univ {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} {s : ι → set α} (hs : ∀ (i : ι), measurable_set (s i)) (H : pairwise (disjoint on s)) :
∑' (i : ι), μ (s i)
theorem measure_theory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure {α : Type u_1} {ι : Type u_5} (μ : measure_theory.measure α) {s : ι → set α} (hs : ∀ (i : ι), measurable_set (s i)) (H : < ∑' (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_5} (μ : measure_theory.measure α) {s : finset ι} {t : ι → set α} (h : ∀ (i : ι), i smeasurable_set (t i)) (H : < ∑ (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_5} {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} (h : ∀ (i : ι), measurable_set (s i)) (hd : 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_5} {μ : measure_theory.measure α} {s : ι → set α} {t : set ι} (ht : t.countable) (h : ∀ (i : ι), i tmeasurable_set (s i)) (hd : 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_5} {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} (h : ∀ (i : ι), measurable_set (s i)) (hd : s) (hfin : ∃ (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} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) (ht : measurable_set t) :
μ s = μ (s t) + μ (s \ t)
theorem measure_theory.measure_union_add_inter {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) (ht : measurable_set t) :
μ (s t) + μ (s t) = μ s + μ t
theorem measure_theory.tendsto_measure_Union {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : ∀ (n : ), measurable_set (s n)) (hm : monotone s) :
(𝓝 (μ (⋃ (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} {μ : measure_theory.measure α} {s : set α} (hs : ∀ (n : ), measurable_set (s n)) (hm : ∀ ⦃n m : ⦄, n ms m s n) (hf : ∃ (i : ), μ (s i) < ) :
(𝓝 (μ (⋂ (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} {μ : measure_theory.measure α} {s : set α} (hs : ∀ (i : ), measurable_set (s i)) (hs' : ∑' (i : ), μ (s i) ) :
μ = 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} {β : Type u_2} {x : β} {t : set β} {s : set α} {μ : measure_theory.measure α} :
μ (ite (x t) s ) = t.indicator (λ (_x : β), μ s) x
def measure_theory.outer_measure.to_measure {α : Type u_1} [ms : measurable_space α] (h : ms m.caratheodory) :

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

Equations
@[simp]
@[simp]
theorem measure_theory.to_measure_apply {α : Type u_1} [ms : measurable_space α] (h : ms m.caratheodory) {s : set α} (hs : measurable_set s) :
(m.to_measure h) s = m s
theorem measure_theory.le_to_measure_apply {α : Type u_1} [ms : measurable_space α] (h : ms m.caratheodory) (s : set α) :
m s (m.to_measure h) s
@[simp]
theorem measure_theory.measure.caratheodory {α : Type u_1} {s t : set α} (μ : measure_theory.measure α) (hs : measurable_set s) :
μ (t s) + μ (t \ s) = μ t

### The `ℝ≥0∞`-module of measures #

@[instance]
def measure_theory.measure.has_zero {α : Type u_1}  :
Equations
@[simp]
theorem measure_theory.measure.zero_to_outer_measure {α : Type u_1}  :
@[simp]
theorem measure_theory.measure.coe_zero {α : Type u_1}  :
0 = 0
theorem measure_theory.measure.eq_zero_of_not_nonempty {α : Type u_1} (h : ¬) (μ : measure_theory.measure α) :
μ = 0
@[instance]
def measure_theory.measure.inhabited {α : Type u_1}  :
Equations
@[instance]
def measure_theory.measure.has_add {α : Type u_1}  :
Equations
@[simp]
theorem measure_theory.measure.add_to_outer_measure {α : Type u_1} (μ₁ μ₂ : measure_theory.measure α) :
(μ₁ + μ₂).to_outer_measure =
@[simp]
theorem measure_theory.measure.coe_add {α : Type u_1} (μ₁ μ₂ : measure_theory.measure α) :
(μ₁ + μ₂) = μ₁ + μ₂
theorem measure_theory.measure.add_apply {α : Type u_1} (μ₁ μ₂ : measure_theory.measure α) (s : set α) :
(μ₁ + μ₂) s = μ₁ s + μ₂ s
@[instance]
def measure_theory.measure.add_comm_monoid {α : Type u_1}  :
Equations
@[instance]
def measure_theory.measure.has_scalar {α : Type u_1}  :
Equations
@[simp]
theorem measure_theory.measure.coe_smul {α : Type u_1} (c : ℝ≥0∞) (μ : measure_theory.measure α) :
(c μ) = c μ
theorem measure_theory.measure.smul_apply {α : Type u_1} (c : ℝ≥0∞) (μ : measure_theory.measure α) (s : set α) :
(c μ) s = c * μ s
@[instance]
def measure_theory.measure.module {α : Type u_1}  :
Equations
@[simp]
theorem measure_theory.measure.coe_nnreal_smul {α : Type u_1} (c : ℝ≥0) (μ : measure_theory.measure α) :
(c μ) = c μ

### The complete lattice of measures #

@[instance]
def measure_theory.measure.partial_order {α : Type u_1}  :

Measures are partially ordered.

The definition of less equal here is equivalent to the definition without the measurable set condition, and this is shown by `measure.le_iff'`. It is defined this way since, to prove `μ ≤ ν`, we may simply `intros s hs` instead of rewriting followed by `intros s hs`.

Equations
theorem measure_theory.measure.le_iff {α : Type u_1} {μ₁ μ₂ : measure_theory.measure α} :
μ₁ μ₂ ∀ (s : set α), μ₁ s μ₂ s
theorem measure_theory.measure.to_outer_measure_le {α : Type u_1} {μ₁ μ₂ : measure_theory.measure α} :
μ₁ μ₂
theorem measure_theory.measure.le_iff' {α : Type u_1} {μ₁ μ₂ : measure_theory.measure α} :
μ₁ μ₂ ∀ (s : set α), μ₁ s μ₂ s
theorem measure_theory.measure.lt_iff {α : Type u_1} {μ ν : measure_theory.measure α} :
μ < ν μ ν ∃ (s : set α), μ s < ν s
theorem measure_theory.measure.lt_iff' {α : Type u_1} {μ ν : measure_theory.measure α} :
μ < ν μ ν ∃ (s : set α), μ s < ν s
@[instance]
def measure_theory.measure.covariant_add_le {α : Type u_1}  :
theorem measure_theory.measure.le_add_left {α : Type u_1} {μ ν ν' : measure_theory.measure α} (h : μ ν) :
μ ν' + ν
theorem measure_theory.measure.le_add_right {α : Type u_1} {μ ν ν' : measure_theory.measure α} (h : μ ν) :
μ ν + ν'
theorem measure_theory.measure.Inf_caratheodory {α : Type u_1} {m : set } (s : set α) (hs : measurable_set s) :
@[instance]
def measure_theory.measure.has_Inf {α : Type u_1}  :
Equations
theorem measure_theory.measure.Inf_apply {α : Type u_1} {s : set α} {m : set } (hs : measurable_set s) :
(Inf m) s =
theorem measure_theory.measure.zero_le {α : Type u_1} (μ : measure_theory.measure α) :
0 μ
theorem measure_theory.measure.nonpos_iff_eq_zero' {α : Type u_1} {μ : measure_theory.measure α} :
μ 0 μ = 0
@[simp]
theorem measure_theory.measure.measure_univ_eq_zero {α : Type u_1} {μ : measure_theory.measure α} :
= 0 μ = 0

### Pushforward and pullback #

def measure_theory.measure.lift_linear {α : Type u_1} {β : Type u_2} (hf : ∀ (μ : , _inst_2 ) :

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
@[simp]
theorem measure_theory.measure.lift_linear_apply {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (hf : ∀ (μ : , _inst_2 ) {s : set β} (hs : measurable_set s) :
theorem measure_theory.measure.le_lift_linear_apply {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (hf : ∀ (μ : , _inst_2 ) (s : set β) :
def measure_theory.measure.map {α : Type u_1} {β : Type u_2} (f : α → β) :

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} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} (hs : measurable_set s) :
μ) s = μ (f ⁻¹' s)

We can evaluate the pushforward on measurable sets. For non-measurable sets, see `measure_theory.measure.le_map_apply` and `measurable_equiv.map_apply`.

theorem measure_theory.measure.map_of_not_measurable {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : ¬) :
= 0
@[simp]
theorem measure_theory.measure.map_id {α : Type u_1} {μ : measure_theory.measure α} :
theorem measure_theory.measure.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μ : measure_theory.measure α} {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :
theorem measure_theory.measure.map_mono {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} (f : α → β) (h : μ ν) :
theorem measure_theory.measure.le_map_apply {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) (s : set β) :
μ (f ⁻¹' s) μ) s

Even if `s` is not measurable, we can bound `map f μ s` from below. See also `measurable_equiv.map_apply`.

theorem measure_theory.measure.preimage_null_of_map_null {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} (hs : μ) s = 0) :
μ (f ⁻¹' s) = 0

Even if `s` is not measurable, `map f μ s = 0` implies that `μ (f ⁻¹' s) = 0`.

theorem measure_theory.measure.tendsto_ae_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) :
μ.ae μ).ae
def measure_theory.measure.comap {α : Type u_1} {β : Type u_2} (f : α → β) :

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} {s : set α} (f : α → β) (hfi : function.injective f) (hf : ∀ (s : set α), measurable_set (f '' s)) (μ : measure_theory.measure β) (hs : measurable_set s) :
s = μ (f '' s)

### Restricting a measure #

def measure_theory.measure.restrictₗ {α : Type u_1} (s : set α) :

Restrict a measure `μ` to a set `s` as an `ℝ≥0∞`-linear map.

Equations
def measure_theory.measure.restrict {α : Type u_1} (μ : measure_theory.measure α) (s : set α) :

Restrict a measure `μ` to a set `s`.

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

If `t` is a measurable set, then the measure of `t` with respect to the restriction of the measure to `s` equals the outer measure of `t ∩ s`. An alternate version requiring that `s` be measurable instead of `t` exists as `measure.restrict_apply'`.

theorem measure_theory.measure.restrict_eq_self {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (h_meas_t : measurable_set t) (h : t s) :
(μ.restrict s) t = μ t
theorem measure_theory.measure.restrict_apply_self {α : Type u_1} {s : set α} (μ : measure_theory.measure α) (h_meas_s : measurable_set s) :
(μ.restrict s) s = μ s
theorem measure_theory.measure.restrict_apply_univ {α : Type u_1} {μ : measure_theory.measure α} (s : set α) :
theorem measure_theory.measure.le_restrict_apply {α : Type u_1} {μ : measure_theory.measure α} (s t : set α) :
μ (t s) (μ.restrict s) t
@[simp]
theorem measure_theory.measure.restrict_add {α : Type u_1} (μ ν : measure_theory.measure α) (s : set α) :
+ ν).restrict s = μ.restrict s + ν.restrict s
@[simp]
theorem measure_theory.measure.restrict_zero {α : Type u_1} (s : set α) :
0.restrict s = 0
@[simp]
theorem measure_theory.measure.restrict_smul {α : Type u_1} (c : ℝ≥0∞) (μ : measure_theory.measure α) (s : set α) :
(c μ).restrict s = c μ.restrict s
@[simp]
theorem measure_theory.measure.restrict_restrict {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) :
(μ.restrict t).restrict s = μ.restrict (s t)
theorem measure_theory.measure.restrict_comm {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) (ht : measurable_set t) :
(μ.restrict t).restrict s = (μ.restrict s).restrict t
theorem measure_theory.measure.restrict_apply_eq_zero {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (ht : measurable_set t) :
(μ.restrict s) t = 0 μ (t s) = 0
theorem measure_theory.measure.measure_inter_eq_zero_of_restrict {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (h : (μ.restrict s) t = 0) :
μ (t s) = 0
theorem measure_theory.measure.restrict_apply_eq_zero' {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) :
(μ.restrict s) t = 0 μ (t s) = 0
@[simp]
theorem measure_theory.measure.restrict_eq_zero {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
μ.restrict s = 0 μ s = 0
theorem measure_theory.measure.restrict_zero_set {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (h : μ s = 0) :
μ.restrict s = 0
@[simp]
theorem measure_theory.measure.restrict_empty {α : Type u_1} {μ : measure_theory.measure α} :
= 0
@[simp]
theorem measure_theory.measure.restrict_univ {α : Type u_1} {μ : measure_theory.measure α} :
theorem measure_theory.measure.restrict_eq_self_of_measurable_subset {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (ht : measurable_set t) (t_subset : t s) :
(μ.restrict s) t = μ t
theorem measure_theory.measure.restrict_union_apply {α : Type u_1} {μ : measure_theory.measure α} {s s' t : set α} (h : disjoint (t s) (t s')) (hs : measurable_set s) (hs' : measurable_set s') (ht : measurable_set t) :
(μ.restrict (s s')) t = (μ.restrict s) t + (μ.restrict s') t
theorem measure_theory.measure.restrict_union {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (h : t) (hs : measurable_set s) (ht : measurable_set t) :
μ.restrict (s t) = μ.restrict s + μ.restrict t
theorem measure_theory.measure.restrict_union_add_inter {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) (ht : measurable_set t) :
μ.restrict (s t) + μ.restrict (s t) = μ.restrict s + μ.restrict t
@[simp]
theorem measure_theory.measure.restrict_add_restrict_compl {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
μ.restrict s + μ.restrict s = μ
@[simp]
theorem measure_theory.measure.restrict_compl_add_restrict {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
μ.restrict s + μ.restrict s = μ
theorem measure_theory.measure.restrict_union_le {α : Type u_1} {μ : measure_theory.measure α} (s s' : set α) :
μ.restrict (s s') μ.restrict s + μ.restrict s'
theorem measure_theory.measure.restrict_Union_apply {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} (hd : pairwise (disjoint on s)) (hm : ∀ (i : ι), measurable_set (s i)) {t : set α} (ht : measurable_set t) :
(μ.restrict (⋃ (i : ι), s i)) t = ∑' (i : ι), (μ.restrict (s i)) t
theorem measure_theory.measure.restrict_Union_apply_eq_supr {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} (hm : ∀ (i : ι), measurable_set (s i)) (hd : s) {t : set α} (ht : measurable_set t) :
(μ.restrict (⋃ (i : ι), s i)) t = ⨆ (i : ι), (μ.restrict (s i)) t
theorem measure_theory.measure.restrict_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} (hs : measurable_set s) :
μ).restrict s = (μ.restrict (f ⁻¹' s))
theorem measure_theory.measure.map_comap_subtype_coe {α : Type u_1} {s : set α} (hs : measurable_set s) :
theorem measure_theory.measure.restrict_mono' {α : Type u_1} ⦃s s' : set α⦄ ⦃μ ν : measure_theory.measure α⦄ (hs : s ≤ᵐ[μ] s') (hμν : μ ν) :
μ.restrict s ν.restrict s'

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

theorem measure_theory.measure.restrict_mono {α : Type u_1} ⦃s s' : set α⦄ (hs : s s') ⦃μ ν : measure_theory.measure α⦄ (hμν : μ ν) :
μ.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} {μ : measure_theory.measure α} {s : set α} :
μ.restrict s μ
theorem measure_theory.measure.restrict_congr_meas {α : Type u_1} {μ ν : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
μ.restrict s = ν.restrict s ∀ (t : set α), t sμ t = ν t
theorem measure_theory.measure.restrict_congr_mono {α : Type u_1} {μ ν : measure_theory.measure α} {s t : set α} (hs : s t) (hm : measurable_set s) (h : μ.restrict t = ν.restrict t) :
μ.restrict s = ν.restrict s
theorem measure_theory.measure.restrict_union_congr {α : Type u_1} {μ ν : measure_theory.measure α} {s t : set α} (hsm : measurable_set s) (htm : measurable_set 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} {ι : Type u_5} {μ ν : measure_theory.measure α} {s : finset ι} {t : ι → set α} (htm : ∀ (i : ι), i smeasurable_set (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} {ι : Type u_5} {μ ν : measure_theory.measure α} [encodable ι] {s : ι → set α} (hm : ∀ (i : ι), measurable_set (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} {ι : Type u_5} {μ ν : measure_theory.measure α} {s : set ι} {t : ι → set α} (hc : s.countable) (htm : ∀ (i : ι), i smeasurable_set (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} {μ ν : measure_theory.measure α} {S : set (set α)} (hc : S.countable) (hm : ∀ (s : set α), s 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} {t : set α} {m : set } (hm : m.nonempty) (ht : measurable_set t) :
(Inf m).restrict t = Inf ((λ (μ : , μ.restrict t) '' m)

This lemma shows that `Inf` and `restrict` commute for measures.

theorem measure_theory.measure.restrict_apply' {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) :
(μ.restrict s) t = μ (t s)

If `s` is a measurable set, then the outer measure of `t` with respect to the restriction of the measure to `s` equals the outer measure of `t ∩ s`. This is an alternate version of `measure.restrict_apply`, requiring that `s` is measurable instead of `t`.

theorem measure_theory.measure.restrict_eq_self_of_subset_of_measurable {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (hs : measurable_set s) (t_subset : t s) :
(μ.restrict s) t = μ t

### Extensionality results #

theorem measure_theory.measure.ext_iff_of_Union_eq_univ {α : Type u_1} {ι : Type u_5} {μ ν : measure_theory.measure α} [encodable ι] {s : ι → set α} (hm : ∀ (i : ι), measurable_set (s i)) (hs : (⋃ (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_of_Union_eq_univ {α : Type u_1} {ι : Type u_5} {μ ν : measure_theory.measure α} [encodable ι] {s : ι → set α} (hm : ∀ (i : ι), measurable_set (s i)) (hs : (⋃ (i : ι), s i) = set.univ) :
(∀ (i : ι), μ.restrict (s i) = ν.restrict (s i))μ = ν

Alias of `ext_iff_of_Union_eq_univ`.

theorem measure_theory.measure.ext_iff_of_bUnion_eq_univ {α : Type u_1} {ι : Type u_5} {μ ν : measure_theory.measure α} {S : set ι} {s : ι → set α} (hc : S.countable) (hm : ∀ (i : ι), i Smeasurable_set (s i)) (hs : (⋃ (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_of_bUnion_eq_univ {α : Type u_1} {ι : Type u_5} {μ ν : measure_theory.measure α} {S : set ι} {s : ι → set α} (hc : S.countable) (hm : ∀ (i : ι), i Smeasurable_set (s i)) (hs : (⋃ (i : ι) (H : i S), s i) = set.univ) :
(∀ (i : ι), i Sμ.restrict (s i) = ν.restrict (s i))μ = ν

Alias of `ext_iff_of_bUnion_eq_univ`.

theorem measure_theory.measure.ext_iff_of_sUnion_eq_univ {α : Type u_1} {μ ν : measure_theory.measure α} {S : set (set α)} (hc : S.countable) (hm : ∀ (s : set α), s S) (hs : ⋃₀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_sUnion_eq_univ {α : Type u_1} {μ ν : measure_theory.measure α} {S : set (set α)} (hc : S.countable) (hm : ∀ (s : set α), s S) (hs : ⋃₀S = set.univ) :
(∀ (s : set α), s Sμ.restrict s = ν.restrict s)μ = ν

Alias of `ext_iff_of_sUnion_eq_univ`.

theorem measure_theory.measure.ext_of_generate_from_of_cover {α : Type u_1} {μ ν : measure_theory.measure α} {S T : set (set α)} (h_gen : _inst_1 = ) (hc : T.countable) (h_inter : is_pi_system S) (hm : ∀ (t : set α), t T) (hU : ⋃₀T = set.univ) (htop : ∀ (t : set α), t Tμ t < ) (ST_eq : ∀ (t : set α), t T∀ (s : set α), s Sμ (s t) = ν (s t)) (T_eq : ∀ (t : set α), t Tμ t = ν t) :
μ = ν
theorem measure_theory.measure.ext_of_generate_from_of_cover_subset {α : Type u_1} {μ ν : measure_theory.measure α} {S T : set (set α)} (h_gen : _inst_1 = ) (h_inter : is_pi_system S) (h_sub : T S) (hc : T.countable) (hU : ⋃₀T = set.univ) (htop : ∀ (s : set α), s Tμ s < ) (h_eq : ∀ (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} {μ ν : measure_theory.measure α} (C : set (set α)) (B : set α) (hA : _inst_1 = ) (hC : is_pi_system C) (h1B : (⋃ (i : ), B i) = set.univ) (h2B : ∀ (i : ), B i C) (hμB : ∀ (i : ), μ (B i) < ) (h_eq : ∀ (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.

def measure_theory.measure.dirac {α : Type u_1} (a : α) :

The dirac measure.

Equations
theorem measure_theory.measure.le_dirac_apply {α : Type u_1} {s : set α} {a : α} :
s.indicator 1 a
@[simp]
theorem measure_theory.measure.dirac_apply' {α : Type u_1} {s : set α} (a : α) (hs : measurable_set s) :
= s.indicator 1 a
@[simp]
theorem measure_theory.measure.dirac_apply_of_mem {α : Type u_1} {s : set α} {a : α} (h : a s) :
@[simp]
theorem measure_theory.measure.dirac_apply {α : Type u_1} (a : α) (s : set α) :
= s.indicator 1 a
theorem measure_theory.measure.map_dirac {α : Type u_1} {β : Type u_2} {f : α → β} (hf : measurable f) (a : α) :
def measure_theory.measure.sum {α : Type u_1} {ι : Type u_5} (f : ι → ) :

Sum of an indexed family of measures.

Equations
theorem measure_theory.measure.le_sum_apply {α : Type u_1} {ι : Type u_5} (f : ι → ) (s : set α) :
∑' (i : ι), (f i) s
@[simp]
theorem measure_theory.measure.sum_apply {α : Type u_1} {ι : Type u_5} (f : ι → ) {s : set α} (hs : measurable_set s) :
= ∑' (i : ι), (f i) s
theorem measure_theory.measure.le_sum {α : Type u_1} {ι : Type u_5} (μ : ι → ) (i : ι) :
theorem measure_theory.measure.restrict_Union {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} (hd : pairwise (disjoint on s)) (hm : ∀ (i : ι), measurable_set (s i)) :
μ.restrict (⋃ (i : ι), s i) = measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))
theorem measure_theory.measure.restrict_Union_le {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} [encodable ι] {s : ι → set α} :
μ.restrict (⋃ (i : ι), s i) measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))
@[simp]
theorem measure_theory.measure.sum_bool {α : Type u_1} (f : bool) :
= f tt + f ff
@[simp]
theorem measure_theory.measure.sum_cond {α : Type u_1} (μ ν : measure_theory.measure α) :
measure_theory.measure.sum (λ (b : bool), cond b μ ν) = μ + ν
@[simp]
theorem measure_theory.measure.restrict_sum {α : Type u_1} {ι : Type u_5} (μ : ι → ) {s : set α} (hs : measurable_set s) :
= measure_theory.measure.sum (λ (i : ι), (μ i).restrict s)
def measure_theory.measure.count {α : Type u_1}  :

Counting measure on any measurable space.

Equations
theorem measure_theory.measure.le_count_apply {α : Type u_1} {s : set α} :
∑' (i : s), 1
theorem measure_theory.measure.count_apply {α : Type u_1} {s : set α} (hs : measurable_set s) :
= ∑' (i : s), 1
@[simp]
theorem measure_theory.measure.count_apply_finset {α : Type u_1} (s : finset α) :
theorem measure_theory.measure.count_apply_finite {α : Type u_1} (s : set α) (hs : s.finite) :
theorem measure_theory.measure.count_apply_infinite {α : Type u_1} {s : set α} (hs : s.infinite) :

`count` measure evaluates to infinity at infinite sets.

@[simp]
theorem measure_theory.measure.count_apply_eq_top {α : Type u_1} {s : set α}  :
@[simp]
theorem measure_theory.measure.count_apply_lt_top {α : Type u_1} {s : set α}  :

### Absolute continuity #

def measure_theory.measure.absolutely_continuous {α : Type u_1} (μ ν : measure_theory.measure α) :
Prop

We say that `μ` is absolutely continuous with respect to `ν`, or that `μ` is dominated by `ν`, if `ν(A) = 0` implies that `μ(A) = 0`.

Equations
theorem measure_theory.measure.absolutely_continuous_of_le {α : Type u_1} {μ ν : measure_theory.measure α} (h : μ ν) :
μ ν
theorem has_le.le.absolutely_continuous {α : Type u_1} {μ ν : measure_theory.measure α} (h : μ ν) :
μ ν

Alias of `absolutely_continuous_of_le`.

theorem measure_theory.measure.absolutely_continuous_of_eq {α : Type u_1} {μ ν : measure_theory.measure α} (h : μ = ν) :
μ ν
theorem eq.absolutely_continuous {α : Type u_1} {μ ν : measure_theory.measure α} (h : μ = ν) :
μ ν

Alias of `absolutely_continuous_of_eq`.

theorem measure_theory.measure.absolutely_continuous.mk {α : Type u_1} {μ ν : measure_theory.measure α} (h : ∀ ⦃s : set α⦄, ν s = 0μ s = 0) :
μ ν
theorem measure_theory.measure.absolutely_continuous.trans {α : Type u_1} {μ₁ μ₂ μ₃ : measure_theory.measure α} (h1 : μ₁ μ₂) (h2 : μ₂ μ₃) :
μ₁ μ₃
theorem measure_theory.measure.absolutely_continuous.map {α : Type u_1} {β : Type u_2} {μ ν : measure_theory.measure α} (h : μ ν) (f : α → β) :
theorem has_le.le.absolutely_continuous_of_ae {α : Type u_1} {μ ν : measure_theory.measure α} :
μ.ae ν.aeμ ν

Alias of `ae_le_iff_absolutely_continuous`.

theorem measure_theory.measure.absolutely_continuous.ae_le {α : Type u_1} {μ ν : measure_theory.measure α} :
μ νμ.ae ν.ae

Alias of `ae_le_iff_absolutely_continuous`.

theorem ae_mono' {α : Type u_1} {μ ν : measure_theory.measure α} :
μ νμ.ae ν.ae

Alias of `absolutely_continuous.ae_le`.

theorem measure_theory.measure.absolutely_continuous.ae_eq {α : Type u_1} {δ : Type u_4} {μ ν : measure_theory.measure α} (h : μ ν) {f g : α → δ} (h' : f =ᵐ[ν] g) :
f =ᵐ[μ] g

### Quasi measure preserving maps (a.k.a. non-singular maps) #

structure measure_theory.measure.quasi_measure_preserving {α : Type u_1} {β : Type u_2} (f : α → β) (μa : . "volume_tac") (μb : . "volume_tac") :
Prop
• measurable :
• absolutely_continuous : μb

A map `f : α → β` is said to be quasi measure preserving (a.k.a. non-singular) w.r.t. measures `μa` and `μb` if it is measurable and `μb s = 0` implies `μa (f ⁻¹' s) = 0`.

theorem measure_theory.measure.quasi_measure_preserving.mono_left {α : Type u_1} {β : Type u_2} {μa μa' : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (h : μb) (ha : μa' μa) :
theorem measure_theory.measure.quasi_measure_preserving.mono_right {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb μb' : measure_theory.measure β} {f : α → β} (h : μb) (ha : μb μb') :
theorem measure_theory.measure.quasi_measure_preserving.mono {α : Type u_1} {β : Type u_2} {μa μa' : measure_theory.measure α} {μb μb' : measure_theory.measure β} {f : α → β} (ha : μa' μa) (hb : μb μb') (h : μb) :
theorem measure_theory.measure.quasi_measure_preserving.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {μc : measure_theory.measure γ} {g : β → γ} {f : α → β} (hg : μc) (hf : μb) :
μc
theorem measure_theory.measure.quasi_measure_preserving.iterate {α : Type u_1} {μa : measure_theory.measure α} {f : α → α} (hf : μa) (n : ) :
theorem measure_theory.measure.quasi_measure_preserving.ae_map_le {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (h : μb) :
μa).ae μb.ae
theorem measure_theory.measure.quasi_measure_preserving.tendsto_ae {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (h : μb) :
μa.ae μb.ae
theorem measure_theory.measure.quasi_measure_preserving.ae {α : Type u_1} {β : Type u_2} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (h : μb) {p : β → Prop} (hg : ∀ᵐ (x : β) ∂μb, p x) :
∀ᵐ (x : α) ∂μa, p (f x)
theorem measure_theory.measure.quasi_measure_preserving.ae_eq {α : Type u_1} {β : Type u_2} {δ : Type u_4} {μa : measure_theory.measure α} {μb : measure_theory.measure β} {f : α → β} (h : μb) {g₁ g₂ : β → δ} (hg : g₁ =ᵐ[μb] g₂) :
g₁ f =ᵐ[μa] g₂ f

### The `cofinite` filter #

def measure_theory.measure.cofinite {α : Type u_1} (μ : measure_theory.measure α) :

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

Equations
theorem measure_theory.measure.mem_cofinite {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
theorem measure_theory.measure.compl_mem_cofinite {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
theorem measure_theory.measure.eventually_cofinite {α : Type u_1} {μ : measure_theory.measure α} {p : α → Prop} :
(∀ᶠ (x : α) in μ.cofinite, p x) μ {x : α | ¬p x} <
@[simp]
theorem measure_theory.ae_eq_bot {α : Type u_1} {μ : measure_theory.measure α} :
μ.ae = μ = 0
@[simp]
theorem measure_theory.ae_ne_bot {α : Type u_1} {μ : measure_theory.measure α} :
μ.ae.ne_bot μ 0
@[simp]
theorem measure_theory.ae_zero {α : Type u_1}  :
0.ae =
theorem measure_theory.ae_mono {α : Type u_1} {μ ν : measure_theory.measure α} (h : μ ν) :
μ.ae ν.ae
theorem measure_theory.mem_ae_map_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} (hs : measurable_set s) :
s μ).ae f ⁻¹' s μ.ae
theorem measure_theory.mem_ae_of_mem_ae_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {s : set β} (hs : s μ).ae) :
f ⁻¹' s μ.ae
theorem measure_theory.ae_map_iff {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {p : β → Prop} (hp : measurable_set {x : β | p x}) :
(∀ᵐ (y : β) ∂, p y) ∀ᵐ (x : α) ∂μ, p (f x)
theorem measure_theory.ae_of_ae_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {f : α → β} (hf : measurable f) {p : β → Prop} (h : ∀ᵐ (y : β) ∂, p y) :
∀ᵐ (x : α) ∂μ, p (f x)
theorem measure_theory.ae_map_mem_range {α : Type u_1} {β : Type u_2} (f : α → β) (hf : measurable_set (set.range f)) (μ : measure_theory.measure α) :
∀ᵐ (x : β) ∂, x
theorem measure_theory.ae_restrict_iff {α : Type u_1} {μ : measure_theory.measure α} {s : set α} {p : α → Prop} (hp : measurable_set {x : α | p x}) :
(∀ᵐ (x : α) ∂μ.restrict s, p x) ∀ᵐ (x : α) ∂μ, x sp x
theorem measure_theory.ae_imp_of_ae_restrict {α : Type u_1} {μ : measure_theory.measure α} {s : set α} {p : α → Prop} (h : ∀ᵐ (x : α) ∂μ.restrict s, p x) :
∀ᵐ (x : α) ∂μ, x sp x
theorem measure_theory.ae_restrict_iff' {α : Type u_1} {μ : measure_theory.measure α} {s : set α} {p : α → Prop} (hs : measurable_set s) :
(∀ᵐ (x : α) ∂μ.restrict s, p x) ∀ᵐ (x : α) ∂μ, x sp x
theorem measure_theory.ae_restrict_mem {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
∀ᵐ (x : α) ∂μ.restrict s, x s
theorem measure_theory.ae_restrict_of_ae {α : Type u_1} {μ : measure_theory.measure α} {s : set α} {p : α → Prop} (h : ∀ᵐ (x : α) ∂μ, p x) :
∀ᵐ (x : α) ∂μ.restrict s, p x
theorem measure_theory.ae_restrict_of_ae_restrict_of_subset {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} {p : α → Prop} (hst : s t) (h : ∀ᵐ (x : α) ∂μ.restrict t, p x) :
∀ᵐ (x : α) ∂μ.restrict s, p x
theorem measure_theory.ae_smul_measure {α : Type u_1} {μ : measure_theory.measure α} {p : α → Prop} (h : ∀ᵐ (x : α) ∂μ, p x) (c : ℝ≥0∞) :
∀ᵐ (x : α) ∂c μ, p x
theorem measure_theory.ae_smul_measure_iff {α : Type u_1} {μ : measure_theory.measure α} {p : α → Prop} {c : ℝ≥0∞} (hc : c 0) :
(∀ᵐ (x : α) ∂c μ, p x) ∀ᵐ (x : α) ∂μ, p x
theorem measure_theory.ae_add_measure_iff {α : Type u_1} {μ : measure_theory.measure α} {p : α → Prop} {ν : measure_theory.measure α} :
(∀ᵐ (x : α) ∂μ + ν, p x) (∀ᵐ (x : α) ∂μ, p x) ∀ᵐ (x : α) ∂ν, p x
theorem measure_theory.ae_eq_comp' {α : Type u_1} {β : Type u_2} {δ : Type u_4} {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → β} {g g' : β → δ} (hf : measurable f) (h : g =ᵐ[ν] g') (h2 : ν) :
g f =ᵐ[μ] g' f
theorem measure_theory.ae_eq_comp {α : Type u_1} {β : Type u_2} {δ : Type u_4} {μ : measure_theory.measure α} {f : α → β} {g g' : β → δ} (hf : measurable f) (h : g =ᵐ[] g') :
g f =ᵐ[μ] g' f
theorem measure_theory.le_ae_restrict {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
μ.ae 𝓟 s (μ.restrict s).ae
@[simp]
theorem measure_theory.ae_restrict_eq {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
(μ.restrict s).ae = μ.ae 𝓟 s
@[simp]
theorem measure_theory.ae_restrict_eq_bot {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
(μ.restrict s).ae = μ s = 0
@[simp]
theorem measure_theory.ae_restrict_ne_bot {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
(μ.restrict s).ae.ne_bot 0 < μ s
theorem measure_theory.self_mem_ae_restrict {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
s (μ.restrict s).ae
theorem measure_theory.ae_eventually_not_mem {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : ∀ (i : ), measurable_set (s i)) (hs' : ∑' (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_ae_dirac_iff {α : Type u_1} {s : set α} {a : α} (hs : measurable_set s) :
a s
theorem measure_theory.ae_dirac_iff {α : Type u_1} {a : α} {p : α → Prop} (hp : measurable_set {x : α | p x}) :
(∀ᵐ (x : α) ∂, p x) p a
@[simp]
theorem measure_theory.ae_dirac_eq {α : Type u_1} (a : α) :
theorem measure_theory.ae_eq_dirac' {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} (hf : measurable f) :
theorem measure_theory.ae_eq_dirac {α : Type u_1} {δ : Type u_4} {a : α} (f : α → δ) :
theorem measure_theory.restrict_mono_ae {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (h : s ≤ᵐ[μ] t) :
theorem measure_theory.restrict_congr_set {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (H : s =ᵐ[μ] t) :
μ.restrict s = μ.restrict t
@[class]
structure measure_theory.finite_measure {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• measure_univ_lt_top :

A measure `μ` is called finite if `μ univ < ∞`.

Instances
@[instance]
def measure_theory.restrict.finite_measure {α : Type u_1} {s : set α} (μ : measure_theory.measure α) [hs : fact (μ s < )] :
theorem measure_theory.measure_lt_top {α : Type u_1} (μ : measure_theory.measure α) (s : set α) :
μ s <
theorem measure_theory.measure_ne_top {α : Type u_1} (μ : measure_theory.measure α) (s : set α) :
μ s

The measure of the whole space with respect to a finite measure, considered as `ℝ≥0`.

Equations
@[simp]
theorem measure_theory.coe_measure_univ_nnreal {α : Type u_1} (μ : measure_theory.measure α)  :
@[instance]
def measure_theory.finite_measure_zero {α : Type u_1}  :
@[instance]
def measure_theory.finite_measure_add {α : Type u_1} {μ ν : measure_theory.measure α}  :
@[instance]
@[simp]
theorem measure_theory.measure_univ_nnreal_zero {α : Type u_1}  :
@[simp]
theorem measure_theory.measure_univ_nnreal_pos {α : Type u_1} {μ : measure_theory.measure α} (hμ : μ 0) :
theorem measure_theory.measure.le_of_add_le_add_left {α : Type u_1} {μ ν₁ ν₂ : measure_theory.measure α} (A2 : μ + ν₁ μ + ν₂) :
ν₁ ν₂

`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.summable_measure_to_real {α : Type u_1} {μ : measure_theory.measure α} {f : set α} (hf₁ : ∀ (i : ), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) :
summable (λ (x : ), (μ (f x)).to_real)
@[class]
structure measure_theory.probability_measure {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• measure_univ : = 1

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

Instances
@[instance]
def measure_theory.measure.dirac.probability_measure {α : Type u_1} {x : α} :
@[instance]
theorem measure_theory.prob_add_prob_compl {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (h : measurable_set s) :
μ s + μ s = 1
theorem measure_theory.prob_le_one {α : Type u_1} {μ : measure_theory.measure α} {s : set α}  :
μ s 1
@[class]
structure measure_theory.has_no_atoms {α : Type u_1} (μ : measure_theory.measure α) :
Prop
• 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_subsingleton {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : s.subsingleton) :
μ s = 0
theorem set.subsingleton.measure_eq {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : s.subsingleton) :
μ s = 0

Alias of `measure_subsingleton`.

@[simp]
theorem measure_theory.measure.restrict_singleton' {α : Type u_1} {μ : measure_theory.measure α} {a : α} :
μ.restrict {a} = 0
@[instance]
def measure_theory.measure.restrict.has_no_atoms {α : Type u_1} {μ : measure_theory.measure α} (s : set α) :
theorem set.countable.measure_zero {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (h : s.countable) :
μ s = 0
theorem set.finite.measure_zero {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (h : s.finite) :
μ s = 0
theorem finset.measure_zero {α : Type u_1} {μ : measure_theory.measure α} (s : finset α) :
μ s = 0
theorem measure_theory.insert_ae_eq_self {α : Type u_1} {μ : measure_theory.measure α} (a : α) (s : set α) :
s =ᵐ[μ] s
theorem measure_theory.Iio_ae_eq_Iic {α : Type u_1} {μ : measure_theory.measure α} {a : α} :
=ᵐ[μ]
theorem measure_theory.Ioi_ae_eq_Ici {α : Type u_1} {μ : measure_theory.measure α} {a : α} :
=ᵐ[μ]
theorem measure_theory.Ioo_ae_eq_Ioc {α : Type u_1} {μ : measure_theory.measure α} {a b : α} :
b =ᵐ[μ] b
theorem measure_theory.Ioc_ae_eq_Icc {α : Type u_1} {μ : measure_theory.measure α} {a b : α} :
b =ᵐ[μ] b
theorem measure_theory.Ioo_ae_eq_Ico {α : Type u_1} {μ : measure_theory.measure α} {a b : α} :
b =ᵐ[μ] b
theorem measure_theory.Ioo_ae_eq_Icc {α : Type u_1} {μ : measure_theory.measure α} {a b : α} :
b =ᵐ[μ] b
theorem measure_theory.Ico_ae_eq_Icc {α : Type u_1} {μ : measure_theory.measure α} {a b : α} :
b =ᵐ[μ] b
theorem measure_theory.Ico_ae_eq_Ioc {α : Type u_1} {μ : measure_theory.measure α} {a b : α} :
b =ᵐ[μ] b
theorem measure_theory.ite_ae_eq_of_measure_zero {α : Type u_1} {μ : measure_theory.measure α} {γ : Type u_2} (f g : α → γ) (s : set α) (hs_zero : μ s = 0) :
(λ (x : α), ite (x s) (f x) (g x)) =ᵐ[μ] g
theorem measure_theory.ite_ae_eq_of_measure_compl_zero {α : Type u_1} {μ : measure_theory.measure α} {γ : Type u_2} (f g : α → γ) (s : set α) (hs_zero : μ s = 0) :
(λ (x : α), ite (x s) (f x) (g x)) =ᵐ[μ] f
def measure_theory.measure.finite_at_filter {α : Type u_1} (μ : measure_theory.measure α) (f : filter α) :
Prop

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
theorem measure_theory.measure.finite_at_filter.exists_mem_basis {α : Type u_1} {ι : Type u_5} {μ : measure_theory.measure α} {f : filter α} (hμ : μ.finite_at_filter f) {p : ι → Prop} {s : ι → set α} (hf : f.has_basis p s) :
∃ (i : ι) (hi : p i), μ (s i) <
@[nolint]
structure measure_theory.measure.finite_spanning_sets_in {α : Type u_1} (μ : measure_theory.measure α) (C : 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]
structure measure_theory.sigma_finite {α : Type u_1} (μ : measure_theory.measure α) :
Prop

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`.

Instances

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

Equations
def measure_theory.spanning_sets {α : Type u_1} (μ : measure_theory.measure α) (i : ) :
set α

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
theorem measure_theory.measurable_spanning_sets {α : Type u_1} (μ : measure_theory.measure α) (i : ) :
theorem measure_theory.Union_spanning_sets {α : Type u_1} (μ : measure_theory.measure α)  :
(⋃ (i : ), = set.univ
theorem measure_theory.measure.supr_restrict_spanning_sets {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) :
(⨆ (i : ), (μ.restrict s) = μ s
def measure_theory.measure.finite_spanning_sets_in.mono {α : Type u_1} {μ : measure_theory.measure α} {C D : set (set α)} (h : μ.finite_spanning_sets_in C) (hC : C D) :

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

Equations
theorem measure_theory.measure.finite_spanning_sets_in.sigma_finite {α : Type u_1} {μ : measure_theory.measure α} {C : set (set α)} (h : μ.finite_spanning_sets_in C) (hC : ∀ (s : set α), s C) :

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} {μ ν : measure_theory.measure α} {C : set (set α)} (hA : _inst_1 = ) (hC : is_pi_system C) (h : μ.finite_spanning_sets_in C) (h_eq : ∀ (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`.

theorem measure_theory.measure.sigma_finite_of_countable {α : Type u_1} {μ : measure_theory.measure α} {S : set (set α)} (hc : S.countable) (hμ : ∀ (s : set α), s Sμ s < ) (hU : ⋃₀S = set.univ) :
@[instance]

Every finite measure is σ-finite.

@[instance]
def measure_theory.restrict.sigma_finite {α : Type u_1} (μ : measure_theory.measure α) (s : set α) :
@[instance]
def measure_theory.sum.sigma_finite {α : Type u_1} {ι : Type u_2} [fintype ι] (μ : ι → ) [∀ (i : ι), ] :
@[instance]
def measure_theory.add.sigma_finite {α : Type u_1} (μ ν : measure_theory.measure α)  :
theorem measure_theory.sigma_finite.of_map {α : Type u_1} {β : Type u_2} (μ : measure_theory.measure α) {f : α → β} (hf : measurable f)  :
@[class]
structure measure_theory.locally_finite_measure {α : Type u_1} (μ : measure_theory.measure α) :
Prop

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

Instances
@[instance]
theorem measure_theory.measure.finite_at_nhds {α : Type u_1} (μ : measure_theory.measure α) (x : α) :
theorem measure_theory.measure.smul_finite {α : Type u_1} (μ : measure_theory.measure α) {c : ℝ≥0∞} (hc : c < ) :
theorem measure_theory.measure.exists_is_open_measure_lt_top {α : Type u_1} (μ : measure_theory.measure α) (x : α) :
∃ (s : set α), x s μ s <
@[instance]
theorem measure_theory.ext_on_measurable_space_of_generate_finite {α : Type u_1} (m₀ : measurable_space α) {μ ν : measure_theory.measure α} (C : set (set α)) (hμν : ∀ (s : set α), s Cμ s = ν s) {m : measurable_space α} (h : m m₀) (hA : m = ) (hC : is_pi_system C) (h_univ : = ) {s : set α} (hs : m.measurable_set' s) :
μ s = ν s

If two finite measures give the same mass to the whole space and coincide on a π-system made of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.

theorem measure_theory.ext_of_generate_finite {α : Type u_1} (C : set (set α)) (hA : _inst_1 = ) (hC : is_pi_system C) {μ ν : measure_theory.measure α} (hμν : ∀ (s : set α), s Cμ s = ν s) (h_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.filter_mono {α : Type u_1} {μ : measure_theory.measure α} {f g : filter α} (h : f g) :
@[simp]
theorem measure_theory.measure.finite_at_filter.of_inf_ae {α : Type u_1} {μ : measure_theory.measure α} {f : filter α} :
μ.finite_at_filter (f μ.ae)

Alias of `inf_ae_iff`.

theorem measure_theory.measure.finite_at_filter.filter_mono_ae {α : Type u_1} {μ : measure_theory.measure α} {f g : filter α} (h : f μ.ae g) (hg : μ.finite_at_filter g) :
theorem measure_theory.measure.finite_at_filter.measure_mono {α : Type u_1} {μ ν : measure_theory.measure α} {f : filter α} (h : μ ν) :
theorem measure_theory.measure.finite_at_filter.mono {α : Type u_1} {μ ν : measure_theory.measure α} {f g : filter α} (hf : f g) (hμ : μ ν) :
theorem measure_theory.measure.finite_at_filter.eventually {α : Type u_1} {μ : measure_theory.measure α} {f : filter α} (h : μ.finite_at_filter f) :
∀ᶠ (s : set α) in , μ s <
theorem measure_theory.measure.finite_at_filter.filter_sup {α : Type u_1} {μ : measure_theory.measure α} {f g : filter α} :
μ.finite_at_filter (f g)
theorem measure_theory.measure.finite_at_nhds_within {α : Type u_1} (μ : measure_theory.measure α) (x : α) (s : set α) :
@[simp]
theorem measure_theory.measure.finite_at_principal {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :

### Subtraction of measures #

@[instance]
def measure_theory.measure.has_sub {α : Type u_1}  :

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} {μ ν : measure_theory.measure α} :
μ - ν = Inf {d : | μ d + ν}
theorem measure_theory.measure.sub_eq_zero_of_le {α : Type u_1} {μ ν : measure_theory.measure α} (h : μ ν) :
μ - ν = 0
theorem measure_theory.measure.sub_apply {α : Type u_1} {μ ν : measure_theory.measure α} {s : set α} (h₁ : measurable_set s) (h₂ : ν μ) :
- ν) 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} {μ ν : measure_theory.measure α} (h₁ : ν μ) :
μ - ν + ν = μ
theorem measure_theory.measure.sub_le {α : Type u_1} {μ ν : measure_theory.measure α} :
μ - ν μ
theorem measure_theory.measure.restrict_sub_eq_restrict_sub_restrict {α : Type u_1} {μ ν : measure_theory.measure α} {s : set α} (h_meas_s : measurable_set s) :
- ν).restrict s = μ.restrict s - ν.restrict s
theorem measure_theory.measure.sub_apply_eq_zero_of_restrict_le_restrict {α : Type u_1} {μ ν : measure_theory.measure α} {s : set α} (h_le : μ.restrict s ν.restrict s) (h_meas_s : measurable_set s) :
- ν) s = 0
@[instance]

Interactions of measurable equivalences and measures

theorem measurable_equiv.map_apply {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (f : α ≃ᵐ β) (s : set β) :
μ) s = μ (f ⁻¹' s)

If we map a measure along a measurable equivalence, we can compute the measure on all sets (not just the measurable ones).

@[simp]
theorem measurable_equiv.map_symm_map {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} (e : α ≃ᵐ β) :
μ) = μ
@[simp]
theorem measurable_equiv.map_map_symm {α : Type u_1} {β : Type u_2} {ν : measure_theory.measure β} (e : α ≃ᵐ β) :
( ν) = ν
theorem measurable_equiv.map_measurable_equiv_injective {α : Type u_1} {β : Type u_2} (e : α ≃ᵐ β) :
theorem measurable_equiv.map_apply_eq_iff_map_symm_apply_eq {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} {ν : measure_theory.measure β} (e : α ≃ᵐ β) :
ν = μ
@[class]
structure measure_theory.measure.is_complete {α : Type u_1} {_x : measurable_space α} (μ : measure_theory.measure α) :
Prop
• out' : ∀ (s : set α), μ s = 0

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`.

Instances
theorem measure_theory.measure.is_complete_iff {α : Type u_1} {_x : measurable_space α} {μ : measure_theory.measure α} :
μ.is_complete ∀ (s : set α), μ s = 0
theorem measure_theory.measure.is_complete.out {α : Type u_1} {_x : measurable_space α} {μ : measure_theory.measure α} (h : μ.is_complete) (s : set α) :
μ s = 0
def null_measurable_set {α : Type u_1} (μ : measure_theory.measure α) (s : set α) :
Prop

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

Equations
theorem null_measurable_set_iff {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
∃ (t : set α), t s μ (s \ t) = 0
theorem null_measurable_set_measure_eq {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (st : t s) (hz : μ (s \ t) = 0) :
μ s = μ t
theorem measurable_set.null_measurable_set {α : Type u_1} {s : set α} (μ : measure_theory.measure α) (hs : measurable_set s) :
theorem null_measurable_set_of_complete {α : Type u_1} {s : set α} (μ : measure_theory.measure α) [c : μ.is_complete] :
theorem null_measurable_set.union_null {α : Type u_1} {μ : measure_theory.measure α} {s z : set α} (hs : s) (hz : μ z = 0) :
(s z)
theorem null_null_measurable_set {α : Type u_1} {μ : measure_theory.measure α} {z : set α} (hz : μ z = 0) :
theorem null_measurable_set.Union_nat {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : ∀ (i : ), (s i)) :
theorem measurable_set.diff_null {α : Type u_1} {μ : measure_theory.measure α} {s z : set α} (hs : measurable_set s) (hz : μ z = 0) :
(s \ z)
theorem null_measurable_set.diff_null {α : Type u_1} {μ : measure_theory.measure α} {s z : set α} (hs : s) (hz : μ z = 0) :
(s \ z)
theorem null_measurable_set.compl {α : Type u_1} {μ : measure_theory.measure α} {s : set α} (hs : s) :
theorem null_measurable_set_iff_ae {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
∃ (t : set α), s =ᵐ[μ] t
theorem null_measurable_set_iff_sandwich {α : Type u_1} {μ : measure_theory.measure α} {s : set α} :
∃ (t u : set α), t s s u μ (u \ t) = 0
theorem restrict_apply_of_null_measurable_set {α : Type u_1} {μ : measure_theory.measure α} {s t : set α} (ht : t) :
(μ.restrict s) t = μ (t s)
def null_measurable {α : Type u_1} (μ : measure_theory.measure α) :

The measurable space of all null measurable sets.

Equations
def completion {α : Type u_1} (μ : measure_theory.measure α) :

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

Equations
@[instance]
def completion.is_complete {α : Type u_1} (μ : measure_theory.measure α) :
theorem measurable.ae_eq {α : Type u_1} {β : Type u_2} {μ : measure_theory.measure α} [hμ : μ.is_complete] {f g : α → β} (hf : measurable f) (hfg : f =ᵐ[μ] g) :
def measure_theory.measure.trim {α : Type u_1} {m m0 : measurable_space α} (μ : measure_theory.measure α) (hm : m