mathlib3 documentation

measure_theory.measure.measure_space_def

Measure spaces #

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

This file defines measure spaces, the almost-everywhere filter and ae_measurable functions. See measure_theory.measure_space for their properties and for extended documentation.

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

μ ∅ = 0;
μ is countably additive. This means that the measure of a countable union of pairwise disjoint sets is equal to the sum of the measures 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, an outer 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∞.

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.

See the documentation of measure_theory.measure_space for ways to construct measures and proving that two measure are equal.

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

This file does not import measure_theory.measurable_space, but only measurable_space_def.

References #

Tags #

measure, almost everywhere, measure space

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

Type u_6

to_outer_measure : measure_theory.outer_measure α
m_Union : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), measurable_set (f i)) → pairwise (disjoint on f) → self.to_outer_measure.measure_of (⋃ (i : ℕ), f i) = ∑' (i : ℕ), self.to_outer_measure.measure_of (f i)
trimmed : self.to_outer_measure.trim = self.to_outer_measure

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.

Instances for measure_theory.measure

@[protected, instance]

def measure_theory.measure.has_coe_to_fun {α : Type u_1} [measurable_space α] :

has_coe_to_fun (measure_theory.measure α) (λ (_x : measure_theory.measure α), set α → ennreal)

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

measure_theory.measure.has_coe_to_fun = {coe := λ (m : measure_theory.measure α), ⇑(m.to_outer_measure)}

General facts about measures #

noncomputable def measure_theory.measure.of_measurable {α : Type u_1} [measurable_space α] (m : Π (s : set α), measurable_set s → ennreal) (m0 : m ∅ measurable_set.empty = 0) (mU : ∀ ⦃f : ℕ → set α⦄ (h : ∀ (i : ℕ), measurable_set (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

measure_theory.measure.of_measurable m m0 mU = {to_outer_measure := {measure_of := (measure_theory.induced_outer_measure m measurable_set.empty m0).measure_of, empty := _, mono := _, Union_nat := _}, m_Union := _, trimmed := _}

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

⇑(measure_theory.measure.of_measurable m m0 mU) s = m s hs

theorem measure_theory.measure.to_outer_measure_injective {α : Type u_1} [measurable_space α] :

function.injective measure_theory.measure.to_outer_measure

@[ext]

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

μ₁ = μ₂

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

μ₁ = μ₂ ↔ ∀ (s : set α), measurable_set s → ⇑μ₁ s = ⇑μ₂ s

@[simp]

theorem measure_theory.coe_to_outer_measure {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :

⇑(μ.to_outer_measure) = ⇑μ

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

⇑(μ.to_outer_measure) s = ⇑μ s

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

⇑μ s = ⇑(μ.to_outer_measure.trim) s

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

⇑μ s = ⨅ (t : set α) (st : s ⊆ t) (ht : measurable_set t), ⇑μ t

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

⇑μ s = ⨅ (t : {t // s ⊆ t ∧ measurable_set t}), ⇑μ ↑t

A variant of measure_eq_infi which has a single infi. This is useful when applying a lemma next that only works for non-empty infima, in which case you can use nonempty_measurable_superset.

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

⇑μ s = ⇑(measure_theory.induced_outer_measure (λ (s : set α) (_x : measurable_set s), ⇑μ s) measurable_set.empty _) s

theorem measure_theory.to_outer_measure_eq_induced_outer_measure {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :

μ.to_outer_measure = measure_theory.induced_outer_measure (λ (s : set α) (_x : measurable_set s), ⇑μ s) measurable_set.empty _

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

⇑μ s = measure_theory.extend (λ (t : set α) (ht : measurable_set t), ⇑μ t) s

@[simp]

theorem measure_theory.measure_empty {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :

theorem measure_theory.nonempty_of_measure_ne_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} (h : ⇑μ s ≠ 0) :

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

⇑μ s₁ ≤ ⇑μ s₂

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

⇑μ s₁ = 0

theorem measure_theory.measure_mono_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s₁ s₂ : set α} (h : s₁ ⊆ s₂) (h₁ : ⇑μ s₁ = ⊤) :

⇑μ s₂ = ⊤

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

∃ (t : set α), s ⊆ t ∧ measurable_set t ∧ ⇑μ t = ⇑μ s

For every set there exists a measurable superset of the same measure.

theorem measure_theory.exists_measurable_superset_forall_eq {α : Type u_1} [measurable_space α] {ι : Sort u_2} [countable ι] (μ : ι → measure_theory.measure α) (s : set α) :

∃ (t : set α), s ⊆ t ∧ measurable_set t ∧ ∀ (i : ι), ⇑(μ i) t = ⇑(μ i) s

For every set s and a countable collection of measures μ i there exists a measurable superset t ⊇ s such that each measure μ i takes the same value on s and t.

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

∃ (t : set α), s ⊆ t ∧ measurable_set t ∧ ⇑μ t = ⇑μ s ∧ ⇑ν t = ⇑ν s

theorem measure_theory.exists_measurable_superset_of_null {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s : set α} (h : ⇑μ s = 0) :

∃ (t : set α), s ⊆ t ∧ measurable_set t ∧ ⇑μ t = 0

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

(∃ (t : set α), s ⊆ t ∧ measurable_set t ∧ ⇑μ t = 0) ↔ ⇑μ s = 0

theorem measure_theory.measure_Union_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [countable β] (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) ≤ s.sum (λ (p : β), ⇑μ (f p))

theorem measure_theory.measure_Union_fintype_le {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [fintype β] (f : β → set α) :

⇑μ (⋃ (b : β), f b) ≤ finset.univ.sum (λ (p : β), ⇑μ (f p))

theorem measure_theory.measure_bUnion_lt_top {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} {s : set β} {f : β → set α} (hs : s.finite) (hfin : ∀ (i : β), i ∈ s → ⇑μ (f i) ≠ ⊤) :

⇑μ (⋃ (i : β) (H : i ∈ s), f i) < ⊤

theorem measure_theory.measure_Union_null {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [countable β] {s : β → set α} :

(∀ (i : β), ⇑μ (s i) = 0) → ⇑μ (⋃ (i : β), s i) = 0

@[simp]

theorem measure_theory.measure_Union_null_iff {α : Type u_1} {ι : Type u_5} [measurable_space α] {μ : measure_theory.measure α} [countable ι] {s : ι → set α} :

⇑μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), ⇑μ (s i) = 0

@[simp]

theorem measure_theory.measure_Union_null_iff' {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Prop} {s : ι → set α} :

⇑μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), ⇑μ (s i) = 0

A version of measure_Union_null_iff for unions indexed by Props TODO: in the long run it would be better to combine this with measure_Union_null_iff by generalising to Sort.

theorem measure_theory.measure_bUnion_null_iff {α : Type u_1} {ι : Type u_5} [measurable_space α] {μ : measure_theory.measure α} {s : set ι} (hs : s.countable) {t : ι → set α} :

⇑μ (⋃ (i : ι) (H : i ∈ s), t i) = 0 ↔ ∀ (i : ι), i ∈ s → ⇑μ (t i) = 0

theorem measure_theory.measure_sUnion_null_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {S : set (set α)} (hS : S.countable) :

⇑μ (⋃₀ S) = 0 ↔ ∀ (s : set α), s ∈ S → ⇑μ s = 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

@[simp]

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_lt_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (hs : ⇑μ s < ⊤) (ht : ⇑μ t < ⊤) :

⇑μ (s ∪ t) < ⊤

@[simp]

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

⇑μ (s ∪ t) < ⊤ ↔ ⇑μ s < ⊤ ∧ ⇑μ t < ⊤

theorem measure_theory.measure_union_ne_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (hs : ⇑μ s ≠ ⊤) (ht : ⇑μ t ≠ ⊤) :

⇑μ (s ∪ t) ≠ ⊤

@[simp]

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

⇑μ (s ∪ t) = ⊤ ↔ ⇑μ s = ⊤ ∨ ⇑μ t = ⊤

theorem measure_theory.exists_measure_pos_of_not_measure_Union_null {α : Type u_1} {β : Type u_2} [measurable_space α] {μ : measure_theory.measure α} [countable β] {s : β → set α} (hs : ⇑μ (⋃ (n : β), s n) ≠ 0) :

∃ (n : β), 0 < ⇑μ (s n)

theorem measure_theory.measure_inter_lt_top_of_left_ne_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (hs_finite : ⇑μ s ≠ ⊤) :

⇑μ (s ∩ t) < ⊤

theorem measure_theory.measure_inter_lt_top_of_right_ne_top {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (ht_finite : ⇑μ t ≠ ⊤) :

⇑μ (s ∩ t) < ⊤

theorem measure_theory.measure_inter_null_of_null_right {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} (S : set α) {T : set α} (h : ⇑μ T = 0) :

⇑μ (S ∩ T) = 0

theorem measure_theory.measure_inter_null_of_null_left {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {S : set α} (T : set α) (h : ⇑μ S = 0) :

⇑μ (S ∩ T) = 0

The almost everywhere filter #

def measure_theory.measure.ae {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) :

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

Equations

μ.ae = {sets := {s : set α | ⇑μ sᶜ = 0}, univ_sets := _, sets_of_superset := _, inter_sets := _}

Instances for measure_theory.measure.ae

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.frequently_ae_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {p : α → Prop} :

(∃ᵐ (a : α) ∂μ, p a) ↔ ⇑μ {a : α | p a} ≠ 0

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

(∃ᵐ (a : α) ∂μ, a ∈ s) ↔ ⇑μ 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

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

(∀ (a : α), p a) → (∀ᵐ (a : α) ∂μ, p a)

@[protected, instance]

def measure_theory.measure.ae.countable_Inter_filter {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} :

countable_Inter_filter μ.ae

theorem measure_theory.ae_all_iff {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {ι : Sort u_2} [countable ι] {p : α → ι → Prop} :

(∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i

theorem measure_theory.ae_ball_iff {α : Type u_1} {ι : Type u_5} [measurable_space α] {μ : measure_theory.measure α} {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_4} [measurable_space α] {μ : measure_theory.measure α} (f : α → δ) :

f =ᵐ[μ] f

theorem measure_theory.ae_eq_symm {α : Type u_1} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} {f g : α → δ} (h : f =ᵐ[μ] g) :

g =ᵐ[μ] f

theorem measure_theory.ae_eq_trans {α : Type u_1} {δ : Type u_4} [measurable_space α] {μ : measure_theory.measure α} {f g h : α → δ} (h₁ : f =ᵐ[μ] g) (h₂ : g =ᵐ[μ] h) :

f =ᵐ[μ] h

theorem measure_theory.ae_le_of_ae_lt {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {f g : α → ennreal} (h : ∀ᵐ (x : α) ∂μ, f x < g x) :

@[simp]

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

s =ᵐ[μ] ∅ ↔ ⇑μ s = 0

@[simp]

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

s =ᵐ[μ] set.univ ↔ ⇑μ 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.ae_le_set_inter {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t s' t' : set α} (h : s ≤ᵐ[μ] t) (h' : s' ≤ᵐ[μ] t') :

s ∩ s' ≤ᵐ[μ] t ∩ t'

theorem measure_theory.ae_le_set_union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t s' t' : set α} (h : s ≤ᵐ[μ] t) (h' : s' ≤ᵐ[μ] t') :

s ∪ s' ≤ᵐ[μ] t ∪ t'

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.diff_null_ae_eq_self {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (ht : ⇑μ t = 0) :

s \ t =ᵐ[μ] s

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

s =ᵐ[μ] t ↔ ⇑μ (s \ t) = 0 ∧ ⇑μ (t \ s) = 0

@[simp]

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

⇑μ (s ∆ t) = 0 ↔ s =ᵐ[μ] t

@[simp]

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

sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t

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

sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ

theorem measure_theory.ae_eq_set_inter {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t s' t' : set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t') :

s ∩ s' =ᵐ[μ] t ∩ t'

theorem measure_theory.ae_eq_set_union {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t s' t' : set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t') :

s ∪ s' =ᵐ[μ] t ∪ t'

theorem measure_theory.union_ae_eq_univ_of_ae_eq_univ_left {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : s =ᵐ[μ] set.univ) :

s ∪ t =ᵐ[μ] set.univ

theorem measure_theory.union_ae_eq_univ_of_ae_eq_univ_right {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : t =ᵐ[μ] set.univ) :

s ∪ t =ᵐ[μ] set.univ

theorem measure_theory.union_ae_eq_right_of_ae_eq_empty {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : s =ᵐ[μ] ∅) :

s ∪ t =ᵐ[μ] t

theorem measure_theory.union_ae_eq_left_of_ae_eq_empty {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : t =ᵐ[μ] ∅) :

s ∪ t =ᵐ[μ] s

theorem measure_theory.inter_ae_eq_right_of_ae_eq_univ {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : s =ᵐ[μ] set.univ) :

s ∩ t =ᵐ[μ] t

theorem measure_theory.inter_ae_eq_left_of_ae_eq_univ {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : t =ᵐ[μ] set.univ) :

s ∩ t =ᵐ[μ] s

theorem measure_theory.inter_ae_eq_empty_of_ae_eq_empty_left {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : s =ᵐ[μ] ∅) :

s ∩ t =ᵐ[μ] ∅

theorem measure_theory.inter_ae_eq_empty_of_ae_eq_empty_right {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (h : t =ᵐ[μ] ∅) :

s ∩ t =ᵐ[μ] ∅

theorem set.mul_indicator_ae_eq_one {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {M : Type u_2} [has_one M] {f : α → M} {s : set α} :

s.mul_indicator f =ᵐ[μ] 1 ↔ ⇑μ (s ∩ function.mul_support f) = 0

theorem set.indicator_ae_eq_zero {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {M : Type u_2} [has_zero M] {f : α → M} {s : set α} :

s.indicator f =ᵐ[μ] 0 ↔ ⇑μ (s ∩ function.support f) = 0

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

⇑μ s ≤ ⇑μ t

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

theorem filter.eventually_le.measure_le {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (H : s ≤ᵐ[μ] t) :

⇑μ s ≤ ⇑μ t

Alias of measure_theory.measure_mono_ae.

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

⇑μ s = ⇑μ t

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

theorem filter.eventually_eq.measure_eq {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (H : s =ᵐ[μ] t) :

⇑μ s = ⇑μ t

Alias of measure_theory.measure_congr.

theorem measure_theory.measure_mono_null_ae {α : Type u_1} [measurable_space α] {μ : measure_theory.measure α} {s t : set α} (H : s ≤ᵐ[μ] t) (ht : ⇑μ t = 0) :

⇑μ s = 0

@[irreducible]

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

set α

A measurable set t ⊇ s such that μ t = μ s. It even satisfies μ (t ∩ u) = μ (s ∩ u) for any measurable set u if μ s ≠ ∞, see measure_to_measurable_inter. (This property holds without the assumption μ s ≠ ∞ when the space is sigma-finite, see measure_to_measurable_inter_of_sigma_finite). If s is a null measurable set, then we also have t =ᵐ[μ] s, see null_measurable_set.to_measurable_ae_eq. This notion is sometimes called a "measurable hull" in the literature.

Equations

measure_theory.to_measurable μ s = dite (∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ t =ᵐ[μ] s) (λ (h : ∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ t =ᵐ[μ] s), h.some) (λ (h : ¬∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ t =ᵐ[μ] s), dite (∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ ∀ (u : set α), measurable_set u → ⇑μ (t ∩ u) = ⇑μ (s ∩ u)) (λ (h' : ∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ ∀ (u : set α), measurable_set u → ⇑μ (t ∩ u) = ⇑μ (s ∩ u)), h'.some) (λ (h' : ¬∃ (t : set α) (H : t ⊇ s), measurable_set t ∧ ∀ (u : set α), measurable_set u → ⇑μ (t ∩ u) = ⇑μ (s ∩ u)), _.some))

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

s ⊆ measure_theory.to_measurable μ s

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

s ≤ᵐ[μ] measure_theory.to_measurable μ s

@[simp]

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

measurable_set (measure_theory.to_measurable μ s)

@[simp]

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

⇑μ (measure_theory.to_measurable μ s) = ⇑μ s

@[class]

structure measure_theory.measure_space (α : Type u_6) :

Type u_6

to_measurable_space : measurable_space α
volume : measure_theory.measure α

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

Instances of this typeclass

Instances of other typeclasses for measure_theory.measure_space

measure_theory.measure_space.has_sizeof_inst

meta def measure_theory.volume_tac :

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

Almost everywhere measurable functions #

A function is almost everywhere measurable if it coincides almost everywhere with a measurable function. We define this property, called ae_measurable f μ. It's properties are discussed in measure_theory.measure_space.

def ae_measurable {α : Type u_1} {β : Type u_2} [measurable_space β] {m : measurable_space α} (f : α → β) (μ : measure_theory.measure α . "volume_tac") :

Prop

A function is almost everywhere measurable if it coincides almost everywhere with a measurable function.

Equations

ae_measurable f μ = ∃ (g : α → β), measurable g ∧ f =ᵐ[μ] g

theorem measurable.ae_measurable {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} (h : measurable f) :

ae_measurable f μ

noncomputable def ae_measurable.mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {μ : measure_theory.measure α} (f : α → β) (h : ae_measurable f μ) :

α → β

Given an almost everywhere measurable function f, associate to it a measurable function that coincides with it almost everywhere. f is explicit in the definition to make sure that it shows in pretty-printing.

Equations

ae_measurable.mk f h = classical.some h

@[measurability]

theorem ae_measurable.measurable_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} (h : ae_measurable f μ) :

measurable (ae_measurable.mk f h)

theorem ae_measurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {f : α → β} {μ : measure_theory.measure α} (h : ae_measurable f μ) :

f =ᵐ[μ] ae_measurable.mk f h

theorem ae_measurable.congr {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {f g : α → β} {μ : measure_theory.measure α} (hf : ae_measurable f μ) (h : f =ᵐ[μ] g) :

ae_measurable g μ

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

ae_measurable f μ ↔ ae_measurable g μ

@[simp, measurability]

theorem ae_measurable_const {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {μ : measure_theory.measure α} {b : β} :

ae_measurable (λ (a : α), b) μ

@[measurability]

theorem ae_measurable_id {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :

ae_measurable id μ

@[measurability]

theorem ae_measurable_id' {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} :

ae_measurable (λ (x : α), x) μ

theorem measurable.comp_ae_measurable {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : measurable_space α} [measurable_space β] {μ : measure_theory.measure α} [measurable_space δ] {f : α → δ} {g : δ → β} (hg : measurable g) (hf : ae_measurable f μ) :

ae_measurable (g ∘ f) μ