Measure spaces

This file defines measure spaces, the almost-everywhere filter and ae_measurable functions. See MeasureTheory.MeasureSpace 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:

1. μ ∅ = 0;
2. μ 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∞.

Notation

TODO add this!

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 MeasureTheory.MeasureSpace for ways to construct measures and proving that two measure are equal.

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

This file does not import MeasureTheory.MeasurableSpace.Basic, but only MeasurableSpace.Defs.

References

Tags

measure, almost everywhere, measure space

structure MeasureTheory.Measure (α : Type u_6) [MeasurableSpace α] extends MeasureTheory.OuterMeasure : Type u_6

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.

• measureOf : Set α → ENNReal
• empty : ↑↑self ∅ = 0
• mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → ↑↑self s₁ ≤ ↑↑self s₂
• iUnion_nat : ∀ (s : ℕ → Set α), ↑↑self (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), ↑↑self (s i)
• m_iUnion : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑↑self (⋃ (i : ℕ), f i) = ∑' (i : ℕ), ↑↑self (f i)
• trimmed : MeasureTheory.OuterMeasure.trim ↑self = ↑self

instance MeasureTheory.Measure.instCoeFun {α : Type u_1} [MeasurableSpace α] : CoeFun (MeasureTheory.Measure α) fun (x : MeasureTheory.Measure α) => Set α → ENNReal

Measure projections for a measure space.

For measurable sets this returns the measure assigned by the measureOf 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

• MeasureTheory.Measure.instCoeFun = { coe := fun (m : MeasureTheory.Measure α) => ↑↑m }

General facts about measures

def MeasureTheory.Measure.ofMeasurable {α : Type u_1} [MeasurableSpace α] (m : (s : Set α) → MeasurableSet s → ENNReal) (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) : MeasureTheory.Measure α

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

Equations

• MeasureTheory.Measure.ofMeasurable m m0 mU = let __src := MeasureTheory.inducedOuterMeasure m ⋯ m0; { toOuterMeasure := __src, m_iUnion := ⋯, trimmed := ⋯ }

theorem MeasureTheory.Measure.ofMeasurable_apply {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} {m0 : m ∅ ⋯ = 0} {mU : ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯} (s : Set α) (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.ofMeasurable m m0 mU) s = m s hs

theorem MeasureTheory.Measure.toOuterMeasure_injective {α : Type u_1} [MeasurableSpace α] : Function.Injective MeasureTheory.Measure.toOuterMeasure

theorem MeasureTheory.Measure.ext {α : Type u_1} [MeasurableSpace α] {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} (h : ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s = ↑↑μ₂ s) : μ₁ = μ₂

theorem MeasureTheory.Measure.ext_iff {α : Type u_1} [MeasurableSpace α] {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} : μ₁ = μ₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑↑μ₁ s = ↑↑μ₂ s

theorem MeasureTheory.Measure.ext_iff' {α : Type u_1} [MeasurableSpace α] {μ₁ : MeasureTheory.Measure α} {μ₂ : MeasureTheory.Measure α} : μ₁ = μ₂ ↔ ∀ (s : Set α), ↑↑μ₁ s = ↑↑μ₂ s

theorem MeasureTheory.measure_eq_trim {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α) : ↑↑μ s = ↑(MeasureTheory.OuterMeasure.trim ↑μ) s

theorem MeasureTheory.measure_eq_iInf {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α) : ↑↑μ s = ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), ↑↑μ t

theorem MeasureTheory.measure_eq_iInf' {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : ↑↑μ s = ⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), ↑↑μ ↑t

A variant of measure_eq_iInf which has a single iInf. 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 MeasureTheory.measure_eq_inducedOuterMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : ↑↑μ s = ↑(MeasureTheory.inducedOuterMeasure (fun (s : Set α) (x : MeasurableSet s) => ↑↑μ s) ⋯ ⋯) s

theorem MeasureTheory.toOuterMeasure_eq_inducedOuterMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : ↑μ = MeasureTheory.inducedOuterMeasure (fun (s : Set α) (x : MeasurableSet s) => ↑↑μ s) ⋯ ⋯

theorem MeasureTheory.measure_eq_extend {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : ↑↑μ s = MeasureTheory.extend (fun (t : Set α) (_ht : MeasurableSet t) => ↑↑μ t) s

theorem MeasureTheory.measure_empty {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : ↑↑μ ∅ = 0

theorem MeasureTheory.nonempty_of_measure_ne_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : ↑↑μ s ≠ 0) : Set.Nonempty s

theorem MeasureTheory.measure_mono {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (h : s₁ ⊆ s₂) : ↑↑μ s₁ ≤ ↑↑μ s₂

theorem MeasureTheory.measure_mono_null {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (h : s₁ ⊆ s₂) (h₂ : ↑↑μ s₂ = 0) : ↑↑μ s₁ = 0

theorem MeasureTheory.measure_mono_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} (h : s₁ ⊆ s₂) (h₁ : ↑↑μ s₁ = ⊤) : ↑↑μ s₂ = ⊤

@[simp]

theorem MeasureTheory.measure_le_measure_union_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : ↑↑μ s ≤ ↑↑μ (s ∪ t)

@[simp]

theorem MeasureTheory.measure_le_measure_union_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : ↑↑μ t ≤ ↑↑μ (s ∪ t)

theorem MeasureTheory.exists_measurable_superset {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s

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

theorem MeasureTheory.exists_measurable_superset_forall_eq {α : Type u_1} {ι : Sort u_5} [MeasurableSpace α] [Countable ι] (μ : ι → MeasureTheory.Measure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet 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 MeasureTheory.exists_measurable_superset₂ {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s ∧ ↑↑ν t = ↑↑ν s

theorem MeasureTheory.exists_measurable_superset_of_null {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (h : ↑↑μ s = 0) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = 0

theorem MeasureTheory.exists_measurable_superset_iff_measure_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : (∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = 0) ↔ ↑↑μ s = 0

theorem MeasureTheory.measure_iUnion_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable β] (s : β → Set α) : ↑↑μ (⋃ (i : β), s i) ≤ ∑' (i : β), ↑↑μ (s i)

theorem MeasureTheory.measure_biUnion_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set β} (hs : Set.Countable s) (f : β → Set α) : ↑↑μ (⋃ b ∈ s, f b) ≤ ∑' (p : ↑s), ↑↑μ (f ↑p)

theorem MeasureTheory.measure_biUnion_finset_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset β) (f : β → Set α) : ↑↑μ (⋃ b ∈ s, f b) ≤ Finset.sum s fun (p : β) => ↑↑μ (f p)

theorem MeasureTheory.measure_iUnion_fintype_le {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype β] (f : β → Set α) : ↑↑μ (⋃ (b : β), f b) ≤ Finset.sum Finset.univ fun (p : β) => ↑↑μ (f p)

theorem MeasureTheory.measure_biUnion_lt_top {α : Type u_1} {β : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set β} {f : β → Set α} (hs : Set.Finite s) (hfin : ∀ i ∈ s, ↑↑μ (f i) ≠ ⊤) : ↑↑μ (⋃ i ∈ s, f i) < ⊤

theorem MeasureTheory.measure_iUnion_null {α : Type u_1} {ι : Sort u_5} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} : (∀ (i : ι), ↑↑μ (s i) = 0) → ↑↑μ (⋃ (i : ι), s i) = 0

theorem MeasureTheory.measure_iUnion_null_iff {α : Type u_1} {ι : Sort u_5} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} : ↑↑μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), ↑↑μ (s i) = 0

@[deprecated]

theorem MeasureTheory.measure_iUnion_null_iff' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Prop} {s : ι → Set α} : ↑↑μ (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), ↑↑μ (s i) = 0

theorem MeasureTheory.measure_biUnion_null_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_6} {s : Set ι} (hs : Set.Countable s) {t : ι → Set α} : ↑↑μ (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, ↑↑μ (t i) = 0

theorem MeasureTheory.measure_sUnion_null_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {S : Set (Set α)} (hS : Set.Countable S) : ↑↑μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, ↑↑μ s = 0

theorem MeasureTheory.measure_null_iff_singleton {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : Set.Countable s) : ↑↑μ s = 0 ↔ ∀ x ∈ s, ↑↑μ {x} = 0

theorem MeasureTheory.measure_union_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s₁ : Set α) (s₂ : Set α) : ↑↑μ (s₁ ∪ s₂) ≤ ↑↑μ s₁ + ↑↑μ s₂

theorem MeasureTheory.measure_union_null {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} : ↑↑μ s₁ = 0 → ↑↑μ s₂ = 0 → ↑↑μ (s₁ ∪ s₂) = 0

@[simp]

theorem MeasureTheory.measure_union_null_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s₁ : Set α} {s₂ : Set α} : ↑↑μ (s₁ ∪ s₂) = 0 ↔ ↑↑μ s₁ = 0 ∧ ↑↑μ s₂ = 0

theorem MeasureTheory.measure_union_lt_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : ↑↑μ s < ⊤) (ht : ↑↑μ t < ⊤) : ↑↑μ (s ∪ t) < ⊤

@[simp]

theorem MeasureTheory.measure_union_lt_top_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : ↑↑μ (s ∪ t) < ⊤ ↔ ↑↑μ s < ⊤ ∧ ↑↑μ t < ⊤

theorem MeasureTheory.measure_union_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : ↑↑μ s ≠ ⊤) (ht : ↑↑μ t ≠ ⊤) : ↑↑μ (s ∪ t) ≠ ⊤

theorem MeasureTheory.measure_symmDiff_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : ↑↑μ s ≠ ⊤) (ht : ↑↑μ t ≠ ⊤) : ↑↑μ (symmDiff s t) ≠ ⊤

@[simp]

theorem MeasureTheory.measure_union_eq_top_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : ↑↑μ (s ∪ t) = ⊤ ↔ ↑↑μ s = ⊤ ∨ ↑↑μ t = ⊤

theorem MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null {α : Type u_1} {ι : Sort u_5} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} (hs : ↑↑μ (⋃ (n : ι), s n) ≠ 0) : ∃ (n : ι), 0 < ↑↑μ (s n)

theorem MeasureTheory.measure_lt_top_of_subset {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hst : t ⊆ s) (hs : ↑↑μ s ≠ ⊤) : ↑↑μ t < ⊤

theorem MeasureTheory.measure_inter_lt_top_of_left_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs_finite : ↑↑μ s ≠ ⊤) : ↑↑μ (s ∩ t) < ⊤

theorem MeasureTheory.measure_inter_lt_top_of_right_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht_finite : ↑↑μ t ≠ ⊤) : ↑↑μ (s ∩ t) < ⊤

theorem MeasureTheory.measure_inter_null_of_null_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (S : Set α) {T : Set α} (h : ↑↑μ T = 0) : ↑↑μ (S ∩ T) = 0

theorem MeasureTheory.measure_inter_null_of_null_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {S : Set α} (T : Set α) (h : ↑↑μ S = 0) : ↑↑μ (S ∩ T) = 0

The almost everywhere filter

def MeasureTheory.Measure.ae {α : Type u_6} {_m : MeasurableSpace α} (μ : MeasureTheory.Measure α) : Filter α

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

Equations

• MeasureTheory.Measure.ae μ = Filter.ofCountableUnion (fun (x : Set α) => ↑↑μ x = 0) ⋯ ⋯

def MeasureTheory.«term∀ᵐ_∂_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∀ᵐ_∂_,_» : Lean.ParserDescr

∀ᵐ a ∂μ, p a means that p a for a.e. a, i.e. p holds true away from a null set.

This is notation for Filter.Eventually p (Measure.ae μ).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∃ᵐ_∂_,_» : Lean.ParserDescr

∃ᵐ a ∂μ, p a means that p holds ∂μ-frequently, i.e. p holds on a set of positive measure.

This is notation for Filter.Frequently p (Measure.ae μ).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∃ᵐ_∂_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term_=ᵐ[_]_» : Lean.TrailingParserDescr

f =ᵐ[μ] g means f and g are eventually equal along the a.e. filter, i.e. f=g away from a null set.

This is notation for Filter.EventuallyEq (Measure.ae μ) f g.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term_≤ᵐ[_]_» : Lean.TrailingParserDescr

f ≤ᵐ[μ] g means f is eventually less than g along the a.e. filter, i.e. f ≤ g away from a null set.

This is notation for Filter.EventuallyLE (Measure.ae μ) f g.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.mem_ae_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : s ∈ MeasureTheory.Measure.ae μ ↔ ↑↑μ sᶜ = 0

theorem MeasureTheory.ae_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : α → Prop} : (∀ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a : α | ¬p a} = 0

theorem MeasureTheory.compl_mem_ae_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : sᶜ ∈ MeasureTheory.Measure.ae μ ↔ ↑↑μ s = 0

theorem MeasureTheory.frequently_ae_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : α → Prop} : (∃ᵐ (a : α) ∂μ, p a) ↔ ↑↑μ {a : α | p a} ≠ 0

theorem MeasureTheory.frequently_ae_mem_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : (∃ᵐ (a : α) ∂μ, a ∈ s) ↔ ↑↑μ s ≠ 0

theorem MeasureTheory.measure_zero_iff_ae_nmem {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : ↑↑μ s = 0 ↔ ∀ᵐ (a : α) ∂μ, a ∉ s

theorem MeasureTheory.ae_of_all {α : Type u_1} [MeasurableSpace α] {p : α → Prop} (μ : MeasureTheory.Measure α) : (∀ (a : α), p a) → ∀ᵐ (a : α) ∂μ, p a

instance MeasureTheory.instCountableInterFilter {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : CountableInterFilter (MeasureTheory.Measure.ae μ)

Equations

• ⋯ = ⋯

theorem MeasureTheory.ae_all_iff {α : Type u_1} {ι : Sort u_5} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable ι] {p : α → ι → Prop} : (∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i

theorem MeasureTheory.all_ae_of {α : Type u_1} {ι : Sort u_5} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : α → ι → Prop} (hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) (i : ι) : ∀ᵐ (a : α) ∂μ, p a i

theorem MeasureTheory.ae_iff_of_countable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Countable α] {p : α → Prop} : (∀ᵐ (x : α) ∂μ, p x) ↔ ∀ (x : α), ↑↑μ {x} ≠ 0 → p x

theorem MeasureTheory.ae_ball_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_6} {S : Set ι} (hS : Set.Countable S) {p : α → (i : ι) → i ∈ S → Prop} : (∀ᵐ (x : α) ∂μ, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᵐ (x : α) ∂μ, p x i hi

theorem MeasureTheory.ae_eq_refl {α : Type u_1} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (f : α → δ) : f =ᶠ[MeasureTheory.Measure.ae μ] f

theorem MeasureTheory.ae_eq_symm {α : Type u_1} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → δ} {g : α → δ} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : g =ᶠ[MeasureTheory.Measure.ae μ] f

theorem MeasureTheory.ae_eq_trans {α : Type u_1} {δ : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → δ} {g : α → δ} {h : α → δ} (h₁ : f =ᶠ[MeasureTheory.Measure.ae μ] g) (h₂ : g =ᶠ[MeasureTheory.Measure.ae μ] h) : f =ᶠ[MeasureTheory.Measure.ae μ] h

theorem MeasureTheory.ae_le_of_ae_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {β : Type u_6} [Preorder β] {f : α → β} {g : α → β} (h : ∀ᵐ (x : α) ∂μ, f x < g x) : f ≤ᶠ[MeasureTheory.Measure.ae μ] g

@[simp]

theorem MeasureTheory.ae_eq_empty {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ↔ ↑↑μ s = 0

@[simp]

theorem MeasureTheory.ae_eq_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ ↔ ↑↑μ sᶜ = 0

theorem MeasureTheory.ae_le_set {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : s ≤ᶠ[MeasureTheory.Measure.ae μ] t ↔ ↑↑μ (s \ t) = 0

theorem MeasureTheory.ae_le_set_inter {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} (h : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) (h' : s' ≤ᶠ[MeasureTheory.Measure.ae μ] t') : s ∩ s' ≤ᶠ[MeasureTheory.Measure.ae μ] t ∩ t'

theorem MeasureTheory.ae_le_set_union {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} (h : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) (h' : s' ≤ᶠ[MeasureTheory.Measure.ae μ] t') : s ∪ s' ≤ᶠ[MeasureTheory.Measure.ae μ] t ∪ t'

theorem MeasureTheory.union_ae_eq_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : s ∪ t =ᶠ[MeasureTheory.Measure.ae μ] t ↔ ↑↑μ (s \ t) = 0

theorem MeasureTheory.diff_ae_eq_self {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : s \ t =ᶠ[MeasureTheory.Measure.ae μ] s ↔ ↑↑μ (s ∩ t) = 0

theorem MeasureTheory.diff_null_ae_eq_self {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : ↑↑μ t = 0) : s \ t =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.ae_eq_set {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : s =ᶠ[MeasureTheory.Measure.ae μ] t ↔ ↑↑μ (s \ t) = 0 ∧ ↑↑μ (t \ s) = 0

@[simp]

theorem MeasureTheory.measure_symmDiff_eq_zero_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : ↑↑μ (symmDiff s t) = 0 ↔ s =ᶠ[MeasureTheory.Measure.ae μ] t

@[simp]

theorem MeasureTheory.ae_eq_set_compl_compl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : sᶜ =ᶠ[MeasureTheory.Measure.ae μ] tᶜ ↔ s =ᶠ[MeasureTheory.Measure.ae μ] t

theorem MeasureTheory.ae_eq_set_compl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} : sᶜ =ᶠ[MeasureTheory.Measure.ae μ] t ↔ s =ᶠ[MeasureTheory.Measure.ae μ] tᶜ

theorem MeasureTheory.ae_eq_set_inter {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] t) (h' : s' =ᶠ[MeasureTheory.Measure.ae μ] t') : s ∩ s' =ᶠ[MeasureTheory.Measure.ae μ] t ∩ t'

theorem MeasureTheory.ae_eq_set_union {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] t) (h' : s' =ᶠ[MeasureTheory.Measure.ae μ] t') : s ∪ s' =ᶠ[MeasureTheory.Measure.ae μ] t ∪ t'

theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ) : s ∪ t =ᶠ[MeasureTheory.Measure.ae μ] Set.univ

theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : t =ᶠ[MeasureTheory.Measure.ae μ] Set.univ) : s ∪ t =ᶠ[MeasureTheory.Measure.ae μ] Set.univ

theorem MeasureTheory.union_ae_eq_right_of_ae_eq_empty {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] ∅) : s ∪ t =ᶠ[MeasureTheory.Measure.ae μ] t

theorem MeasureTheory.union_ae_eq_left_of_ae_eq_empty {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : t =ᶠ[MeasureTheory.Measure.ae μ] ∅) : s ∪ t =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.inter_ae_eq_right_of_ae_eq_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ) : s ∩ t =ᶠ[MeasureTheory.Measure.ae μ] t

theorem MeasureTheory.inter_ae_eq_left_of_ae_eq_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : t =ᶠ[MeasureTheory.Measure.ae μ] Set.univ) : s ∩ t =ᶠ[MeasureTheory.Measure.ae μ] s

theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s =ᶠ[MeasureTheory.Measure.ae μ] ∅) : s ∩ t =ᶠ[MeasureTheory.Measure.ae μ] ∅

theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : t =ᶠ[MeasureTheory.Measure.ae μ] ∅) : s ∩ t =ᶠ[MeasureTheory.Measure.ae μ] ∅

theorem MeasurableSpace.ae_induction_on_inter {α : Type u_1} {β : Type u_6} [MeasurableSpace β] {μ : MeasureTheory.Measure β} {C : β → Set α → Prop} {s : Set (Set α)} [m : MeasurableSpace α] (h_eq : m = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (h_empty : ∀ᵐ (x : β) ∂μ, C x ∅) (h_basic : ∀ᵐ (x : β) ∂μ, ∀ t ∈ s, C x t) (h_compl : ∀ᵐ (x : β) ∂μ, ∀ (t : Set α), MeasurableSet t → C x t → C x tᶜ) (h_union : ∀ᵐ (x : β) ∂μ, ∀ (f : ℕ → Set α), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C x (f i)) → C x (⋃ (i : ℕ), f i)) : ∀ᵐ (x : β) ∂μ, ∀ ⦃t : Set α⦄, MeasurableSet t → C x t

Given a predicate on β and Set α where both α and β are measurable spaces, if the predicate holds for almost every x : β and

• ∅ : Set α
• a family of sets generating the σ-algebra of α Moreover, if for almost every x : β, the predicate is closed under complements and countable disjoint unions, then the predicate holds for almost every x : β and all measurable sets of α.

This is an AE version of MeasurableSpace.induction_on_inter where the condition is dependent on a measurable space β.

theorem Set.indicator_ae_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {M : Type u_6} [Zero M] {f : α → M} {s : Set α} : Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] 0 ↔ ↑↑μ (s ∩ Function.support f) = 0

theorem Set.mulIndicator_ae_eq_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {M : Type u_6} [One M] {f : α → M} {s : Set α} : Set.mulIndicator s f =ᶠ[MeasureTheory.Measure.ae μ] 1 ↔ ↑↑μ (s ∩ Function.mulSupport f) = 0

theorem MeasureTheory.measure_mono_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (H : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) : ↑↑μ s ≤ ↑↑μ t

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

theorem Filter.EventuallyLE.measure_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (H : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) : ↑↑μ s ≤ ↑↑μ t

Alias of MeasureTheory.measure_mono_ae.

---

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

theorem MeasureTheory.measure_congr {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (H : s =ᶠ[MeasureTheory.Measure.ae μ] t) : ↑↑μ s = ↑↑μ t

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

theorem Filter.EventuallyEq.measure_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (H : s =ᶠ[MeasureTheory.Measure.ae μ] t) : ↑↑μ s = ↑↑μ t

Alias of MeasureTheory.measure_congr.

---

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

theorem MeasureTheory.measure_mono_null_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (H : s ≤ᶠ[MeasureTheory.Measure.ae μ] t) (ht : ↑↑μ t = 0) : ↑↑μ s = 0

@[irreducible]

def MeasureTheory.toMeasurable {α : Type u_6} [MeasurableSpace α] (μ : MeasureTheory.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_toMeasurable_inter. (This property holds without the assumption μ s ≠ ∞ when the space is s-finite -- for example σ-finite), see measure_toMeasurable_inter_of_sFinite). If s is a null measurable set, then we also have t =ᵐ[μ] s, see NullMeasurableSet.toMeasurable_ae_eq. This notion is sometimes called a "measurable hull" in the literature.

Equations

• @MeasureTheory.toMeasurable = MeasureTheory.wrapped✝.1

theorem MeasureTheory.toMeasurable_def {α : Type u_6} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.toMeasurable μ s = if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[MeasureTheory.Measure.ae μ] s then Exists.choose h else if h' : ∃ t ⊇ s, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then Exists.choose h' else Exists.choose ⋯

theorem MeasureTheory.subset_toMeasurable {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : s ⊆ MeasureTheory.toMeasurable μ s

theorem MeasureTheory.ae_le_toMeasurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : s ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.toMeasurable μ s

@[simp]

theorem MeasureTheory.measurableSet_toMeasurable {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : MeasurableSet (MeasureTheory.toMeasurable μ s)

@[simp]

theorem MeasureTheory.measure_toMeasurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Set α) : ↑↑μ (MeasureTheory.toMeasurable μ s) = ↑↑μ s

class MeasureTheory.MeasureSpace (α : Type u_6) extends MeasurableSpace : Type u_6

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

• MeasurableSet' : Set α → Prop
• measurableSet_empty : MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' ∅
• measurableSet_compl : ∀ (s : Set α), MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' s → MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' sᶜ
• measurableSet_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' (f i)) → MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' (⋃ (i : ℕ), f i)
• volume : MeasureTheory.Measure α

  volume is the canonical measure on α.

def MeasureTheory.«term∀ᵐ_,_» : Lean.ParserDescr

∀ᵐ a, p a means that p a for a.e. a, i.e. p holds true away from a null set.

This is notation for Filter.Eventually P (Measure.ae MeasureSpace.volume).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∀ᵐ_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∃ᵐ_,_» : Lean.ParserDescr

∃ᵐ a, p a means that p holds frequently, i.e. on a set of positive measure, w.r.t. the volume measure.

This is notation for Filter.Frequently P (Measure.ae MeasureSpace.volume).

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.«term∃ᵐ_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def MeasureTheory.tacticVolume_tac : Lean.ParserDescr

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

Equations

• MeasureTheory.tacticVolume_tac = Lean.ParserDescr.node `MeasureTheory.tacticVolume_tac 1024 (Lean.ParserDescr.nonReservedSymbol "volume_tac" false)

Almost everywhere measurable functions

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

def AEMeasurable {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {_m : MeasurableSpace α} (f : α → β) (μ : autoParam (MeasureTheory.Measure α) _auto✝) : Prop

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

Equations

• AEMeasurable f μ = ∃ (g : α → β), Measurable g ∧ f =ᶠ[MeasureTheory.Measure.ae μ] g

theorem Measurable.aemeasurable {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (h : Measurable f) : AEMeasurable f μ

def AEMeasurable.mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} (f : α → β) (h : AEMeasurable 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

• AEMeasurable.mk f h = Classical.choose h

theorem AEMeasurable.measurable_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (h : AEMeasurable f μ) : Measurable (AEMeasurable.mk f h)

theorem AEMeasurable.ae_eq_mk {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {μ : MeasureTheory.Measure α} (h : AEMeasurable f μ) : f =ᶠ[MeasureTheory.Measure.ae μ] AEMeasurable.mk f h

theorem AEMeasurable.congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {g : α → β} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : AEMeasurable g μ

theorem aemeasurable_congr {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {f : α → β} {g : α → β} {μ : MeasureTheory.Measure α} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : AEMeasurable f μ ↔ AEMeasurable g μ

@[simp]

theorem aemeasurable_const {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} {b : β} : AEMeasurable (fun (_a : α) => b) μ

theorem aemeasurable_id {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} : AEMeasurable id μ

theorem aemeasurable_id' {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} : AEMeasurable (fun (x : α) => x) μ

theorem Measurable.comp_aemeasurable {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasurableSpace δ] {f : α → δ} {g : δ → β} (hg : Measurable g) (hf : AEMeasurable f μ) : AEMeasurable (g ∘ f) μ

theorem Measurable.comp_aemeasurable' {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [MeasurableSpace δ] {f : α → δ} {g : δ → β} (hg : Measurable g) (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => g (f x)) μ