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 ℝ≥0∞.
We introduce the following typeclasses for measures:
probability_measure μ:μ univ = 1;finite_measure μ:μ univ < ∞;sigma_finite μ: there exists a countable collection of measurable sets that coverunivwhereμis finite;locally_finite_measure μ:∀ x, ∃ s ∈ 𝓝 x, μ s < ∞;has_no_atoms μ:∀ x, μ {x} = 0; possibly should be redefined as∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s.
Given a measure, the null sets are the sets where μ s = 0, where μ denotes the corresponding
outer measure (so s might not be measurable). We can then define the completion of μ as the
measure on the least σ-algebra that also contains all null sets, by defining the measure to be 0
on the null sets.
Main statements #
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.
To prove that two measures are equal, there are multiple options:
ext: two measures are equal if they are equal on all measurable sets.ext_of_generate_from_of_Union: two measures are equal if they are equal on a π-system generating the measurable sets, if the π-system contains a spanning increasing sequence of sets where the measures take finite value (in particular the measures are σ-finite). This is a special case of the more generalext_of_generate_from_of_coverext_of_generate_finite: two finite measures are equal if they are equal on a π-system generating the measurable sets. This is a special case ofext_of_generate_from_of_UnionusingC ∪ {univ}, but is easier to work with.
A measure_space is a class that is a measurable space with a canonical measure.
The measure is denoted volume.
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 : ℕ), measurable_set (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.
@[protected, 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 α → ℝ≥0∞, coe := λ (m : measure_theory.measure α), ⇑(m.to_outer_measure)}
General facts about measures #
def
measure_theory.measure.of_measurable
{α : Type u_1}
[measurable_space α]
(m : Π (s : set α), measurable_set s → ℝ≥0∞)
(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) _) :
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 → ℝ≥0∞}
{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
@[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 α} :
@[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_infi'
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(s : set α) :
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) :
s.nonempty
theorem
measure_theory.measure_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : 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) :
theorem
measure_theory.measure_mono_top
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : s₁ ⊆ s₂)
(h₁ : ⇑μ s₁ = ⊤) :
theorem
measure_theory.exists_measurable_superset
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(s : set α) :
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 α]
{ι : Type u_2}
[encodable ι]
(μ : ι → measure_theory.measure α)
(s : set α) :
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.
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.
Equations
theorem
measure_theory.subset_to_measurable
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(s : set α) :
@[simp]
theorem
measure_theory.measurable_set_to_measurable
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(s : set α) :
@[simp]
theorem
measure_theory.measure_to_measurable
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(s : set α) :
⇑μ (measure_theory.to_measurable μ s) = ⇑μ s
theorem
measure_theory.exists_measurable_superset_of_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(h : ⇑μ s = 0) :
theorem
measure_theory.exists_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}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[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_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) < ⊤) :
theorem
measure_theory.measure_Union_null
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable β]
{s : β → set α} :
theorem
measure_theory.measure_Union_null_iff
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α} :
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 α} :
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_null_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
The almost everywhere filter #
def
measure_theory.measure.ae
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
filter α
The “almost everywhere” filter of co-null sets.
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.frequently_ae_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop} :
theorem
measure_theory.frequently_ae_mem_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_of_all
{α : Type u_1}
[measurable_space α]
{p : α → Prop}
(μ : measure_theory.measure α) :
(∀ (a : α), p a) → (∀ᵐ (a : α) ∂μ, p a)
@[protected, instance]
def
measure_theory.ae_is_measurably_generated
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
@[protected, instance]
def
measure_theory.measure.ae.countable_Inter_filter
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.ae_imp_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop}
{q : Prop} :
(∀ᵐ (x : α) ∂μ, q → p x) ↔ q → (∀ᵐ (x : α) ∂μ, p x)
theorem
measure_theory.ae_all_iff
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{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} :
theorem
measure_theory.ae_eq_refl
{α : Type u_1}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
(f : α → δ) :
theorem
measure_theory.ae_eq_symm
{α : Type u_1}
{δ : Type u_4}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : α → δ}
(h : f =ᵐ[μ] g) :
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) :
@[simp]
theorem
measure_theory.ae_eq_empty
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.ae_le_set
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
@[simp]
theorem
measure_theory.union_ae_eq_right
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.diff_ae_eq_self
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.ae_eq_set
{α : 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 α}
(H : 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) :
Alias of measure_mono_ae.
theorem
measure_theory.measure_congr
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(H : s =ᵐ[μ] t) :
If two sets are equal modulo a set of measure zero, then μ s = μ t.
@[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.
The tactic exact volume, to be used in optional (auto_param) arguments.
theorem
measure_theory.measure_Union
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable β]
{f : β → set α}
(hn : pairwise (disjoint on f))
(h : ∀ (i : β), measurable_set (f i)) :
theorem
measure_theory.measure_union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(hd : disjoint s₁ s₂)
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂) :
theorem
measure_theory.measure_bUnion
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set β}
{f : β → set α}
(hs : s.countable)
(hd : s.pairwise_on (disjoint on f))
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
theorem
measure_theory.measure_sUnion
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{S : set (set α)}
(hs : S.countable)
(hd : S.pairwise_on disjoint)
(h : ∀ (s : set α), s ∈ S → measurable_set s) :
theorem
measure_theory.measure_bUnion_finset
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
{s : finset ι}
{f : ι → set α}
(hd : ↑s.pairwise_on (disjoint on f))
(hm : ∀ (b : ι), b ∈ s → measurable_set (f b)) :
theorem
measure_theory.tsum_measure_preimage_singleton
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set β}
(hs : s.countable)
{f : α → β}
(hf : ∀ (y : β), y ∈ s → measurable_set (f ⁻¹' {y})) :
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 : α → β}
(hf : ∀ (y : β), y ∈ s → measurable_set (f ⁻¹' {y})) :
If s is a finset, then the measure of its preimage can be found as the sum of measures
of the fibers f ⁻¹' {y}.
theorem
measure_theory.measure_diff_null'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : ⇑μ (s₁ ∩ s₂) = 0) :
theorem
measure_theory.measure_diff_null
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : ⇑μ s₂ = 0) :
theorem
measure_theory.measure_diff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : s₂ ⊆ s₁)
(h₁ : measurable_set s₁)
(h₂ : measurable_set s₂)
(h_fin : ⇑μ s₂ < ⊤) :
theorem
measure_theory.measure_compl
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(h₁ : measurable_set s)
(h_fin : ⇑μ s < ⊤) :
theorem
measure_theory.sum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
{s : finset ι}
{t : ι → set α}
(h : ∀ (i : ι), i ∈ s → measurable_set (t i))
(H : ↑s.pairwise_on (disjoint on t)) :
theorem
measure_theory.tsum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ι → set α}
(hs : ∀ (i : ι), measurable_set (s i))
(H : pairwise (disjoint on s)) :
theorem
measure_theory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(μ : measure_theory.measure α)
{s : ι → set α}
(hs : ∀ (i : ι), measurable_set (s i))
(H : ⇑μ set.univ < ∑' (i : ι), ⇑μ (s i)) :
Pigeonhole principle for measure spaces: if ∑' i, μ (s i) > μ univ, then
one of the intersections s i ∩ s j is not empty.
theorem
measure_theory.exists_nonempty_inter_of_measure_univ_lt_sum_measure
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(μ : measure_theory.measure α)
{s : finset ι}
{t : ι → set α}
(h : ∀ (i : ι), i ∈ s → measurable_set (t i))
(H : ⇑μ set.univ < ∑ (i : ι) in s, ⇑μ (t i)) :
Pigeonhole principle for measure spaces: if s is a finset and
∑ i in s, μ (t i) > μ univ, then one of the intersections t i ∩ t j is not empty.
theorem
measure_theory.measure_Union_eq_supr
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(h : ∀ (i : ι), measurable_set (s i))
(hd : directed has_subset.subset s) :
Continuity from below: the measure of the union of a directed sequence of measurable sets is the supremum of the measures.
theorem
measure_theory.measure_bUnion_eq_supr
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ι → set α}
{t : set ι}
(ht : t.countable)
(h : ∀ (i : ι), i ∈ t → measurable_set (s i))
(hd : directed_on (has_subset.subset on s) t) :
theorem
measure_theory.measure_Inter_eq_infi
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(h : ∀ (i : ι), measurable_set (s i))
(hd : directed superset s)
(hfin : ∃ (i : ι), ⇑μ (s i) < ⊤) :
Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the infimum of the measures.
theorem
measure_theory.measure_eq_inter_diff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
measure_theory.measure_union_add_inter
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
measure_theory.tendsto_measure_Union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α}
(hs : ∀ (n : ℕ), measurable_set (s n))
(hm : monotone s) :
filter.tendsto (⇑μ ∘ s) filter.at_top (𝓝 (⇑μ (⋃ (n : ℕ), s n)))
Continuity from below: the measure of the union of an increasing sequence of measurable sets is the limit of the measures.
theorem
measure_theory.tendsto_measure_Inter
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α}
(hs : ∀ (n : ℕ), measurable_set (s n))
(hm : ∀ ⦃n m : ℕ⦄, n ≤ m → s m ⊆ s n)
(hf : ∃ (i : ℕ), ⇑μ (s i) < ⊤) :
filter.tendsto (⇑μ ∘ s) filter.at_top (𝓝 (⇑μ (⋂ (n : ℕ), s n)))
Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.
theorem
measure_theory.measure_limsup_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α}
(hs : ∀ (i : ℕ), measurable_set (s i))
(hs' : ∑' (i : ℕ), ⇑μ (s i) ≠ ⊤) :
⇑μ (filter.at_top.limsup s) = 0
One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of measurable sets such that ∑ μ sᵢ exists, then the limit superior of the sᵢ is a null set.
theorem
measure_theory.measure_if
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{x : β}
{t : set β}
{s : set α}
{μ : measure_theory.measure α} :
def
measure_theory.outer_measure.to_measure
{α : Type u_1}
[ms : measurable_space α]
(m : measure_theory.outer_measure α)
(h : ms ≤ m.caratheodory) :
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 : measurable_set 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}
[ms : measurable_space α]
(m : measure_theory.outer_measure α)
(h : ms ≤ m.caratheodory) :
(m.to_measure h).to_outer_measure = m.trim
@[simp]
theorem
measure_theory.to_measure_apply
{α : Type u_1}
[ms : measurable_space α]
(m : measure_theory.outer_measure α)
(h : ms ≤ m.caratheodory)
{s : set α}
(hs : measurable_set s) :
⇑(m.to_measure h) s = ⇑m s
theorem
measure_theory.le_to_measure_apply
{α : Type u_1}
[ms : measurable_space α]
(m : measure_theory.outer_measure α)
(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 _ = μ
@[protected]
theorem
measure_theory.measure.caratheodory
{α : Type u_1}
[measurable_space α]
{s t : set α}
(μ : measure_theory.measure α)
(hs : measurable_set s) :
The ℝ≥0∞-module of measures #
@[protected, 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, norm_cast]
theorem
measure_theory.measure.eq_zero_of_not_nonempty
{α : Type u_1}
[measurable_space α]
(h : ¬nonempty α)
(μ : measure_theory.measure α) :
μ = 0
@[protected, instance]
Equations
@[protected, 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, norm_cast]
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 α) :
@[protected, instance]
@[protected, instance]
Equations
- measure_theory.measure.has_scalar = {smul := λ (c : ℝ≥0∞) (μ : 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 : ℝ≥0∞)
(μ : measure_theory.measure α) :
(c • μ).to_outer_measure = c • μ.to_outer_measure
@[simp, norm_cast]
theorem
measure_theory.measure.coe_smul
{α : Type u_1}
[measurable_space α]
(c : ℝ≥0∞)
(μ : measure_theory.measure α) :
theorem
measure_theory.measure.smul_apply
{α : Type u_1}
[measurable_space α]
(c : ℝ≥0∞)
(μ : measure_theory.measure α)
(s : set α) :
@[protected, instance]
The complete lattice of measures #
@[protected, instance]
Equations
- measure_theory.measure.partial_order = {le := λ (m₁ m₂ : measure_theory.measure α), ∀ (s : set α), measurable_set s → ⇑m₁ s ≤ ⇑m₂ s, lt := preorder.lt._default (λ (m₁ m₂ : measure_theory.measure α), ∀ (s : set α), measurable_set 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 α} :
@[protected]
theorem
measure_theory.measure.add_le_add_left
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α}
(ν : measure_theory.measure α)
(hμ : μ₁ ≤ μ₂) :
@[protected]
theorem
measure_theory.measure.add_le_add_right
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ : measure_theory.measure α}
(hμ : μ₁ ≤ μ₂)
(ν : measure_theory.measure α) :
@[protected]
theorem
measure_theory.measure.add_le_add
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ ν₁ ν₂ : measure_theory.measure α}
(hμ : μ₁ ≤ μ₂)
(hν : ν₁ ≤ ν₂) :
@[protected]
theorem
measure_theory.measure.le_add_left
{α : Type u_1}
[measurable_space α]
{μ ν ν' : measure_theory.measure α}
(h : μ ≤ ν) :
@[protected]
theorem
measure_theory.measure.le_add_right
{α : Type u_1}
[measurable_space α]
{μ ν ν' : measure_theory.measure α}
(h : μ ≤ ν) :
theorem
measure_theory.measure.Inf_caratheodory
{α : Type u_1}
[measurable_space α]
{m : set (measure_theory.measure α)}
(s : set α)
(hs : measurable_set s) :
@[protected, instance]
Equations
theorem
measure_theory.measure.Inf_apply
{α : Type u_1}
[measurable_space α]
{s : set α}
{m : set (measure_theory.measure α)}
(hs : measurable_set s) :
@[protected, instance]
Equations
- measure_theory.measure.complete_semilattice_Inf = {le := partial_order.le measure_theory.measure.partial_order, lt := partial_order.lt measure_theory.measure.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, Inf := Inf measure_theory.measure.has_Inf, Inf_le := _, le_Inf := _}
@[protected, instance]
Equations
- measure_theory.measure.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), le := complete_lattice.le (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), lt := complete_lattice.lt (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), 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_complete_semilattice_Inf (measure_theory.measure α)), inf_le_left := _, inf_le_right := _, le_inf := _, top := complete_lattice.top (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), le_top := _, bot := 0, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), Inf_le := _, le_Inf := _}
@[protected]
theorem
measure_theory.measure.zero_le
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
0 ≤ μ
theorem
measure_theory.measure.nonpos_iff_eq_zero'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.measure_univ_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
Pushforward and pullback #
def
measure_theory.measure.lift_linear
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : measure_theory.outer_measure α →ₗ[ℝ≥0∞] measure_theory.outer_measure β)
(hf : ∀ (μ : measure_theory.measure α), _inst_2 ≤ (⇑f μ.to_outer_measure).caratheodory) :
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 β]
{μ : measure_theory.measure α}
{f : measure_theory.outer_measure α →ₗ[ℝ≥0∞] measure_theory.outer_measure β}
(hf : ∀ (μ : measure_theory.measure α), _inst_2 ≤ (⇑f μ.to_outer_measure).caratheodory)
{s : set β}
(hs : measurable_set 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 β]
{μ : measure_theory.measure α}
{f : measure_theory.outer_measure α →ₗ[ℝ≥0∞] measure_theory.outer_measure β}
(hf : ∀ (μ : measure_theory.measure α), _inst_2 ≤ (⇑f μ.to_outer_measure).caratheodory)
(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 β]
(f : α → β) :
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 β}
(hs : measurable_set s) :
We can evaluate the pushforward on measurable sets. For non-measurable sets, see
measure_theory.measure.le_map_apply and measurable_equiv.map_apply.
theorem
measure_theory.measure.map_of_not_measurable
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ¬measurable f) :
⇑(measure_theory.measure.map f) μ = 0
@[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 : α → β}
(hg : measurable g)
(hf : measurable f) :
⇑(measure_theory.measure.map g) (⇑(measure_theory.measure.map f) μ) = ⇑(measure_theory.measure.map (g ∘ f)) μ
theorem
measure_theory.measure.map_mono
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ ν : measure_theory.measure α}
(f : α → β)
(h : μ ≤ ν) :
⇑(measure_theory.measure.map f) μ ≤ ⇑(measure_theory.measure.map f) ν
theorem
measure_theory.measure.le_map_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
(s : set β) :
Even if s is not measurable, we can bound map f μ s from below.
See also measurable_equiv.map_apply.
theorem
measure_theory.measure.preimage_null_of_map_null
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{s : set β}
(hs : ⇑(⇑(measure_theory.measure.map f) μ) s = 0) :
Even if s is not measurable, map f μ s = 0 implies that μ (f ⁻¹' s) = 0.
theorem
measure_theory.measure.tendsto_ae_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f) :
filter.tendsto f μ.ae (⇑(measure_theory.measure.map f) μ).ae
def
measure_theory.measure.comap
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β) :
Pullback of a measure. If f sends each measurable set to a measurable set, then for each
measurable set s we have comap f μ s = μ (f '' s).
Equations
- measure_theory.measure.comap f = dite (function.injective f ∧ ∀ (s : set α), measurable_set s → measurable_set (f '' s)) (λ (hf : function.injective f ∧ ∀ (s : set α), measurable_set s → measurable_set (f '' s)), measure_theory.measure.lift_linear (measure_theory.outer_measure.comap f) _) (λ (hf : ¬(function.injective f ∧ ∀ (s : set α), measurable_set s → measurable_set (f '' s))), 0)
theorem
measure_theory.measure.comap_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{s : set α}
(f : α → β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measurable_set (f '' s))
(μ : measure_theory.measure β)
(hs : measurable_set s) :
Restricting a measure #
Restrict a measure μ to a set s as an ℝ≥0∞-linear map.
def
measure_theory.measure.restrict
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(s : set α) :
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 α}
(ht : measurable_set t) :
If t is a measurable set, then the measure of t with respect to the restriction of
the measure to s equals the outer measure of t ∩ s. An alternate version requiring that s
be measurable instead of t exists as measure.restrict_apply'.
theorem
measure_theory.measure.restrict_eq_self
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(h_meas_t : measurable_set t)
(h : t ⊆ s) :
theorem
measure_theory.measure.restrict_apply_self
{α : Type u_1}
[measurable_space α]
{s : set α}
(μ : measure_theory.measure α)
(h_meas_s : measurable_set s) :
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 : ℝ≥0∞)
(μ : measure_theory.measure α)
(s : set α) :
@[simp]
theorem
measure_theory.measure.restrict_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_apply_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(ht : measurable_set t) :
theorem
measure_theory.measure.measure_inter_eq_zero_of_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(h : ⇑(μ.restrict s) t = 0) :
theorem
measure_theory.measure.restrict_apply_eq_zero'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s) :
@[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_eq_self_of_measurable_subset
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(ht : measurable_set t)
(t_subset : t ⊆ s) :
theorem
measure_theory.measure.restrict_union_apply
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s s' t : set α}
(h : disjoint (t ∩ s) (t ∩ s'))
(hs : measurable_set s)
(hs' : measurable_set s')
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_union
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(h : disjoint s t)
(hs : measurable_set s)
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_union_add_inter
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(ht : measurable_set t) :
@[simp]
theorem
measure_theory.measure.restrict_add_restrict_compl
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
@[simp]
theorem
measure_theory.measure.restrict_compl_add_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
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}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(hd : pairwise (disjoint on s))
(hm : ∀ (i : ι), measurable_set (s i))
{t : set α}
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_Union_apply_eq_supr
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(hm : ∀ (i : ι), measurable_set (s i))
(hd : directed has_subset.subset s)
{t : set α}
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{s : set β}
(hs : measurable_set s) :
(⇑(measure_theory.measure.map f) μ).restrict s = ⇑(measure_theory.measure.map f) (μ.restrict (f ⁻¹' s))
theorem
measure_theory.measure.map_comap_subtype_coe
{α : Type u_1}
[measurable_space α]
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_mono
{α : Type u_1}
[measurable_space α]
⦃s s' : set α⦄
(hs : s ⊆ s')
⦃μ ν : measure_theory.measure α⦄
(hμν : μ ≤ ν) :
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 α} :
theorem
measure_theory.measure.restrict_congr_meas
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_congr_mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s t : set α}
(hs : s ⊆ t)
(hm : measurable_set s)
(h : μ.restrict t = ν.restrict t) :
theorem
measure_theory.measure.restrict_union_congr
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s t : set α}
(hsm : measurable_set s)
(htm : measurable_set t) :
If two measures agree on all measurable subsets of s and t, then they agree on all
measurable subsets of s ∪ t.
theorem
measure_theory.measure.restrict_finset_bUnion_congr
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s : finset ι}
{t : ι → set α}
(htm : ∀ (i : ι), i ∈ s → measurable_set (t i)) :
theorem
measure_theory.measure.restrict_Union_congr
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(hm : ∀ (i : ι), measurable_set (s i)) :
theorem
measure_theory.measure.restrict_bUnion_congr
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s : set ι}
{t : ι → set α}
(hc : s.countable)
(htm : ∀ (i : ι), i ∈ s → measurable_set (t i)) :
theorem
measure_theory.measure.restrict_sUnion_congr
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S : set (set α)}
(hc : S.countable)
(hm : ∀ (s : set α), s ∈ S → measurable_set s) :
theorem
measure_theory.measure.restrict_to_outer_measure_eq_to_outer_measure_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(h : measurable_set s) :
This lemma shows that restrict and to_outer_measure commute. Note that the LHS has a
restrict on measures and the RHS has a restrict on outer measures.
theorem
measure_theory.measure.restrict_Inf_eq_Inf_restrict
{α : Type u_1}
[measurable_space α]
{t : set α}
{m : set (measure_theory.measure α)}
(hm : m.nonempty)
(ht : measurable_set t) :
This lemma shows that Inf and restrict commute for measures.
theorem
measure_theory.measure.restrict_apply'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s) :
If s is a measurable set, then the outer measure of t with respect to the restriction of
the measure to s equals the outer measure of t ∩ s. This is an alternate version of
measure.restrict_apply, requiring that s is measurable instead of t.
theorem
measure_theory.measure.restrict_eq_self_of_subset_of_measurable
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(t_subset : t ⊆ s) :
Extensionality results #
theorem
measure_theory.measure.ext_iff_of_Union_eq_univ
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(hm : ∀ (i : ι), measurable_set (s i))
(hs : (⋃ (i : ι), s i) = set.univ) :
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using Union).
theorem
measure_theory.measure.ext_of_Union_eq_univ
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(hm : ∀ (i : ι), measurable_set (s i))
(hs : (⋃ (i : ι), s i) = set.univ) :
Alias of ext_iff_of_Union_eq_univ.
theorem
measure_theory.measure.ext_iff_of_bUnion_eq_univ
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S : set ι}
{s : ι → set α}
(hc : S.countable)
(hm : ∀ (i : ι), i ∈ S → measurable_set (s i))
(hs : (⋃ (i : ι) (H : i ∈ S), s i) = set.univ) :
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using bUnion).
theorem
measure_theory.measure.ext_of_bUnion_eq_univ
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S : set ι}
{s : ι → set α}
(hc : S.countable)
(hm : ∀ (i : ι), i ∈ S → measurable_set (s i))
(hs : (⋃ (i : ι) (H : i ∈ S), s i) = set.univ) :
Alias of ext_iff_of_bUnion_eq_univ.
theorem
measure_theory.measure.ext_iff_of_sUnion_eq_univ
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S : set (set α)}
(hc : S.countable)
(hm : ∀ (s : set α), s ∈ S → measurable_set s)
(hs : ⋃₀S = set.univ) :
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using sUnion).
theorem
measure_theory.measure.ext_of_sUnion_eq_univ
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S : set (set α)}
(hc : S.countable)
(hm : ∀ (s : set α), s ∈ S → measurable_set s)
(hs : ⋃₀S = set.univ) :
Alias of ext_iff_of_sUnion_eq_univ.
theorem
measure_theory.measure.ext_of_generate_from_of_cover
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S T : set (set α)}
(h_gen : _inst_1 = measurable_space.generate_from S)
(hc : T.countable)
(h_inter : is_pi_system S)
(hm : ∀ (t : set α), t ∈ T → measurable_set t)
(hU : ⋃₀T = set.univ)
(htop : ∀ (t : set α), t ∈ T → ⇑μ t < ⊤)
(ST_eq : ∀ (t : set α), t ∈ T → ∀ (s : set α), s ∈ S → ⇑μ (s ∩ t) = ⇑ν (s ∩ t))
(T_eq : ∀ (t : set α), t ∈ T → ⇑μ t = ⇑ν t) :
μ = ν
theorem
measure_theory.measure.ext_of_generate_from_of_cover_subset
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{S T : set (set α)}
(h_gen : _inst_1 = measurable_space.generate_from S)
(h_inter : is_pi_system S)
(h_sub : T ⊆ S)
(hc : T.countable)
(hU : ⋃₀T = set.univ)
(htop : ∀ (s : set α), s ∈ T → ⇑μ s < ⊤)
(h_eq : ∀ (s : set α), s ∈ S → ⇑μ s = ⇑ν s) :
μ = ν
Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on a increasing spanning sequence of sets in the π-system.
This lemma is formulated using sUnion.
theorem
measure_theory.measure.ext_of_generate_from_of_Union
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(C : set (set α))
(B : ℕ → set α)
(hA : _inst_1 = measurable_space.generate_from C)
(hC : is_pi_system C)
(h1B : (⋃ (i : ℕ), B i) = set.univ)
(h2B : ∀ (i : ℕ), B i ∈ C)
(hμB : ∀ (i : ℕ), ⇑μ (B i) < ⊤)
(h_eq : ∀ (s : set α), s ∈ C → ⇑μ s = ⇑ν s) :
μ = ν
Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on a increasing spanning sequence of sets in the π-system.
This lemma is formulated using Union.
finite_spanning_sets_in.ext is a reformulation of this lemma.
The dirac measure.
Equations
theorem
measure_theory.measure.le_dirac_apply
{α : Type u_1}
[measurable_space α]
{s : set α}
{a : α} :
s.indicator 1 a ≤ ⇑(measure_theory.measure.dirac a) s
@[simp]
theorem
measure_theory.measure.dirac_apply'
{α : Type u_1}
[measurable_space α]
{s : set α}
(a : α)
(hs : measurable_set s) :
⇑(measure_theory.measure.dirac a) s = s.indicator 1 a
@[simp]
theorem
measure_theory.measure.dirac_apply_of_mem
{α : Type u_1}
[measurable_space α]
{s : set α}
{a : α}
(h : a ∈ s) :
⇑(measure_theory.measure.dirac a) s = 1
@[simp]
theorem
measure_theory.measure.dirac_apply
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(a : α)
(s : set α) :
⇑(measure_theory.measure.dirac a) s = s.indicator 1 a
theorem
measure_theory.measure.map_dirac
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{f : α → β}
(hf : measurable f)
(a : α) :
def
measure_theory.measure.sum
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(f : ι → 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 _
theorem
measure_theory.measure.le_sum_apply
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(f : ι → measure_theory.measure α)
(s : set α) :
∑' (i : ι), ⇑(f i) s ≤ ⇑(measure_theory.measure.sum f) s
@[simp]
theorem
measure_theory.measure.sum_apply
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(f : ι → measure_theory.measure α)
{s : set α}
(hs : measurable_set s) :
⇑(measure_theory.measure.sum f) s = ∑' (i : ι), ⇑(f i) s
theorem
measure_theory.measure.le_sum
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(μ : ι → measure_theory.measure α)
(i : ι) :
μ i ≤ measure_theory.measure.sum μ
theorem
measure_theory.measure.restrict_Union
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α}
(hd : pairwise (disjoint on s))
(hm : ∀ (i : ι), measurable_set (s i)) :
μ.restrict (⋃ (i : ι), s i) = measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))
theorem
measure_theory.measure.restrict_Union_le
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
[encodable ι]
{s : ι → set α} :
μ.restrict (⋃ (i : ι), s i) ≤ measure_theory.measure.sum (λ (i : ι), μ.restrict (s i))
@[simp]
theorem
measure_theory.measure.sum_bool
{α : Type u_1}
[measurable_space α]
(f : bool → measure_theory.measure α) :
measure_theory.measure.sum f = f tt + f ff
@[simp]
theorem
measure_theory.measure.sum_cond
{α : Type u_1}
[measurable_space α]
(μ ν : measure_theory.measure α) :
measure_theory.measure.sum (λ (b : bool), cond b μ ν) = μ + ν
@[simp]
theorem
measure_theory.measure.restrict_sum
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
(μ : ι → measure_theory.measure α)
{s : set α}
(hs : measurable_set 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.le_count_apply
{α : Type u_1}
[measurable_space α]
{s : set α} :
∑' (i : ↥s), 1 ≤ ⇑measure_theory.measure.count s
theorem
measure_theory.measure.count_apply
{α : Type u_1}
[measurable_space α]
{s : set α}
(hs : measurable_set 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 α]
{s : set α}
(hs : s.infinite) :
count measure evaluates to infinity at infinite sets.
@[simp]
theorem
measure_theory.measure.count_apply_eq_top
{α : Type u_1}
[measurable_space α]
{s : set α}
[measurable_singleton_class α] :
@[simp]
theorem
measure_theory.measure.count_apply_lt_top
{α : Type u_1}
[measurable_space α]
{s : set α}
[measurable_singleton_class α] :
Absolute continuity #
def
measure_theory.measure.absolutely_continuous
{α : Type u_1}
[measurable_space α]
(μ ν : measure_theory.measure α) :
Prop
We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν,
if ν(A) = 0 implies that μ(A) = 0.
theorem
measure_theory.measure.absolutely_continuous_of_le
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ ≤ ν) :
μ ≪ ν
theorem
has_le.le.absolutely_continuous
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ ≤ ν) :
μ ≪ ν
Alias of absolutely_continuous_of_le.
theorem
measure_theory.measure.absolutely_continuous_of_eq
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ = ν) :
μ ≪ ν
theorem
eq.absolutely_continuous
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ = ν) :
μ ≪ ν
Alias of absolutely_continuous_of_eq.
theorem
measure_theory.measure.absolutely_continuous.mk
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : ∀ ⦃s : set α⦄, measurable_set s → ⇑ν s = 0 → ⇑μ s = 0) :
μ ≪ ν
@[protected]
theorem
measure_theory.measure.absolutely_continuous.refl
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
μ ≪ μ
@[protected]
theorem
measure_theory.measure.absolutely_continuous.rfl
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
μ ≪ μ
@[protected]
theorem
measure_theory.measure.absolutely_continuous.trans
{α : Type u_1}
[measurable_space α]
{μ₁ μ₂ μ₃ : measure_theory.measure α}
(h1 : μ₁ ≪ μ₂)
(h2 : μ₂ ≪ μ₃) :
μ₁ ≪ μ₃
@[protected]
theorem
measure_theory.measure.absolutely_continuous.map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ ν : measure_theory.measure α}
(h : μ ≪ ν)
(f : α → β) :
⇑(measure_theory.measure.map f) μ ≪ ⇑(measure_theory.measure.map f) ν
theorem
measure_theory.measure.ae_le_iff_absolutely_continuous
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
theorem
has_le.le.absolutely_continuous_of_ae
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
Alias of ae_le_iff_absolutely_continuous.
theorem
measure_theory.measure.absolutely_continuous.ae_le
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
Alias of ae_le_iff_absolutely_continuous.
Alias of absolutely_continuous.ae_le.
theorem
measure_theory.measure.absolutely_continuous.ae_eq
{α : Type u_1}
{δ : Type u_4}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ ≪ ν)
{f g : α → δ}
(h' : f =ᵐ[ν] g) :
Quasi measure preserving maps (a.k.a. non-singular maps) #
structure
measure_theory.measure.quasi_measure_preserving
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β)
(μa : measure_theory.measure α . "volume_tac")
(μb : measure_theory.measure β . "volume_tac") :
Prop
- measurable : measurable f
- absolutely_continuous : ⇑(measure_theory.measure.map f) μa ≪ μb
A map f : α → β is said to be quasi measure preserving (a.k.a. non-singular) w.r.t. measures
μa and μb if it is measurable and μb s = 0 implies μa (f ⁻¹' s) = 0.
@[protected]
theorem
measure_theory.measure.quasi_measure_preserving.id
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
theorem
measure_theory.measure.quasi_measure_preserving.mono_left
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μa μa' : measure_theory.measure α}
{μb : measure_theory.measure β}
{f : α → β}
(h : measure_theory.measure.quasi_measure_preserving f μa μb)
(ha : μa' ≪ μa) :
theorem
measure_theory.measure.quasi_measure_preserving.mono_right
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μa : measure_theory.measure α}
{μb μb' : measure_theory.measure β}
{f : α → β}
(h : measure_theory.measure.quasi_measure_preserving f μa μb)
(ha : μb ≪ μb') :
theorem
measure_theory.measure.quasi_measure_preserving.mono
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μa μa' : measure_theory.measure α}
{μb μb' : measure_theory.measure β}
{f : α → β}
(ha : μa' ≪ μa)
(hb : μb ≪ μb')
(h : measure_theory.measure.quasi_measure_preserving f μa μb) :
@[protected]
theorem
measure_theory.measure.quasi_measure_preserving.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[measurable_space α]
[measurable_space β]
[measurable_space γ]
{μa : measure_theory.measure α}
{μb : measure_theory.measure β}
{μc : measure_theory.measure γ}
{g : β → γ}
{f : α → β}
(hg : measure_theory.measure.quasi_measure_preserving g μb μc)
(hf : measure_theory.measure.quasi_measure_preserving f μa μb) :
measure_theory.measure.quasi_measure_preserving (g ∘ f) μa μc
@[protected]
theorem
measure_theory.measure.quasi_measure_preserving.iterate
{α : Type u_1}
[measurable_space α]
{μa : measure_theory.measure α}
{f : α → α}
(hf : measure_theory.measure.quasi_measure_preserving f μa μa)
(n : ℕ) :
theorem
measure_theory.measure.quasi_measure_preserving.ae_map_le
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μa : measure_theory.measure α}
{μb : measure_theory.measure β}
{f : α → β}
(h : measure_theory.measure.quasi_measure_preserving f μa μb) :
(⇑(measure_theory.measure.map f) μa).ae ≤ μb.ae
theorem
measure_theory.measure.quasi_measure_preserving.tendsto_ae
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μa : measure_theory.measure α}
{μb : measure_theory.measure β}
{f : α → β}
(h : measure_theory.measure.quasi_measure_preserving f μa μb) :
filter.tendsto f μa.ae μb.ae
theorem
measure_theory.measure.quasi_measure_preserving.ae
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μa : measure_theory.measure α}
{μb : measure_theory.measure β}
{f : α → β}
(h : measure_theory.measure.quasi_measure_preserving f μa μb)
{p : β → Prop}
(hg : ∀ᵐ (x : β) ∂μb, p x) :
∀ᵐ (x : α) ∂μa, p (f x)
theorem
measure_theory.measure.quasi_measure_preserving.ae_eq
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
[measurable_space α]
[measurable_space β]
{μa : measure_theory.measure α}
{μb : measure_theory.measure β}
{f : α → β}
(h : measure_theory.measure.quasi_measure_preserving f μa μb)
{g₁ g₂ : β → δ}
(hg : g₁ =ᵐ[μb] g₂) :
The cofinite filter #
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} :
@[simp]
theorem
measure_theory.ae_eq_bot
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.ae_ne_bot
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
theorem
measure_theory.ae_mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ ≤ ν) :
theorem
measure_theory.mem_ae_map_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{s : set β}
(hs : measurable_set s) :
theorem
measure_theory.mem_ae_of_mem_ae_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{s : set β}
(hs : s ∈ (⇑(measure_theory.measure.map f) μ).ae) :
theorem
measure_theory.ae_map_iff
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{p : β → Prop}
(hp : measurable_set {x : β | p x}) :
(∀ᵐ (y : β) ∂⇑(measure_theory.measure.map f) μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
theorem
measure_theory.ae_of_ae_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{p : β → Prop}
(h : ∀ᵐ (y : β) ∂⇑(measure_theory.measure.map f) μ, p y) :
∀ᵐ (x : α) ∂μ, p (f x)
theorem
measure_theory.ae_map_mem_range
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(f : α → β)
(hf : measurable_set (set.range f))
(μ : measure_theory.measure α) :
∀ᵐ (x : β) ∂⇑(measure_theory.measure.map f) μ, x ∈ set.range f
theorem
measure_theory.ae_restrict_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{p : α → Prop}
(hp : measurable_set {x : α | p x}) :
theorem
measure_theory.ae_imp_of_ae_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{p : α → Prop}
(h : ∀ᵐ (x : α) ∂μ.restrict s, p x) :
∀ᵐ (x : α) ∂μ, x ∈ s → p x
theorem
measure_theory.ae_restrict_iff'
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{p : α → Prop}
(hp : measurable_set s) :
theorem
measure_theory.ae_restrict_of_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
{p : α → Prop}
(h : ∀ᵐ (x : α) ∂μ, p x) :
∀ᵐ (x : α) ∂μ.restrict s, p x
theorem
measure_theory.ae_restrict_of_ae_restrict_of_subset
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
{p : α → Prop}
(hst : s ⊆ t)
(h : ∀ᵐ (x : α) ∂μ.restrict t, p x) :
∀ᵐ (x : α) ∂μ.restrict s, p x
theorem
measure_theory.ae_smul_measure
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop}
(h : ∀ᵐ (x : α) ∂μ, p x)
(c : ℝ≥0∞) :
∀ᵐ (x : α) ∂c • μ, p x
theorem
measure_theory.ae_smul_measure_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop}
{c : ℝ≥0∞}
(hc : c ≠ 0) :
theorem
measure_theory.ae_add_measure_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{p : α → Prop}
{ν : measure_theory.measure α} :
theorem
measure_theory.ae_eq_comp'
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{ν : measure_theory.measure β}
{f : α → β}
{g g' : β → δ}
(hf : measurable f)
(h : g =ᵐ[ν] g')
(h2 : ⇑(measure_theory.measure.map f) μ ≪ ν) :
theorem
measure_theory.ae_eq_comp
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
[measurable_space α]
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
{g g' : β → δ}
(hf : measurable f)
(h : g =ᵐ[⇑(measure_theory.measure.map f) μ] g') :
theorem
measure_theory.le_ae_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
@[simp]
theorem
measure_theory.ae_restrict_eq
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set 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.self_mem_ae_restrict
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.ae_eventually_not_mem
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : ℕ → set α}
(hs : ∀ (i : ℕ), measurable_set (s i))
(hs' : ∑' (i : ℕ), ⇑μ (s i) ≠ ⊤) :
∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in filter.at_top, x ∉ s n
A version of the Borel-Cantelli lemma: if sᵢ is a sequence of measurable sets such that
∑ μ sᵢ exists, then for almost all x, x does not belong to almost all sᵢ.
theorem
measure_theory.mem_ae_dirac_iff
{α : Type u_1}
[measurable_space α]
{s : set α}
{a : α}
(hs : measurable_set s) :
s ∈ (measure_theory.measure.dirac a).ae ↔ a ∈ s
theorem
measure_theory.ae_dirac_iff
{α : Type u_1}
[measurable_space α]
{a : α}
{p : α → Prop}
(hp : measurable_set {x : α | p x}) :
(∀ᵐ (x : α) ∂measure_theory.measure.dirac a, p x) ↔ p a
@[simp]
theorem
measure_theory.ae_dirac_eq
{α : Type u_1}
[measurable_space α]
[measurable_singleton_class α]
(a : α) :
(measure_theory.measure.dirac a).ae = pure a
theorem
measure_theory.ae_eq_dirac'
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
[measurable_singleton_class β]
{a : α}
{f : α → β}
(hf : measurable f) :
f =ᵐ[measure_theory.measure.dirac a] function.const α (f a)
theorem
measure_theory.ae_eq_dirac
{α : Type u_1}
{δ : Type u_4}
[measurable_space α]
[measurable_singleton_class α]
{a : α}
(f : α → δ) :
f =ᵐ[measure_theory.measure.dirac a] function.const α (f a)
theorem
measure_theory.restrict_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(h : s ≤ᵐ[μ] t) :
theorem
measure_theory.restrict_congr_set
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s t : set α}
(H : s =ᵐ[μ] t) :
@[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.
@[protected, instance]
@[class]
structure
measure_theory.finite_measure
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
Prop
A measure μ is called finite if μ univ < ∞.
@[protected, instance]
def
measure_theory.restrict.finite_measure
{α : Type u_1}
[measurable_space α]
{s : set α}
(μ : measure_theory.measure α)
[hs : fact (⇑μ s < ⊤)] :
@[class]
structure
measure_theory.has_no_atoms
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
Prop
Measure μ has no atoms if the measure of each singleton is zero.
NB: Wikipedia assumes that for any measurable set s with positive μ-measure,
there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0,
the converse is not true.
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 α) :
def
measure_theory.measure_univ_nnreal
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
The measure of the whole space with respect to a finite measure, considered as ℝ≥0.
Equations
@[simp]
theorem
measure_theory.coe_measure_univ_nnreal
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ] :
@[protected, instance]
@[simp]
@[simp]
theorem
measure_theory.measure_univ_nnreal_eq_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.finite_measure μ] :
measure_theory.measure_univ_nnreal μ = 0 ↔ μ = 0
theorem
measure_theory.measure_univ_nnreal_pos
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.finite_measure μ]
(hμ : μ ≠ 0) :
theorem
measure_theory.measure.le_of_add_le_add_left
{α : Type u_1}
[measurable_space α]
{μ ν₁ ν₂ : measure_theory.measure α}
[measure_theory.finite_measure μ]
(A2 : μ + ν₁ ≤ μ + ν₂) :
ν₁ ≤ ν₂
le_of_add_le_add_left is normally applicable to ordered_cancel_add_comm_monoid,
but it holds for measures with the additional assumption that μ is finite.
@[protected, instance]
def
measure_theory.probability_measure.to_finite_measure
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.probability_measure μ] :
theorem
measure_theory.probability_measure.ne_zero
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.probability_measure μ] :
μ ≠ 0
theorem
measure_theory.measure_countable
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
[measure_theory.has_no_atoms μ]
(h : s.countable) :
theorem
measure_theory.measure_finite
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
[measure_theory.has_no_atoms μ]
(h : s.finite) :
theorem
measure_theory.measure_finset
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
(s : finset α) :
theorem
measure_theory.insert_ae_eq_self
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
(a : α)
(s : set α) :
theorem
measure_theory.Iio_ae_eq_Iic
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a : α} :
theorem
measure_theory.Ioi_ae_eq_Ici
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a : α} :
theorem
measure_theory.Ioo_ae_eq_Ioc
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a b : α} :
theorem
measure_theory.Ioc_ae_eq_Icc
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a b : α} :
theorem
measure_theory.Ioo_ae_eq_Ico
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a b : α} :
theorem
measure_theory.Ioo_ae_eq_Icc
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a b : α} :
theorem
measure_theory.Ico_ae_eq_Icc
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a b : α} :
theorem
measure_theory.Ico_ae_eq_Ioc
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
[measure_theory.has_no_atoms μ]
[partial_order α]
{a b : α} :
theorem
measure_theory.ite_ae_eq_of_measure_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{γ : Type u_2}
(f g : α → γ)
(s : set α)
(hs_zero : ⇑μ s = 0) :
theorem
measure_theory.ite_ae_eq_of_measure_compl_zero
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{γ : Type u_2}
(f g : α → γ)
(s : set α)
(hs_zero : ⇑μ sᶜ = 0) :
def
measure_theory.measure.finite_at_filter
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(f : filter α) :
Prop
A measure is called finite at filter f if it is finite at some set s ∈ f.
Equivalently, it is eventually finite at s in f.lift' powerset.
theorem
measure_theory.measure.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_filter.exists_mem_basis
{α : Type u_1}
{ι : Type u_5}
[measurable_space α]
{μ : measure_theory.measure α}
{f : filter α}
(hμ : μ.finite_at_filter f)
{p : ι → Prop}
{s : ι → set α}
(hf : f.has_basis p s) :
theorem
measure_theory.measure.finite_at_bot
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
@[nolint]
structure
measure_theory.measure.finite_spanning_sets_in
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(C : set (set α)) :
Type u_1
- set : ℕ → set α
- set_mem : ∀ (i : ℕ), c.set i ∈ C
- finite : ∀ (i : ℕ), ⇑μ (c.set i) < ⊤
- spanning : (⋃ (i : ℕ), c.set i) = set.univ
μ has finite spanning sets in C if there is a countable sequence of sets in C that have
finite measures. This structure is a type, which is useful if we want to record extra properties
about the sets, such as that they are monotone.
sigma_finite is defined in terms of this: μ is σ-finite if there exists a sequence of
finite spanning sets in the collection of all measurable sets.
@[class]
structure
measure_theory.sigma_finite
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
Prop
- out' : nonempty (μ.finite_spanning_sets_in {s : set α | measurable_set s})
A measure μ is called σ-finite if there is a countable collection of sets
{ A i | i ∈ ℕ } such that μ (A i) < ∞ and ⋃ i, A i = s.
Instances
- measure_theory.finite_measure.to_sigma_finite
- measure_theory.sigma_finite_of_locally_finite
- measure_theory.restrict.sigma_finite
- measure_theory.sum.sigma_finite
- measure_theory.add.sigma_finite
- measure_theory.measure.prod.sigma_finite
- measure_theory.measure.sigma_finite_tprod
- measure_theory.measure.pi.sigma_finite
- measure_theory.measure.haar_measure.measure_theory.sigma_finite
theorem
measure_theory.sigma_finite_iff
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α} :
measure_theory.sigma_finite μ ↔ nonempty (μ.finite_spanning_sets_in {s : set α | measurable_set s})
theorem
measure_theory.sigma_finite.out
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
(h : measure_theory.sigma_finite μ) :
nonempty (μ.finite_spanning_sets_in {s : set α | measurable_set s})
def
measure_theory.measure.to_finite_spanning_sets_in
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[h : measure_theory.sigma_finite μ] :
μ.finite_spanning_sets_in {s : set α | measurable_set s}
If μ is σ-finite it has finite spanning sets in the collection of all measurable sets.
Equations
def
measure_theory.spanning_sets
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ]
(i : ℕ) :
set α
A noncomputable way to get a monotone collection of sets that span univ and have finite
measure using classical.some. This definition satisfies monotonicity in addition to all other
properties in sigma_finite.
Equations
theorem
measure_theory.monotone_spanning_sets
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ] :
theorem
measure_theory.measurable_spanning_sets
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ]
(i : ℕ) :
theorem
measure_theory.measure_spanning_sets_lt_top
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ]
(i : ℕ) :
⇑μ (measure_theory.spanning_sets μ i) < ⊤
theorem
measure_theory.Union_spanning_sets
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ] :
(⋃ (i : ℕ), measure_theory.spanning_sets μ i) = set.univ
theorem
measure_theory.is_countably_spanning_spanning_sets
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ] :
theorem
measure_theory.measure.supr_restrict_spanning_sets
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
[measure_theory.sigma_finite μ]
(hs : measurable_set s) :
@[protected]
def
measure_theory.measure.finite_spanning_sets_in.mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{C D : set (set α)}
(h : μ.finite_spanning_sets_in C)
(hC : C ⊆ D) :
If μ has finite spanning sets in C and C ⊆ D then μ has finite spanning sets in D.
@[protected]
theorem
measure_theory.measure.finite_spanning_sets_in.sigma_finite
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{C : set (set α)}
(h : μ.finite_spanning_sets_in C)
(hC : ∀ (s : set α), s ∈ C → measurable_set s) :
If μ has finite spanning sets in the collection of measurable sets C, then μ is σ-finite.
@[protected]
theorem
measure_theory.measure.finite_spanning_sets_in.ext
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{C : set (set α)}
(hA : _inst_1 = measurable_space.generate_from C)
(hC : is_pi_system C)
(h : μ.finite_spanning_sets_in C)
(h_eq : ∀ (s : set α), s ∈ C → ⇑μ s = ⇑ν s) :
μ = ν
An extensionality for measures. It is ext_of_generate_from_of_Union formulated in terms of
finite_spanning_sets_in.
@[protected]
theorem
measure_theory.measure.finite_spanning_sets_in.is_countably_spanning
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{C : set (set α)}
(h : μ.finite_spanning_sets_in C) :
theorem
measure_theory.measure.sigma_finite_of_not_nonempty
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(hα : ¬nonempty α) :
theorem
measure_theory.measure.sigma_finite_of_countable
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{S : set (set α)}
(hc : S.countable)
(hμ : ∀ (s : set α), s ∈ S → ⇑μ s < ⊤)
(hU : ⋃₀S = set.univ) :
@[protected, instance]
def
measure_theory.finite_measure.to_sigma_finite
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ] :
Every finite measure is σ-finite.
@[protected, instance]
def
measure_theory.restrict.sigma_finite
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.sigma_finite μ]
(s : set α) :
@[protected, instance]
def
measure_theory.sum.sigma_finite
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
[fintype ι]
(μ : ι → measure_theory.measure α)
[∀ (i : ι), measure_theory.sigma_finite (μ i)] :
@[protected, instance]
def
measure_theory.add.sigma_finite
{α : Type u_1}
[measurable_space α]
(μ ν : measure_theory.measure α)
[measure_theory.sigma_finite μ]
[measure_theory.sigma_finite ν] :
measure_theory.sigma_finite (μ + ν)
theorem
measure_theory.sigma_finite.of_map
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
[measurable_space β]
(μ : measure_theory.measure α)
{f : α → β}
(hf : measurable f)
(h : measure_theory.sigma_finite (⇑(measure_theory.measure.map f) μ)) :
@[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 (𝓝 x)
A measure is called locally finite if it is finite in some neighborhood of each point.
@[protected, instance]
def
measure_theory.finite_measure.to_locally_finite_measure
{α : Type u_1}
[measurable_space α]
[topological_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ] :
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 (𝓝 x)
theorem
measure_theory.measure.smul_finite
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
[measure_theory.finite_measure μ]
{c : ℝ≥0∞}
(hc : c < ⊤) :
theorem
measure_theory.measure.exists_is_open_measure_lt_top
{α : Type u_1}
[measurable_space α]
[topological_space α]
(μ : measure_theory.measure α)
[measure_theory.locally_finite_measure μ]
(x : α) :
@[protected, instance]
def
measure_theory.sigma_finite_of_locally_finite
{α : Type u_1}
[measurable_space α]
[topological_space α]
[topological_space.second_countable_topology α]
{μ : measure_theory.measure α}
[measure_theory.locally_finite_measure μ] :
theorem
measure_theory.ext_on_measurable_space_of_generate_finite
{α : Type u_1}
(m₀ : measurable_space α)
{μ ν : measure_theory.measure α}
[measure_theory.finite_measure μ]
(C : set (set α))
(hμν : ∀ (s : set α), s ∈ C → ⇑μ s = ⇑ν s)
{m : measurable_space α}
(h : m ≤ m₀)
(hA : m = measurable_space.generate_from C)
(hC : is_pi_system C)
(h_univ : ⇑μ set.univ = ⇑ν set.univ)
{s : set α}
(hs : m.measurable_set' s) :
If two finite measures give the same mass to the whole space and coincide on a π-system made of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.
theorem
measure_theory.ext_of_generate_finite
{α : Type u_1}
[measurable_space α]
(C : set (set α))
(hA : _inst_1 = measurable_space.generate_from C)
(hC : is_pi_system C)
{μ ν : measure_theory.measure α}
[measure_theory.finite_measure μ]
(hμν : ∀ (s : set α), s ∈ C → ⇑μ s = ⇑ν s)
(h_univ : ⇑μ set.univ = ⇑ν set.univ) :
μ = ν
Two finite measures are equal if they are equal on the π-system generating the σ-algebra
(and univ).
theorem
measure_theory.measure.finite_at_filter.filter_mono
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α}
(h : 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 α}
(h : μ.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 α}
(h : μ.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.of_inf_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : filter α} :
μ.finite_at_filter (f ⊓ μ.ae) → μ.finite_at_filter f
Alias of inf_ae_iff.
theorem
measure_theory.measure.finite_at_filter.filter_mono_ae
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f g : filter α}
(h : f ⊓ μ.ae ≤ g)
(hg : μ.finite_at_filter g) :
μ.finite_at_filter f
@[protected]
theorem
measure_theory.measure.finite_at_filter.measure_mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{f : filter α}
(h : μ ≤ ν) :
ν.finite_at_filter f → μ.finite_at_filter f
@[protected]
theorem
measure_theory.measure.finite_at_filter.mono
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{f g : filter α}
(hf : f ≤ g)
(hμ : μ ≤ ν) :
ν.finite_at_filter g → μ.finite_at_filter f
@[protected]
theorem
measure_theory.measure.finite_at_filter.eventually
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{f : filter α}
(h : μ.finite_at_filter f) :
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 (𝓝[s] x)
@[simp]
theorem
measure_theory.measure.finite_at_principal
{α : Type u_1}
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α} :
Subtraction of measures #
@[protected, instance]
The measure μ - ν is defined to be the least measure τ such that μ ≤ τ + ν.
It is the equivalent of (μ - ν) ⊔ 0 if μ and ν were signed measures.
Compare with ennreal.has_sub.
Specifically, note that if you have α = {1,2}, and μ {1} = 2, μ {2} = 0, and
ν {2} = 2, ν {1} = 0, then (μ - ν) {1, 2} = 2. However, if μ ≤ ν, and
ν univ ≠ ∞, then (μ - ν) + ν = μ.
Equations
- measure_theory.measure.has_sub = {sub := λ (μ ν : measure_theory.measure α), Inf {τ : measure_theory.measure α | μ ≤ τ + ν}}
theorem
measure_theory.measure.sub_def
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α} :
theorem
measure_theory.measure.sub_eq_zero_of_le
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
(h : μ ≤ ν) :
theorem
measure_theory.measure.sub_apply
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s : set α}
[measure_theory.finite_measure ν]
(h₁ : measurable_set s)
(h₂ : ν ≤ μ) :
This application lemma only works in special circumstances. Given knowledge of
when μ ≤ ν and ν ≤ μ, a more general application lemma can be written.
theorem
measure_theory.measure.sub_add_cancel_of_le
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
[measure_theory.finite_measure ν]
(h₁ : ν ≤ μ) :
theorem
measure_theory.measure.restrict_sub_eq_restrict_sub_restrict
{α : Type u_1}
[measurable_space α]
{μ ν : measure_theory.measure α}
{s : set α}
(h_meas_s : measurable_set s) :