Measure spaces
Given a measurable space α, a measure on α is a function that sends measurable sets to the
extended nonnegative reals that satisfies the following conditions:
μ ∅ = 0;μis countably additive. This means that the measure of a countable union of pairwise disjoint sets is equal to the measure of the individual sets.
Every measure can be canonically extended to an outer measure, so that it assigns values to all subsets, not just the measurable subsets. On the other hand, a measure that is countably additive on measurable sets can be restricted to measurable sets to obtain a measure. In this file a measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.
Measures on α form a complete lattice, and are closed under scalar multiplication with ennreal.
We introduce the following typeclasses for measures:
probability_measure μ:μ univ = 1;finite_measure μ:μ univ < ⊤;locally_finite_measure μ:∀ x, ∃ s ∈ 𝓝 x, μ 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
completionis the completion of a measure to all null measurable sets.measure.of_measurableandouter_measure.to_measureare 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_measurableis 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_measureis a way of obtaining a measure from an outer measure by showing that all measurable sets in the measurable space are Carathéodory measurable.
A measure_space is a class that is a measurable space with a canonical measure.
The measure is denoted volume.
References
- https://en.wikipedia.org/wiki/Measure_(mathematics)
- https://en.wikipedia.org/wiki/Complete_measure
- https://en.wikipedia.org/wiki/Almost_everywhere
Tags
measure, almost everywhere, measure space, completion, null set, null measurable set
- to_outer_measure : measure_theory.outer_measure α
- m_Union : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), is_measurable (f i)) → pairwise (disjoint on f) → (c.to_outer_measure.measure_of (⋃ (i : ℕ), f i) = ∑' (i : ℕ), c.to_outer_measure.measure_of (f i))
- trimmed : c.to_outer_measure.trim = c.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.
@[instance]
Measure projections for a measure space.
For measurable sets this returns the measure assigned by the measure_of field in measure.
But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and
subadditivity for all sets.
Equations
- measure_theory.measure.has_coe_to_fun = {F := λ (_x : measure_theory.measure α), set α → ennreal, coe := λ (m : measure_theory.measure α), ⇑(m.to_outer_measure)}
def
measure_theory.measure.of_measurable
{α : Type u_1}
[measurable_space α]
(m : Π (s : set α), is_measurable s → ennreal) :
m ∅ is_measurable.empty = 0 → (∀ ⦃f : ℕ → set α⦄ (h : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → (m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _)) → measure_theory.measure α
Obtain a measure by giving a countably additive function that sends ∅ to 0.
Equations
- measure_theory.measure.of_measurable m m0 mU = {to_outer_measure := {measure_of := (measure_theory.induced_outer_measure m is_measurable.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 α), is_measurable s → ennreal}
{m0 : m ∅ is_measurable.empty = 0}
{mU : ∀ ⦃f : ℕ → set α⦄ (h : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → (m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _)}
(s : set α)
(hs : is_measurable s) :
⇑(measure_theory.measure.of_measurable m m0 mU) s = m s hs
@[ext]
theorem
measure_theory.measure.ext
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α} :
theorem
measure_theory.measure.ext_iff
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α} :
@[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 α) :
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 : is_measurable s), ⇑μ s) is_measurable.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 : is_measurable s), ⇑μ s) is_measurable.empty _
theorem
measure_theory.measure_eq_extend
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
is_measurable s → ⇑μ s = measure_theory.extend (λ (t : set α) (ht : is_measurable t), ⇑μ t) s
@[simp]
theorem
measure_theory.measure_empty
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.nonempty_of_measure_ne_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
theorem
measure_theory.measure_mono_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
theorem
measure_theory.exists_is_measurable_superset_of_measure_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.exists_is_measurable_superset_iff_measure_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure_Union_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[encodable β]
(s : β → set α) :
theorem
measure_theory.measure_bUnion_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set β}
(hs : s.countable)
(f : β → set α) :
theorem
measure_theory.measure_bUnion_finset_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
(s : finset β)
(f : β → set α) :
theorem
measure_theory.measure_Union_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[encodable β]
{s : β → set α} :
theorem
measure_theory.measure_union_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(s₁ s₂ : set α) :
theorem
measure_theory.measure_union_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
theorem
measure_theory.measure_Union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{β : Type u_2}
[encodable β]
{f : β → set α} :
theorem
measure_theory.measure_union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
disjoint s₁ s₂ → is_measurable s₁ → is_measurable s₂ → ⇑μ (s₁ ∪ s₂) = ⇑μ s₁ + ⇑μ s₂
theorem
measure_theory.measure_bUnion
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set β}
{f : β → set α} :
theorem
measure_theory.measure_sUnion
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{S : set (set α)} :
theorem
measure_theory.measure_bUnion_finset
{α : Type u_1}
{ι : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
{s : finset ι}
{f : ι → set α} :
theorem
measure_theory.tsum_measure_preimage_singleton
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set β}
(hs : s.countable)
{f : α → β} :
If s is a countable set, then the measure of its preimage can be found as the sum of measures
of the fibers f ⁻¹' {y}.
theorem
measure_theory.sum_measure_preimage_singleton
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
(s : finset β)
{f : α → β} :
If s is a finset, then the measure of its preimage can be found as the sum of measures
of the fibers f ⁻¹' {y}.
theorem
measure_theory.measure_diff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
theorem
measure_theory.sum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
{s : finset ι}
{t : ι → set α} :
theorem
measure_theory.tsum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ι → set α} :
theorem
measure_theory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure
{α : Type u_1}
{ι : Type u_3}
[measurable_space α]
(μ : measure_theory.measure α)
{s : ι → set α} :
Pigeonhole principle for measure spaces: if ∑' i, μ (s i) > μ univ, then
one of the intersections s i ∩ s j is not empty.
theorem
measure_theory.exists_nonempty_inter_of_measure_univ_lt_sum_measure
{α : Type u_1}
{ι : Type u_3}
[measurable_space α]
(μ : measure_theory.measure α)
{s : finset ι}
{t : ι → set α} :
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_nat
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α} :
theorem
measure_theory.measure_Inter_eq_infi_nat
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α} :
theorem
measure_theory.measure_eq_inter_diff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
is_measurable s → is_measurable t → ⇑μ s = ⇑μ (s ∩ t) + ⇑μ (s \ t)
theorem
measure_theory.tendsto_measure_Union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α} :
(∀ (n : ℕ), is_measurable (s n)) → monotone s → filter.tendsto (⇑μ ∘ s) filter.at_top (nhds (⇑μ (⋃ (n : ℕ), s n)))
theorem
measure_theory.tendsto_measure_Inter
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α} :
def
measure_theory.outer_measure.to_measure
{α : Type u_1}
(m : measure_theory.outer_measure α)
[ms : measurable_space α] :
ms ≤ m.caratheodory → measure_theory.measure α
Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.
Equations
- m.to_measure h = measure_theory.measure.of_measurable (λ (s : set α) (_x : is_measurable s), ⇑m s) _ _
theorem
measure_theory.le_to_outer_measure_caratheodory
{α : Type u_1}
[ms : measurable_space α]
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.to_measure_to_outer_measure
{α : Type u_1}
(m : measure_theory.outer_measure α)
[ms : measurable_space α]
(h : ms ≤ m.caratheodory) :
(m.to_measure h).to_outer_measure = m.trim
@[simp]
theorem
measure_theory.to_measure_apply
{α : Type u_1}
(m : measure_theory.outer_measure α)
[ms : measurable_space α]
(h : ms ≤ m.caratheodory)
{s : set α} :
is_measurable s → ⇑(m.to_measure h) s = ⇑m s
theorem
measure_theory.le_to_measure_apply
{α : Type u_1}
(m : measure_theory.outer_measure α)
[ms : measurable_space α]
(h : ms ≤ m.caratheodory)
(s : set α) :
⇑m s ≤ ⇑(m.to_measure h) s
@[simp]
theorem
measure_theory.to_outer_measure_to_measure
{α : Type u_1}
[ms : measurable_space α]
{μ : measure_theory.measure α} :
μ.to_outer_measure.to_measure _ = μ
@[instance]
Equations
- measure_theory.measure.has_zero = {zero := {to_outer_measure := 0, m_Union := _, trimmed := _}}
@[simp]
theorem
measure_theory.measure.zero_to_outer_measure
{α : Type u_1}
[measurable_space α] :
0.to_outer_measure = 0
@[simp]
theorem
measure_theory.measure.eq_zero_of_not_nonempty
{α : Type u_1}
[measurable_space α]
(h : ¬nonempty α)
(μ : measure_theory.measure α) :
μ = 0
@[instance]
Equations
- measure_theory.measure.has_add = {add := λ (μ₁ μ₂ : measure_theory.measure α), {to_outer_measure := μ₁.to_outer_measure + μ₂.to_outer_measure, m_Union := _, trimmed := _}}
@[simp]
theorem
measure_theory.measure.add_to_outer_measure
{α : Type u_1}
[measurable_space α]
(μ₁ μ₂ : measure_theory.measure α) :
(μ₁ + μ₂).to_outer_measure = μ₁.to_outer_measure + μ₂.to_outer_measure
@[simp]
theorem
measure_theory.measure.coe_add
{α : Type u_1}
[measurable_space α]
(μ₁ μ₂ : measure_theory.measure α) :
theorem
measure_theory.measure.add_apply
{α : Type u_1}
[measurable_space α]
(μ₁ μ₂ : measure_theory.measure α)
(s : set α) :
@[instance]
@[instance]
Equations
- measure_theory.measure.has_scalar = {smul := λ (c : ennreal) (μ : measure_theory.measure α), {to_outer_measure := c • μ.to_outer_measure, m_Union := _, trimmed := _}}
@[simp]
theorem
measure_theory.measure.smul_to_outer_measure
{α : Type u_1}
[measurable_space α]
(c : ennreal)
(μ : measure_theory.measure α) :
(c • μ).to_outer_measure = c • μ.to_outer_measure
@[simp]
theorem
measure_theory.measure.coe_smul
{α : Type u_1}
[measurable_space α]
(c : ennreal)
(μ : measure_theory.measure α) :
theorem
measure_theory.measure.smul_apply
{α : Type u_1}
[measurable_space α]
(c : ennreal)
(μ : measure_theory.measure α)
(s : set α) :
@[instance]
@[instance]
Equations
- measure_theory.measure.partial_order = {le := λ (m₁ m₂ : measure_theory.measure α), ∀ (s : set α), is_measurable s → ⇑m₁ s ≤ ⇑m₂ s, lt := preorder.lt._default (λ (m₁ m₂ : measure_theory.measure α), ∀ (s : set α), is_measurable s → ⇑m₁ s ≤ ⇑m₂ s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
theorem
measure_theory.measure.le_iff
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α} :
theorem
measure_theory.measure.to_outer_measure_le
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α} :
μ₁.to_outer_measure ≤ μ₂.to_outer_measure ↔ μ₁ ≤ μ₂
theorem
measure_theory.measure.le_iff'
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α} :
theorem
measure_theory.measure.lt_iff
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
theorem
measure_theory.measure.lt_iff'
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
theorem
measure_theory.measure.Inf_caratheodory
{α : Type u_1}
[measurable_space α]
{m : set (measure_theory.measure α)}
(s : set α) :
theorem
measure_theory.measure.Inf_apply
{α : Type u_1}
[measurable_space α]
{m : set (measure_theory.measure α)}
{s : set α} :
is_measurable s → ⇑(has_Inf.Inf m) s = ⇑(has_Inf.Inf (measure_theory.measure.to_outer_measure '' m)) s
@[instance]
Equations
- measure_theory.measure.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), inf_le_left := _, inf_le_right := _, le_inf := _, top := complete_lattice.top (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le_top := _, bot := 0, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), Inf := complete_lattice.Inf (complete_lattice_of_Inf (measure_theory.measure α) measure_theory.measure.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
@[simp]
theorem
measure_theory.measure.measure_univ_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.measure.add_le_add_left
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α}
(ν : measure_theory.measure α) :
theorem
measure_theory.measure.add_le_add_right
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α}
(hμ : μ₁ ≤ μ₂)
(ν : measure_theory.measure α) :
theorem
measure_theory.measure.add_le_add
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α}
(hμ : μ₁ ≤ μ₂)
{ν₁ ν₂ : measure_theory.measure α} :
theorem
measure_theory.measure.zero_le
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
0 ≤ μ
theorem
measure_theory.measure.le_add_left
{α : Type u_1}
[measurable_space α]
{μ ν ν' : measure_theory.measure α} :
theorem
measure_theory.measure.le_add_right
{α : Type u_1}
[measurable_space α]
{μ ν ν' : measure_theory.measure α} :
def
measure_theory.measure.lift_linear
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β) :
(∀ (μ : measure_theory.measure α), _inst_2 ≤ (⇑f μ.to_outer_measure).caratheodory) → (measure_theory.measure α →ₗ[ennreal] measure_theory.measure β)
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
- measure_theory.measure.lift_linear f hf = {to_fun := λ (μ : measure_theory.measure α), (⇑f μ.to_outer_measure).to_measure _, map_add' := _, map_smul' := _}
@[simp]
theorem
measure_theory.measure.lift_linear_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β}
(hf : ∀ (μ : measure_theory.measure α), _inst_2 ≤ (⇑f μ.to_outer_measure).caratheodory)
{μ : measure_theory.measure α}
{s : set β} :
is_measurable s → ⇑(⇑(measure_theory.measure.lift_linear f hf) μ) s = ⇑(⇑f μ.to_outer_measure) s
theorem
measure_theory.measure.le_lift_linear_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β}
(hf : ∀ (μ : measure_theory.measure α), _inst_2 ≤ (⇑f μ.to_outer_measure).caratheodory)
{μ : measure_theory.measure α}
(s : set β) :
⇑(⇑f μ.to_outer_measure) s ≤ ⇑(⇑(measure_theory.measure.lift_linear f hf) μ) s
def
measure_theory.measure.map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β] :
(α → β) → (measure_theory.measure α →ₗ[ennreal] measure_theory.measure β)
The pushforward of a measure. It is defined to be 0 if f is not a measurable function.
Equations
- measure_theory.measure.map f = dite (measurable f) (λ (hf : measurable f), measure_theory.measure.lift_linear (measure_theory.outer_measure.map f) _) (λ (hf : ¬measurable f), 0)
@[simp]
theorem
measure_theory.measure.map_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{s : set β} :
is_measurable s → ⇑(⇑(measure_theory.measure.map f) μ) s = ⇑μ (f ⁻¹' s)
@[simp]
theorem
measure_theory.measure.map_id
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
⇑(measure_theory.measure.map id) μ = μ
theorem
measure_theory.measure.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μ : measure_theory.measure α}
{g : β → γ}
{f : α → β} :
measurable g → measurable f → ⇑(measure_theory.measure.map g) (⇑(measure_theory.measure.map f) μ) = ⇑(measure_theory.measure.map (g ∘ f)) μ
def
measure_theory.measure.comap
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β] :
(α → β) → (measure_theory.measure β →ₗ[ennreal] measure_theory.measure α)
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
- measure_theory.measure.comap f = dite (function.injective f ∧ ∀ (s : set α), is_measurable s → is_measurable (f '' s)) (λ (hf : function.injective f ∧ ∀ (s : set α), is_measurable s → is_measurable (f '' s)), measure_theory.measure.lift_linear (measure_theory.outer_measure.comap f) _) (λ (hf : ¬(function.injective f ∧ ∀ (s : set α), is_measurable s → is_measurable (f '' s))), 0)
theorem
measure_theory.measure.comap_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β)
(hfi : function.injective f)
(hf : ∀ (s : set α), is_measurable s → is_measurable (f '' s))
(μ : measure_theory.measure β)
{s : set α} :
is_measurable s → ⇑(⇑(measure_theory.measure.comap f) μ) s = ⇑μ (f '' s)
Restrict a measure μ to a set s as an ennreal-linear map.
def
measure_theory.measure.restrict
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → set α → measure_theory.measure α
Restrict a measure μ to a set s.
Equations
- μ.restrict s = ⇑(measure_theory.measure.restrictₗ s) μ
@[simp]
theorem
measure_theory.measure.restrictₗ_apply
{α : Type u_1}
[measurable_space α]
(s : set α)
(μ : measure_theory.measure α) :
⇑(measure_theory.measure.restrictₗ s) μ = μ.restrict s
@[simp]
theorem
measure_theory.measure.restrict_apply
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.measure.restrict_apply_univ
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(s : set α) :
theorem
measure_theory.measure.le_restrict_apply
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(s t : set α) :
@[simp]
theorem
measure_theory.measure.restrict_add
{α : Type u_1}
[measurable_space α]
(μ ν : measure_theory.measure α)
(s : set α) :
@[simp]
@[simp]
theorem
measure_theory.measure.restrict_smul
{α : Type u_1}
[measurable_space α]
(c : ennreal)
(μ : measure_theory.measure α)
(s : set α) :
theorem
measure_theory.measure.restrict_apply_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.measure.restrict_apply_eq_zero'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
@[simp]
theorem
measure_theory.measure.restrict_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
@[simp]
theorem
measure_theory.measure.restrict_empty
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.restrict_univ
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.measure.restrict_union_apply
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s s' t : set α} :
disjoint (t ∩ s) (t ∩ s') → is_measurable s → is_measurable s' → is_measurable t → ⇑(μ.restrict (s ∪ s')) t = ⇑(μ.restrict s) t + ⇑(μ.restrict s') t
theorem
measure_theory.measure.restrict_union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
disjoint s t → is_measurable s → is_measurable t → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
@[simp]
theorem
measure_theory.measure.restrict_add_restrict_compl
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
@[simp]
theorem
measure_theory.measure.restrict_compl_add_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure.restrict_union_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(s s' : set α) :
theorem
measure_theory.measure.restrict_Union_apply
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Type u_2}
[encodable ι]
{s : ι → set α}
(hd : pairwise (disjoint on s))
(hm : ∀ (i : ι), is_measurable (s i))
{t : set α} :
theorem
measure_theory.measure.map_comap_subtype_coe
{α : Type u_1}
[measurable_space α]
{s : set α} :
theorem
measure_theory.measure.restrict_mono
{α : Type u_1}
[measurable_space α]
⦃s s' : set α⦄
(hs : s ⊆ s')
⦃μ ν : measure_theory.measure α⦄ :
Restriction of a measure to a subset is monotone both in set and in measure.
theorem
measure_theory.measure.restrict_le_self
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
def
measure_theory.measure.dirac
{α : Type u_1}
[measurable_space α] :
α → measure_theory.measure α
The dirac measure.
Equations
theorem
measure_theory.measure.dirac_apply'
{α : Type u_1}
[measurable_space α]
(a : α)
{s : set α} :
is_measurable s → (⇑(measure_theory.measure.dirac a) s = ⨆ (h : a ∈ s), 1)
@[simp]
theorem
measure_theory.measure.dirac_apply
{α : Type u_1}
[measurable_space α]
(a : α)
{s : set α} :
is_measurable s → ⇑(measure_theory.measure.dirac a) s = s.indicator 1 a
theorem
measure_theory.measure.dirac_apply_of_mem
{α : Type u_1}
[measurable_space α]
{a : α}
{s : set α} :
a ∈ s → ⇑(measure_theory.measure.dirac a) s = 1
def
measure_theory.measure.sum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2} :
(ι → measure_theory.measure α) → measure_theory.measure α
Sum of an indexed family of measures.
Equations
- measure_theory.measure.sum f = (measure_theory.outer_measure.sum (λ (i : ι), (f i).to_outer_measure)).to_measure _
@[simp]
theorem
measure_theory.measure.sum_apply
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
(f : ι → measure_theory.measure α)
{s : set α} :
is_measurable s → (⇑(measure_theory.measure.sum f) s = ∑' (i : ι), ⇑(f i) s)
theorem
measure_theory.measure.le_sum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
(μ : ι → measure_theory.measure α)
(i : ι) :
μ i ≤ measure_theory.measure.sum μ
theorem
measure_theory.measure.restrict_Union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Type u_2}
[encodable ι]
{s : ι → set α} :
pairwise (disjoint on s) → (∀ (i : ι), is_measurable (s i)) → μ.restrict (⋃ (i : ι), s i) = measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))
theorem
measure_theory.measure.restrict_Union_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Type u_2}
[encodable ι]
{s : ι → set α} :
μ.restrict (⋃ (i : ι), s i) ≤ measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))
@[simp]
theorem
measure_theory.measure.sum_bool
{α : Type u_1}
[measurable_space α]
(f : bool → measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.restrict_sum
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
(μ : ι → measure_theory.measure α)
{s : set α} :
is_measurable s → (measure_theory.measure.sum μ).restrict s = measure_theory.measure.sum (λ (i : ι), (μ i).restrict s)
Counting measure on any measurable space.
theorem
measure_theory.measure.count_apply
{α : Type u_1}
[measurable_space α]
{s : set α} :
is_measurable s → (⇑measure_theory.measure.count s = ∑' (i : ↥s), 1)
@[simp]
theorem
measure_theory.measure.count_apply_finset
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(s : finset α) :
theorem
measure_theory.measure.count_apply_finite
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(s : set α)
(hs : s.finite) :
theorem
measure_theory.measure.count_apply_infinite
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α} :
count measure evaluates to infinity at infinite sets.
@[simp]
theorem
measure_theory.measure.count_apply_eq_top
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α} :
@[simp]
theorem
measure_theory.measure.count_apply_lt_top
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
{s : set α} :
@[class]
def
measure_theory.measure.is_complete
{α : Type u_1}
{_x : measurable_space α} :
measure_theory.measure α → Prop
A measure is complete if every null set is also measurable.
A null set is a subset of a measurable set with measure 0.
Since every measure is defined as a special case of an outer measure, we can more simply state
that a set s is null if μ s = 0.
Equations
- μ.is_complete = ∀ (s : set α), ⇑μ s = 0 → is_measurable s
Instances
def
measure_theory.measure.ae
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → filter α
The “almost everywhere” filter of co-null sets.
def
measure_theory.measure.cofinite
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → filter α
The filter of sets s such that sᶜ has finite measure.
theorem
measure_theory.measure.mem_cofinite
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure.compl_mem_cofinite
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure.eventually_cofinite
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop} :
theorem
measure_theory.mem_ae_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.ae_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop} :
theorem
measure_theory.compl_mem_ae_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure_zero_iff_ae_nmem
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.ae_eq_bot
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.ae_of_all
{α : Type u_1}
[measurable_space α]
{p : α → Prop}
(μ : measure_theory.measure α) :
(∀ (a : α), p a) → (∀ᵐ (a : α) ∂μ, p a)
theorem
measure_theory.ae_mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
@[instance]
def
measure_theory.countable_Inter_filter
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
Equations
@[instance]
def
measure_theory.ae_is_measurably_generated
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
Equations
theorem
measure_theory.ae_all_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Type u_2}
[encodable ι]
{p : α → ι → Prop} :
(∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i) ↔ ∀ (i : ι), ∀ᵐ (a : α) ∂μ, p a i
theorem
measure_theory.ae_ball_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{ι : Type u_2}
{S : set ι}
(hS : S.countable)
{p : α → Π (i : ι), i ∈ S → Prop} :
theorem
measure_theory.ae_eq_refl
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α → β) :
theorem
measure_theory.ae_eq_symm
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → β} :
theorem
measure_theory.ae_eq_trans
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{f g h : α → β} :
theorem
measure_theory.mem_ae_map_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
{f : α → β}
(hf : measurable f)
{s : set β} :
is_measurable s → (s ∈ (⇑(measure_theory.measure.map f) μ).ae ↔ f ⁻¹' s ∈ μ.ae)
theorem
measure_theory.ae_map_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[measurable_space β]
{f : α → β}
(hf : measurable f)
{p : β → Prop} :
is_measurable {x : β | p x} → ((∀ᵐ (y : β) ∂⇑(measure_theory.measure.map f) μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x))
theorem
measure_theory.ae_restrict_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{p : α → Prop} :
is_measurable {x : α | p x} → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
theorem
measure_theory.ae_smul_measure
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop}
(h : ∀ᵐ (x : α) ∂μ, p x)
(c : ennreal) :
∀ᵐ (x : α) ∂c • μ, p x
theorem
measure_theory.ae_add_measure_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop}
{ν : measure_theory.measure α} :
@[simp]
theorem
measure_theory.ae_restrict_eq
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
is_measurable s → (μ.restrict s).ae = μ.ae ⊓ filter.principal s
@[simp]
theorem
measure_theory.ae_restrict_eq_bot
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
@[simp]
theorem
measure_theory.ae_restrict_ne_bot
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.mem_dirac_ae_iff
{α : Type u_1}
[measurable_space α]
{a : α}
{s : set α} :
is_measurable s → (s ∈ (measure_theory.measure.dirac a).ae ↔ a ∈ s)
theorem
measure_theory.eventually_dirac
{α : Type u_1}
[measurable_space α]
{a : α}
{p : α → Prop} :
is_measurable {x : α | p x} → ((∀ᵐ (x : α) ∂measure_theory.measure.dirac a, p x) ↔ p a)
theorem
measure_theory.eventually_eq_dirac
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[measurable_singleton_class β]
{a : α}
{f : α → β} :
measurable f → f =ᵐ[measure_theory.measure.dirac a] function.const α (f a)
theorem
measure_theory.dirac_ae_eq
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(a : α) :
theorem
measure_theory.eventually_eq_dirac'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_singleton_class α]
{a : α}
(f : α → β) :
f =ᵐ[measure_theory.measure.dirac a] function.const α (f a)
theorem
measure_theory.measure_diff_of_ae_le
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.measure_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
If s ⊆ t modulo a set of measure 0, then μ s ≤ μ t.
theorem
measure_theory.measure_congr
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
If two sets are equal modulo a set of measure zero, then μ s = μ t.
theorem
measure_theory.restrict_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.restrict_congr
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
@[class]
structure
measure_theory.probability_measure
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → Prop
A measure μ is called a probability measure if μ univ = 1.
@[class]
structure
measure_theory.finite_measure
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → Prop
A measure μ is called finite if μ univ < ⊤.
theorem
measure_theory.measure_lt_top
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ]
(s : set α) :
theorem
measure_theory.measure_ne_top
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ]
(s : set α) :
@[instance]
def
measure_theory.probability_measure.to_finite_measure
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.probability_measure μ] :
Equations
- _ = _
def
measure_theory.measure.finite_at_filter
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → 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.
theorem
measure_theory.finite_at_filter_of_finite
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ]
(f : filter α) :
μ.finite_at_filter f
theorem
measure_theory.measure.finite_at_bot
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
@[class]
structure
measure_theory.locally_finite_measure
{α : Type u_1}
[measurable_space α]
[topological_space α] :
measure_theory.measure α → Prop
- finite_at_nhds : ∀ (x : α), μ.finite_at_filter (nhds x)
A measure is called locally finite if it is finite in some neighborhood of each point.
@[instance]
def
measure_theory.finite_measure.to_locally_finite_measure
{α : Type u_1}
[measurable_space α]
[topological_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ] :
Equations
- _ = _
theorem
measure_theory.measure.finite_at_nhds
{α : Type u_1}
[measurable_space α]
[topological_space α]
(μ : measure_theory.measure α)
[measure_theory.locally_finite_measure μ]
(x : α) :
μ.finite_at_filter (nhds x)
theorem
measure_theory.measure.finite_at_filter.filter_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α} :
f ≤ g → μ.finite_at_filter g → μ.finite_at_filter f
theorem
measure_theory.measure.finite_at_filter.inf_of_left
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α} :
μ.finite_at_filter f → μ.finite_at_filter (f ⊓ g)
theorem
measure_theory.measure.finite_at_filter.inf_of_right
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α} :
μ.finite_at_filter g → μ.finite_at_filter (f ⊓ g)
@[simp]
theorem
measure_theory.measure.finite_at_filter.inf_ae_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : filter α} :
μ.finite_at_filter (f ⊓ μ.ae) ↔ μ.finite_at_filter f
theorem
measure_theory.measure.finite_at_filter.filter_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α} :
f ⊓ μ.ae ≤ g → μ.finite_at_filter g → μ.finite_at_filter f
theorem
measure_theory.measure.finite_at_filter.measure_mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{f : filter α} :
μ ≤ ν → ν.finite_at_filter f → μ.finite_at_filter f
theorem
measure_theory.measure.finite_at_filter.mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{f g : filter α} :
f ≤ g → μ ≤ ν → ν.finite_at_filter g → μ.finite_at_filter f
theorem
measure_theory.measure.finite_at_filter.eventually
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : filter α} :
μ.finite_at_filter f → (∀ᶠ (s : set α) in f.lift' set.powerset, ⇑μ s < ⊤)
theorem
measure_theory.measure.finite_at_filter.filter_sup
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α} :
μ.finite_at_filter f → μ.finite_at_filter g → μ.finite_at_filter (f ⊔ g)
theorem
measure_theory.measure.finite_at_nhds_within
{α : Type u_1}
[measurable_space α]
[topological_space α]
(μ : measure_theory.measure α)
[measure_theory.locally_finite_measure μ]
(x : α)
(s : set α) :
μ.finite_at_filter (nhds_within x s)
@[simp]
theorem
measure_theory.measure.finite_at_principal
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
μ.finite_at_filter (filter.principal s) ↔ ⇑μ s < ⊤
def
is_null_measurable
{α : Type u_1}
[measurable_space α] :
measure_theory.measure α → set α → Prop
A set is null measurable if it is the union of a null set and a measurable set.
Equations
- is_null_measurable μ s = ∃ (t z : set α), s = t ∪ z ∧ is_measurable t ∧ ⇑μ z = 0
theorem
is_null_measurable_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
is_null_measurable μ s ↔ ∃ (t : set α), t ⊆ s ∧ is_measurable t ∧ ⇑μ (s \ t) = 0
theorem
is_null_measurable_measure_eq
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
is_measurable.is_null_measurable
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
{s : set α} :
is_measurable s → is_null_measurable μ s
theorem
is_null_measurable_of_complete
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[c : μ.is_complete]
{s : set α} :
is_null_measurable μ s ↔ is_measurable s
theorem
is_null_measurable.union_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s z : set α} :
is_null_measurable μ s → ⇑μ z = 0 → is_null_measurable μ (s ∪ z)
theorem
null_is_null_measurable
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{z : set α} :
⇑μ z = 0 → is_null_measurable μ z
theorem
is_null_measurable.Union_nat
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α} :
(∀ (i : ℕ), is_null_measurable μ (s i)) → is_null_measurable μ (set.Union s)
theorem
is_measurable.diff_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s z : set α} :
is_measurable s → ⇑μ z = 0 → is_null_measurable μ (s \ z)
theorem
is_null_measurable.diff_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s z : set α} :
is_null_measurable μ s → ⇑μ z = 0 → is_null_measurable μ (s \ z)
theorem
is_null_measurable.compl
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
is_null_measurable μ s → is_null_measurable μ sᶜ
The measurable space of all null measurable sets.
Equations
- null_measurable μ = {is_measurable := is_null_measurable μ, is_measurable_empty := _, is_measurable_compl := _, is_measurable_Union := _}
Given a measure we can complete it to a (complete) measure on all null measurable sets.
Equations
- completion μ = {to_outer_measure := μ.to_outer_measure, m_Union := _, trimmed := _}
@[instance]
Equations
- _ = _
@[class]
- 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
The tactic exact volume, to be used in optional (auto_param) arguments.
theorem
is_compact.finite_measure_of_nhds_within
{α : Type u_1}
[topological_space α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
is_compact s → (∀ (a : α), a ∈ s → μ.finite_at_filter (nhds_within a s)) → ⇑μ s < ⊤
theorem
is_compact.finite_measure
{α : Type u_1}
[topological_space α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
[measure_theory.locally_finite_measure μ] :
is_compact s → ⇑μ s < ⊤
theorem
is_compact.measure_zero_of_nhds_within
{α : Type u_1}
[topological_space α]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
is_compact s → (∀ (a : α), a ∈ s → (∃ (t : set α) (H : t ∈ nhds_within a s), ⇑μ t = 0)) → ⇑μ s = 0
theorem
metric.bounded.finite_measure
{α : Type u_1}
[metric_space α]
[proper_space α]
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ]
{s : set α} :
metric.bounded s → ⇑μ s < ⊤