Measure spaces #
The definition of a measure and a measure space are in measure_theory.measure_space_def, with
only a few basic properties. This file provides many more properties of these objects.
This separation allows the measurability tactic to import only the file measure_space_def, and to
be available in measure_space (through measurable_space).
Given a measurable space α, a measure on α is a function that sends measurable sets to the
extended nonnegative reals that satisfies the following conditions:
μ ∅ = 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:
is_probability_measure μ:μ univ = 1;is_finite_measure μ:μ univ < ∞;sigma_finite μ: there exists a countable collection of sets that coverunivwhereμis finite;is_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
@[protected, instance]
def
measure_theory.ae_is_measurably_generated
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.ae_uIoc_iff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
[linear_order α]
{a b : α}
{P : α → Prop} :
See also measure_theory.ae_restrict_uIoc_iff.
theorem
measure_theory.measure_union
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(hd : disjoint s₁ s₂)
(h : measurable_set s₂) :
theorem
measure_theory.measure_union'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(hd : disjoint s₁ s₂)
(h : measurable_set s₁) :
theorem
measure_theory.measure_inter_add_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measurable_set t) :
theorem
measure_theory.measure_diff_add_inter
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measurable_set t) :
theorem
measure_theory.measure_union_add_inter
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measurable_set t) :
theorem
measure_theory.measure_union_add_inter'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(t : set α) :
theorem
measure_theory.measure_add_measure_compl
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : measurable_set s) :
theorem
measure_theory.measure_bUnion₀
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set β}
{f : β → set α}
(hs : s.countable)
(hd : s.pairwise (measure_theory.ae_disjoint μ on f))
(h : ∀ (b : β), b ∈ s → measure_theory.null_measurable_set (f b) μ) :
theorem
measure_theory.measure_bUnion
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set β}
{f : β → set α}
(hs : s.countable)
(hd : s.pairwise_disjoint f)
(h : ∀ (b : β), b ∈ s → measurable_set (f b)) :
theorem
measure_theory.measure_sUnion₀
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{S : set (set α)}
(hs : S.countable)
(hd : S.pairwise (measure_theory.ae_disjoint μ))
(h : ∀ (s : set α), s ∈ S → measure_theory.null_measurable_set s μ) :
theorem
measure_theory.measure_bUnion_finset₀
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : finset ι}
{f : ι → set α}
(hd : ↑s.pairwise (measure_theory.ae_disjoint μ on f))
(hm : ∀ (b : ι), b ∈ s → measure_theory.null_measurable_set (f b) μ) :
theorem
measure_theory.measure_bUnion_finset
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : finset ι}
{f : ι → set α}
(hd : ↑s.pairwise_disjoint f)
(hm : ∀ (b : ι), b ∈ s → measurable_set (f b)) :
theorem
measure_theory.tsum_meas_le_meas_Union_of_disjoint
{α : Type u_1}
{ι : Type u_2}
[measurable_space α]
(μ : measure_theory.measure α)
{As : ι → set α}
(As_mble : ∀ (i : ι), measurable_set (As i))
(As_disj : pairwise (disjoint on As)) :
The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of the measures of the sets.
theorem
measure_theory.tsum_measure_preimage_singleton
{α : Type u_1}
{β : Type u_2}
{m : 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}
{m : 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}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : ⇑μ (s₁ ∩ s₂) = 0) :
theorem
measure_theory.measure_diff_null
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : ⇑μ s₂ = 0) :
theorem
measure_theory.measure_add_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(t : set α) :
theorem
measure_theory.measure_diff'
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(hm : measurable_set t)
(h_fin : ⇑μ t ≠ ⊤) :
theorem
measure_theory.measure_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ : set α}
(h : s₂ ⊆ s₁)
(h₂ : measurable_set s₂)
(h_fin : ⇑μ s₂ ≠ ⊤) :
theorem
measure_theory.le_measure_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ : set α} :
theorem
measure_theory.measure_diff_lt_of_lt_add
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(hst : s ⊆ t)
(hs' : ⇑μ s ≠ ⊤)
{ε : ennreal}
(h : ⇑μ t < ⇑μ s + ε) :
theorem
measure_theory.measure_diff_le_iff_le_add
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(hst : s ⊆ t)
(hs' : ⇑μ s ≠ ⊤)
{ε : ennreal} :
theorem
measure_theory.measure_eq_measure_of_null_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hst : s ⊆ t)
(h_nulldiff : ⇑μ (t \ s) = 0) :
theorem
measure_theory.measure_eq_measure_smaller_of_between_null_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ s₃ : set α}
(h12 : s₁ ⊆ s₂)
(h23 : s₂ ⊆ s₃)
(h_nulldiff : ⇑μ (s₃ \ s₁) = 0) :
theorem
measure_theory.measure_eq_measure_larger_of_between_null_diff
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s₁ s₂ s₃ : set α}
(h12 : s₁ ⊆ s₂)
(h23 : s₂ ⊆ s₃)
(h_nulldiff : ⇑μ (s₃ \ s₁) = 0) :
theorem
measure_theory.measure_compl
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h₁ : measurable_set s)
(h_fin : ⇑μ s ≠ ⊤) :
@[simp]
theorem
measure_theory.union_ae_eq_left_iff_ae_subset
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α} :
@[simp]
theorem
measure_theory.union_ae_eq_right_iff_ae_subset
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.ae_eq_of_ae_subset_of_measure_ge
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h₁ : s ≤ᵐ[μ] t)
(h₂ : ⇑μ t ≤ ⇑μ s)
(hsm : measurable_set s)
(ht : ⇑μ t ≠ ⊤) :
theorem
measure_theory.ae_eq_of_subset_of_measure_ge
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h₁ : s ⊆ t)
(h₂ : ⇑μ t ≤ ⇑μ s)
(hsm : measurable_set s)
(ht : ⇑μ t ≠ ⊤) :
If s ⊆ t, μ t ≤ μ s, μ t ≠ ∞, and s is measurable, then s =ᵐ[μ] t.
@[simp]
theorem
measure_theory.measure_Union_to_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[countable β]
(s : β → set α) :
theorem
measure_theory.measure_bUnion_to_measurable
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{I : set β}
(hc : I.countable)
(s : β → set α) :
@[simp]
theorem
measure_theory.measure_to_measurable_union
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α} :
@[simp]
theorem
measure_theory.measure_union_to_measurable
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α} :
theorem
measure_theory.sum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : finset ι}
{t : ι → set α}
(h : ∀ (i : ι), i ∈ s → measurable_set (t i))
(H : ↑s.pairwise_disjoint t) :
theorem
measure_theory.tsum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_5}
{m : 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}
{m : 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}
{m : measurable_space α}
(μ : measure_theory.measure α)
{s : finset ι}
{t : ι → set α}
(h : ∀ (i : ι), i ∈ s → measurable_set (t i))
(H : ⇑μ set.univ < s.sum (λ (i : ι), ⇑μ (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.nonempty_inter_of_measure_lt_add
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
{s t u : set α}
(ht : measurable_set t)
(h's : s ⊆ u)
(h't : t ⊆ u)
(h : ⇑μ u < ⇑μ s + ⇑μ t) :
If two sets s and t are included in a set u, and μ s + μ t > μ u,
then s intersects t. Version assuming that t is measurable.
theorem
measure_theory.nonempty_inter_of_measure_lt_add'
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
{s t u : set α}
(hs : measurable_set s)
(h's : s ⊆ u)
(h't : t ⊆ u)
(h : ⇑μ u < ⇑μ s + ⇑μ t) :
If two sets s and t are included in a set u, and μ s + μ t > μ u,
then s intersects t. Version assuming that s is measurable.
theorem
measure_theory.measure_Union_eq_supr
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(hd : directed has_subset.subset s) :
Continuity from below: the measure of the union of a directed sequence of (not necessarily -measurable) sets is the supremum of the measures.
theorem
measure_theory.measure_bUnion_eq_supr
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : ι → set α}
{t : set ι}
(ht : t.countable)
(hd : directed_on (has_subset.subset on s) t) :
theorem
measure_theory.measure_Inter_eq_infi
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{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.tendsto_measure_Union
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
[semilattice_sup ι]
[countable ι]
{s : ι → set α}
(hm : monotone s) :
filter.tendsto (⇑μ ∘ s) filter.at_top (nhds (⇑μ (⋃ (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}
{ι : Type u_5}
{m : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
[semilattice_sup ι]
{s : ι → set α}
(hs : ∀ (n : ι), measurable_set (s n))
(hm : antitone s)
(hf : ∃ (i : ι), ⇑μ (s i) ≠ ⊤) :
filter.tendsto (⇑μ ∘ s) filter.at_top (nhds (⇑μ (⋂ (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.tendsto_measure_bInter_gt
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{ι : Type u_2}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[densely_ordered ι]
[topological_space.first_countable_topology ι]
{s : ι → set α}
{a : ι}
(hs : ∀ (r : ι), r > a → measurable_set (s r))
(hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j)
(hf : ∃ (r : ι) (H : r > a), ⇑μ (s r) ≠ ⊤) :
filter.tendsto (⇑μ ∘ s) (nhds_within a (set.Ioi a)) (nhds (⇑μ (⋂ (r : ι) (H : r > a), s r)))
The measure of the intersection of a decreasing sequence of measurable sets indexed by a linear order with first countable topology is the limit of the measures.
theorem
measure_theory.measure_limsup_eq_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : ℕ → set α}
(hs : ∑' (i : ℕ), ⇑μ (s i) ≠ ⊤) :
⇑μ (filter.limsup s filter.at_top) = 0
One direction of the Borel-Cantelli lemma: if (sᵢ) is a sequence of sets such
that ∑ μ sᵢ is finite, then the limit superior of the sᵢ is a null set.
theorem
measure_theory.measure_liminf_eq_zero
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{s : ℕ → set α}
(h : ∑' (i : ℕ), ⇑μ (s i) ≠ ⊤) :
⇑μ (filter.liminf s filter.at_top) = 0
theorem
measure_theory.limsup_ae_eq_of_forall_ae_eq
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(s : ℕ → set α)
{t : set α}
(h : ∀ (n : ℕ), s n =ᵐ[μ] t) :
theorem
measure_theory.liminf_ae_eq_of_forall_ae_eq
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
(s : ℕ → set α)
{t : set α}
(h : ∀ (n : ℕ), s n =ᵐ[μ] t) :
theorem
measure_theory.measure_if
{α : Type u_1}
{β : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
{x : β}
{t : set β}
{s : set α} :
noncomputable
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
theorem
measure_theory.to_measure_apply₀
{α : Type u_1}
[ms : measurable_space α]
(m : measure_theory.outer_measure α)
(h : ms ≤ m.caratheodory)
{s : set α}
(hs : measure_theory.null_measurable_set s (m.to_measure h)) :
⇑(m.to_measure h) s = ⇑m s
@[simp]
theorem
measure_theory.to_outer_measure_to_measure
{α : Type u_1}
[ms : measurable_space α]
{μ : measure_theory.measure α} :
μ.to_outer_measure.to_measure _ = μ
@[simp]
theorem
measure_theory.bounded_by_measure
{α : Type u_1}
[ms : measurable_space α]
(μ : measure_theory.measure α) :
theorem
measure_theory.measure.measure_inter_eq_of_measure_eq
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t u : set α}
(hs : measurable_set s)
(h : ⇑μ t = ⇑μ u)
(htu : t ⊆ u)
(ht_ne_top : ⇑μ t ≠ ⊤) :
If u is a superset of t with the same (finite) measure (both sets possibly non-measurable),
then for any measurable set s one also has μ (t ∩ s) = μ (u ∩ s).
theorem
measure_theory.measure.measure_to_measurable_inter
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(ht : ⇑μ t ≠ ⊤) :
The measurable superset to_measurable μ t of t (which has the same measure as t)
satisfies, for any measurable set s, the equality μ (to_measurable μ t ∩ s) = μ (u ∩ s).
Here, we require that the measure of t is finite. The conclusion holds without this assumption
when the measure is sigma_finite, see measure_to_measurable_inter_of_sigma_finite.
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}
{m : measurable_space α} :
0.to_outer_measure = 0
@[simp, norm_cast]
@[protected, instance]
theorem
measure_theory.measure.eq_zero_of_is_empty
{α : Type u_1}
[is_empty α]
{m : measurable_space α}
(μ : 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}
{m : 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}
{m : measurable_space α}
(μ₁ μ₂ : measure_theory.measure α) :
theorem
measure_theory.measure.add_apply
{α : Type u_1}
{m : measurable_space α}
(μ₁ μ₂ : measure_theory.measure α)
(s : set α) :
@[protected, instance]
def
measure_theory.measure.has_smul
{α : Type u_1}
{R : Type u_6}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
[measurable_space α] :
Equations
- measure_theory.measure.has_smul = {smul := λ (c : R) (μ : 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}
{R : Type u_6}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
{m : measurable_space α}
(c : R)
(μ : measure_theory.measure α) :
(c • μ).to_outer_measure = c • μ.to_outer_measure
@[simp, norm_cast]
theorem
measure_theory.measure.coe_smul
{α : Type u_1}
{R : Type u_6}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
{m : measurable_space α}
(c : R)
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.smul_apply
{α : Type u_1}
{R : Type u_6}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
{m : measurable_space α}
(c : R)
(μ : measure_theory.measure α)
(s : set α) :
@[protected, instance]
def
measure_theory.measure.smul_comm_class
{α : Type u_1}
{R : Type u_6}
{R' : Type u_7}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
[has_smul R' ennreal]
[is_scalar_tower R' ennreal ennreal]
[smul_comm_class R R' ennreal]
[measurable_space α] :
smul_comm_class R R' (measure_theory.measure α)
@[protected, instance]
def
measure_theory.measure.is_scalar_tower
{α : Type u_1}
{R : Type u_6}
{R' : Type u_7}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
[has_smul R' ennreal]
[is_scalar_tower R' ennreal ennreal]
[has_smul R R']
[is_scalar_tower R R' ennreal]
[measurable_space α] :
is_scalar_tower R R' (measure_theory.measure α)
@[protected, instance]
def
measure_theory.measure.is_central_scalar
{α : Type u_1}
{R : Type u_6}
[has_smul R ennreal]
[is_scalar_tower R ennreal ennreal]
[has_smul Rᵐᵒᵖ ennreal]
[is_central_scalar R ennreal]
[measurable_space α] :
@[protected, instance]
def
measure_theory.measure.mul_action
{α : Type u_1}
{R : Type u_6}
[monoid R]
[mul_action R ennreal]
[is_scalar_tower R ennreal ennreal]
[measurable_space α] :
Equations
- measure_theory.measure.mul_action = function.injective.mul_action measure_theory.measure.to_outer_measure measure_theory.measure.to_outer_measure_injective measure_theory.measure.mul_action._proof_1
@[protected, instance]
Equations
- measure_theory.measure.add_comm_monoid = function.injective.add_comm_monoid measure_theory.measure.to_outer_measure measure_theory.measure.to_outer_measure_injective measure_theory.measure.zero_to_outer_measure measure_theory.measure.add_to_outer_measure measure_theory.measure.add_comm_monoid._proof_2
Coercion to function as an additive monoid homomorphism.
Equations
@[simp]
theorem
measure_theory.measure.coe_finset_sum
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
(I : finset ι)
(μ : ι → measure_theory.measure α) :
theorem
measure_theory.measure.finset_sum_apply
{α : Type u_1}
{ι : Type u_5}
{m : measurable_space α}
(I : finset ι)
(μ : ι → measure_theory.measure α)
(s : set α) :
@[protected, instance]
noncomputable
def
measure_theory.measure.distrib_mul_action
{α : Type u_1}
{R : Type u_6}
[monoid R]
[distrib_mul_action R ennreal]
[is_scalar_tower R ennreal ennreal]
[measurable_space α] :
Equations
- measure_theory.measure.distrib_mul_action = function.injective.distrib_mul_action {to_fun := measure_theory.measure.to_outer_measure _inst_6, map_zero' := _, map_add' := _} measure_theory.measure.to_outer_measure_injective measure_theory.measure.distrib_mul_action._proof_1
@[protected, instance]
noncomputable
def
measure_theory.measure.module
{α : Type u_1}
{R : Type u_6}
[semiring R]
[module R ennreal]
[is_scalar_tower R ennreal ennreal]
[measurable_space α] :
module R (measure_theory.measure α)
Equations
- measure_theory.measure.module = function.injective.module R {to_fun := measure_theory.measure.to_outer_measure _inst_6, map_zero' := _, map_add' := _} measure_theory.measure.to_outer_measure_injective measure_theory.measure.module._proof_1
@[simp]
theorem
measure_theory.measure.coe_nnreal_smul_apply
{α : Type u_1}
{m : measurable_space α}
(c : nnreal)
(μ : measure_theory.measure α)
(s : set α) :
theorem
measure_theory.measure.measure_to_measurable_add_inter_left
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(ht : ⇑(μ + ν) t ≠ ⊤) :
theorem
measure_theory.measure.measure_to_measurable_add_inter_right
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s)
(ht : ⇑(μ + ν) t ≠ ⊤) :
The complete lattice of measures #
@[protected, instance]
Measures are partially ordered.
The definition of less equal here is equivalent to the definition without the
measurable set condition, and this is shown by measure.le_iff'. It is defined
this way since, to prove μ ≤ ν, we may simply intros s hs instead of rewriting followed
by intros s hs.
Equations
- 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}
{m0 : measurable_space α}
{μ₁ μ₂ : measure_theory.measure α} :
theorem
measure_theory.measure.to_outer_measure_le
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ : measure_theory.measure α} :
μ₁.to_outer_measure ≤ μ₂.to_outer_measure ↔ μ₁ ≤ μ₂
theorem
measure_theory.measure.le_iff'
{α : Type u_1}
{m0 : measurable_space α}
{μ₁ μ₂ : measure_theory.measure α} :
theorem
measure_theory.measure.lt_iff
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α} :
theorem
measure_theory.measure.lt_iff'
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α} :
@[protected, instance]
@[protected]
theorem
measure_theory.measure.le_add_left
{α : Type u_1}
{m0 : measurable_space α}
{μ ν ν' : measure_theory.measure α}
(h : μ ≤ ν) :
@[protected]
theorem
measure_theory.measure.le_add_right
{α : Type u_1}
{m0 : measurable_space α}
{μ ν ν' : measure_theory.measure α}
(h : μ ≤ ν) :
theorem
measure_theory.measure.Inf_caratheodory
{α : Type u_1}
{m0 : 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}
{m0 : measurable_space α}
{s : set α}
{m : set (measure_theory.measure α)}
(hs : measurable_set s) :
⇑(has_Inf.Inf m) s = ⇑(has_Inf.Inf (measure_theory.measure.to_outer_measure '' m)) s
@[protected, instance]
noncomputable
def
measure_theory.measure.complete_semilattice_Inf
{α : Type u_1}
[measurable_space α] :
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 := has_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 := _, 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 := _, top := complete_lattice.top (complete_lattice_of_complete_semilattice_Inf (measure_theory.measure α)), bot := 0, le_top := _, bot_le := _}
@[simp]
theorem
measure_theory.measure.top_add
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.add_top
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[protected]
theorem
measure_theory.measure.zero_le
{α : Type u_1}
{m0 : measurable_space α}
(μ : measure_theory.measure α) :
0 ≤ μ
theorem
measure_theory.measure.nonpos_iff_eq_zero'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.measure_univ_eq_zero
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
Pushforward and pullback #
noncomputable
def
measure_theory.measure.lift_linear
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
{m0 : measurable_space α}
(f : measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β)
(hf : ∀ (μ : measure_theory.measure α), _inst_1 ≤ (⇑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}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β}
(hf : ∀ (μ : measure_theory.measure α), _inst_1 ≤ (⇑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}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β}
(hf : ∀ (μ : measure_theory.measure α), _inst_1 ≤ (⇑f μ.to_outer_measure).caratheodory)
(s : set β) :
⇑(⇑f μ.to_outer_measure) s ≤ ⇑(⇑(measure_theory.measure.lift_linear f hf) μ) s
noncomputable
def
measure_theory.measure.mapₗ
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
[measurable_space α]
(f : α → β) :
The pushforward of a measure as a linear map. 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)
theorem
measure_theory.measure.mapₗ_congr
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f g : α → β}
(hf : measurable f)
(hg : measurable g)
(h : f =ᵐ[μ] g) :
@[irreducible]
noncomputable
def
measure_theory.measure.map
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
[measurable_space α]
(f : α → β)
(μ : measure_theory.measure α) :
The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere
measurable function.
Equations
- measure_theory.measure.map f μ = dite (ae_measurable f μ) (λ (hf : ae_measurable f μ), ⇑(measure_theory.measure.mapₗ (ae_measurable.mk f hf)) μ) (λ (hf : ¬ae_measurable f μ), 0)
theorem
measure_theory.measure.mapₗ_mk_apply_of_ae_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ) :
⇑(measure_theory.measure.mapₗ (ae_measurable.mk f hf)) μ = measure_theory.measure.map f μ
theorem
measure_theory.measure.mapₗ_apply_of_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
(hf : measurable f)
(μ : measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.map_add
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
(μ ν : measure_theory.measure α)
{f : α → β}
(hf : measurable f) :
measure_theory.measure.map f (μ + ν) = measure_theory.measure.map f μ + measure_theory.measure.map f ν
@[simp]
theorem
measure_theory.measure.map_zero
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
(f : α → β) :
measure_theory.measure.map f 0 = 0
theorem
measure_theory.measure.map_of_not_ae_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{f : α → β}
{μ : measure_theory.measure α}
(hf : ¬ae_measurable f μ) :
measure_theory.measure.map f μ = 0
theorem
measure_theory.measure.map_congr
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f g : α → β}
(h : f =ᵐ[μ] g) :
@[protected, simp]
theorem
measure_theory.measure.map_smul
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
(c : ennreal)
(μ : measure_theory.measure α)
(f : α → β) :
measure_theory.measure.map f (c • μ) = c • measure_theory.measure.map f μ
@[protected, simp]
theorem
measure_theory.measure.map_smul_nnreal
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
(c : nnreal)
(μ : measure_theory.measure α)
(f : α → β) :
measure_theory.measure.map f (c • μ) = c • measure_theory.measure.map f μ
@[simp]
theorem
measure_theory.measure.map_apply_of_ae_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ)
{s : set β}
(hs : measurable_set s) :
⇑(measure_theory.measure.map f μ) s = ⇑μ (f ⁻¹' s)
We can evaluate the pushforward on measurable sets. For non-measurable sets, see
measure_theory.measure.le_map_apply and measurable_equiv.map_apply.
@[simp]
theorem
measure_theory.measure.map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : measurable f)
{s : set β}
(hs : measurable_set s) :
⇑(measure_theory.measure.map f μ) s = ⇑μ (f ⁻¹' s)
theorem
measure_theory.measure.map_to_outer_measure
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ) :
@[simp]
theorem
measure_theory.measure.map_id
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.map_id'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
measure_theory.measure.map (λ (x : α), x) μ = μ
theorem
measure_theory.measure.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m0 : 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}
{m0 : measurable_space α}
[measurable_space β]
{μ ν : measure_theory.measure α}
{f : α → β}
(h : μ ≤ ν)
(hf : measurable f) :
theorem
measure_theory.measure.le_map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ)
(s : set β) :
⇑μ (f ⁻¹' s) ≤ ⇑(measure_theory.measure.map f μ) s
Even if s is not measurable, we can bound map f μ s from below.
See also measurable_equiv.map_apply.
theorem
measure_theory.measure.preimage_null_of_map_null
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_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}
{m0 : measurable_space α}
[measurable_space β]
{μ : measure_theory.measure α}
{f : α → β}
(hf : ae_measurable f μ) :
filter.tendsto f μ.ae (measure_theory.measure.map f μ).ae
noncomputable
def
measure_theory.measure.comapₗ
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
[measurable_space α]
(f : α → β) :
Pullback of a measure as a linear map. If f sends each measurable set to a measurable
set, then for each measurable set s we have comapₗ f μ s = μ (f '' s).
If the linearity is not needed, please use comap instead, which works for a larger class of
functions.
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}
{s : set α}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measurable_set (f '' s))
(μ : measure_theory.measure β)
(hs : measurable_set s) :
noncomputable
def
measure_theory.measure.comap
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
[measurable_space α]
(f : α → β)
(μ : measure_theory.measure β) :
Pullback of a measure. If f sends each measurable set to a null-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 → measure_theory.null_measurable_set (f '' s) μ) (λ (hf : function.injective f ∧ ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ), (⇑(measure_theory.outer_measure.comap f) μ.to_outer_measure).to_measure _) (λ (hf : ¬(function.injective f ∧ ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ)), 0)
theorem
measure_theory.measure.comap_apply₀
{α : Type u_1}
{β : Type u_2}
[measurable_space β]
{s : set α}
[measurable_space α]
(f : α → β)
(μ : measure_theory.measure β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ)
(hs : measure_theory.null_measurable_set s (measure_theory.measure.comap f μ)) :
⇑(measure_theory.measure.comap f μ) s = ⇑μ (f '' s)
theorem
measure_theory.measure.le_comap_apply
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(μ : measure_theory.measure β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ)
(s : set α) :
⇑μ (f '' s) ≤ ⇑(measure_theory.measure.comap f μ) s
theorem
measure_theory.measure.comap_apply
{α : Type u_1}
{s : set α}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measurable_set (f '' s))
(μ : measure_theory.measure β)
(hs : measurable_set s) :
⇑(measure_theory.measure.comap f μ) s = ⇑μ (f '' s)
theorem
measure_theory.measure.comapₗ_eq_comap
{α : Type u_1}
{s : set α}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measurable_set (f '' s))
(μ : measure_theory.measure β)
(hs : measurable_set s) :
⇑(⇑(measure_theory.measure.comapₗ f) μ) s = ⇑(measure_theory.measure.comap f μ) s
theorem
measure_theory.measure.measure_image_eq_zero_of_comap_eq_zero
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(μ : measure_theory.measure β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ)
{s : set α}
(hs : ⇑(measure_theory.measure.comap f μ) s = 0) :
theorem
measure_theory.measure.ae_eq_image_of_ae_eq_comap
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(μ : measure_theory.measure β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ)
{s t : set α}
(hst : s =ᵐ[measure_theory.measure.comap f μ] t) :
theorem
measure_theory.measure.null_measurable_set.image
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(μ : measure_theory.measure β)
(hfi : function.injective f)
(hf : ∀ (s : set α), measurable_set s → measure_theory.null_measurable_set (f '' s) μ)
{s : set α}
(hs : measure_theory.null_measurable_set s (measure_theory.measure.comap f μ)) :
measure_theory.null_measurable_set (f '' s) μ
theorem
measure_theory.measure.comap_preimage
{α : Type u_1}
{β : Type u_2}
[measurable_space α]
{mβ : measurable_space β}
(f : α → β)
(μ : measure_theory.measure β)
{s : set β}
(hf : function.injective f)
(hf' : measurable f)
(h : ∀ (t : set α), measurable_set t → measure_theory.null_measurable_set (f '' t) μ)
(hs : measurable_set s) :
Subtype of a measure space #
theorem
measure_theory.measure.measurable_set.null_measurable_set_subtype_coe
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{t : set ↥s}
(hs : measure_theory.null_measurable_set s μ)
(ht : measurable_set t) :
theorem
measure_theory.measure.null_measurable_set.subtype_coe
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
{t : set ↥s}
(hs : measure_theory.null_measurable_set s μ)
(ht : measure_theory.null_measurable_set t (measure_theory.measure.comap subtype.val μ)) :
theorem
measure_theory.measure.measure_subtype_coe_le_comap
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.null_measurable_set s μ)
(t : set ↥s) :
⇑μ (coe '' t) ≤ ⇑(measure_theory.measure.comap subtype.val μ) t
theorem
measure_theory.measure.measure_subtype_coe_eq_zero_of_comap_eq_zero
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measure_theory.null_measurable_set s μ)
{t : set ↥s}
(ht : ⇑(measure_theory.measure.comap subtype.val μ) t = 0) :
@[protected, instance]
noncomputable
def
measure_theory.measure.subtype.measure_space
{α : Type u_1}
[measure_theory.measure_space α]
{p : α → Prop} :
Equations
- measure_theory.measure.subtype.measure_space = {to_measurable_space := {measurable_set' := subtype.measurable_space.measurable_set', measurable_set_empty := _, measurable_set_compl := _, measurable_set_Union := _}, volume := measure_theory.measure.comap subtype.val measure_theory.measure_space.volume}
theorem
measure_theory.measure.volume_subtype_coe_le_volume
{α : Type u_1}
{s : set α}
[measure_theory.measure_space α]
(hs : measure_theory.null_measurable_set s measure_theory.measure_space.volume)
(t : set ↥s) :
theorem
measure_theory.measure.volume_subtype_coe_eq_zero_of_volume_eq_zero
{α : Type u_1}
{s : set α}
[measure_theory.measure_space α]
(hs : measure_theory.null_measurable_set s measure_theory.measure_space.volume)
{t : set ↥s}
(ht : ⇑measure_theory.measure_space.volume t = 0) :
Restricting a measure #
noncomputable
def
measure_theory.measure.restrictₗ
{α : Type u_1}
{m0 : measurable_space α}
(s : set α) :
Restrict a measure μ to a set s as an ℝ≥0∞-linear map.
noncomputable
def
measure_theory.measure.restrict
{α : Type u_1}
{m0 : measurable_space α}
(μ : measure_theory.measure α)
(s : set α) :
Restrict a measure μ to a set s.
Equations
- μ.restrict s = ⇑(measure_theory.measure.restrictₗ s) μ
Instances for measure_theory.measure.restrict
- measure_theory.restrict.is_finite_measure
- measure_theory.is_finite_measure_restrict
- measure_theory.measure.restrict.has_no_atoms
- measure_theory.restrict.sigma_finite
- measure_theory.ae_fin_strongly_measurable.sigma_finite_restrict
- real.is_finite_measure_restrict_Icc
- real.is_finite_measure_restrict_Ico
- real.is_finite_measure_restrict_Ioc
- real.is_finite_measure_restrict_Ioo
- measure_theory.measure.restrict.measure_theory.is_finite_measure
@[simp]
theorem
measure_theory.measure.restrictₗ_apply
{α : Type u_1}
{m0 : measurable_space α}
(s : set α)
(μ : measure_theory.measure α) :
⇑(measure_theory.measure.restrictₗ s) μ = μ.restrict s
theorem
measure_theory.measure.restrict_to_outer_measure_eq_to_outer_measure_restrict
{α : Type u_1}
{m0 : 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_apply₀
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(ht : measure_theory.null_measurable_set t (μ.restrict s)) :
@[simp]
theorem
measure_theory.measure.restrict_apply
{α : Type u_1}
{m0 : 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_mono'
{α : Type u_1}
{m0 : measurable_space α}
⦃s s' : set α⦄
⦃μ ν : measure_theory.measure α⦄
(hs : s ≤ᵐ[μ] s')
(hμν : μ ≤ ν) :
Restriction of a measure to a subset is monotone both in set and in measure.
theorem
measure_theory.measure.restrict_mono
{α : Type u_1}
{m0 : 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_mono_ae
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : s ≤ᵐ[μ] t) :
theorem
measure_theory.measure.restrict_congr_set
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : s =ᵐ[μ] t) :
@[simp]
theorem
measure_theory.measure.restrict_apply'
{α : Type u_1}
{m0 : 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_apply₀'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s μ) :
theorem
measure_theory.measure.restrict_le_self
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure.restrict_eq_self
{α : Type u_1}
{m0 : measurable_space α}
(μ : measure_theory.measure α)
{s t : set α}
(h : s ⊆ t) :
@[simp]
theorem
measure_theory.measure.restrict_apply_self
{α : Type u_1}
{m0 : measurable_space α}
(μ : measure_theory.measure α)
(s : set α) :
theorem
measure_theory.measure.restrict_apply_univ
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
(s : set α) :
theorem
measure_theory.measure.le_restrict_apply
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
(s t : set α) :
theorem
measure_theory.measure.restrict_apply_superset
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : s ⊆ t) :
@[simp]
theorem
measure_theory.measure.restrict_add
{α : Type u_1}
{m0 : measurable_space α}
(μ ν : measure_theory.measure α)
(s : set α) :
@[simp]
@[simp]
theorem
measure_theory.measure.restrict_smul
{α : Type u_1}
{m0 : measurable_space α}
(c : ennreal)
(μ : measure_theory.measure α)
(s : set α) :
theorem
measure_theory.measure.restrict_restrict₀
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measure_theory.null_measurable_set s (μ.restrict t)) :
@[simp]
theorem
measure_theory.measure.restrict_restrict
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_restrict_of_subset
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : s ⊆ t) :
theorem
measure_theory.measure.restrict_restrict₀'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(ht : measure_theory.null_measurable_set t μ) :
theorem
measure_theory.measure.restrict_restrict'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_comm
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_apply_eq_zero
{α : Type u_1}
{m0 : 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}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : ⇑(μ.restrict s) t = 0) :
theorem
measure_theory.measure.restrict_apply_eq_zero'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(hs : measurable_set s) :
@[simp]
theorem
measure_theory.measure.restrict_eq_zero
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure.restrict_zero_set
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : ⇑μ s = 0) :
@[simp]
theorem
measure_theory.measure.restrict_empty
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
@[simp]
theorem
measure_theory.measure.restrict_univ
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α} :
theorem
measure_theory.measure.restrict_inter_add_diff₀
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measure_theory.null_measurable_set t μ) :
theorem
measure_theory.measure.restrict_inter_add_diff
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_union_add_inter₀
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measure_theory.null_measurable_set t μ) :
theorem
measure_theory.measure.restrict_union_add_inter
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{t : set α}
(s : set α)
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_union_add_inter'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(t : set α) :
theorem
measure_theory.measure.restrict_union₀
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : measure_theory.ae_disjoint μ s t)
(ht : measure_theory.null_measurable_set t μ) :
theorem
measure_theory.measure.restrict_union
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : disjoint s t)
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_union'
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s t : set α}
(h : disjoint s t)
(hs : measurable_set s) :
@[simp]
theorem
measure_theory.measure.restrict_add_restrict_compl
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
@[simp]
theorem
measure_theory.measure.restrict_compl_add_restrict
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_union_le
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
(s s' : set α) :
theorem
measure_theory.measure.restrict_Union_apply_ae
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(hd : pairwise (measure_theory.ae_disjoint μ on s))
(hm : ∀ (i : ι), measure_theory.null_measurable_set (s i) μ)
{t : set α}
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_Union_apply
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{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}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(hd : directed has_subset.subset s)
{t : set α}
(ht : measurable_set t) :
theorem
measure_theory.measure.restrict_map
{α : Type u_1}
{β : Type u_2}
{m0 : 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))
The restriction of the pushforward measure is the pushforward of the restriction. For a version
assuming only ae_measurable, see restrict_map_of_ae_measurable.
theorem
measure_theory.measure.restrict_to_measurable
{α : Type u_1}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
{s : set α}
(h : ⇑μ s ≠ ⊤) :
μ.restrict (measure_theory.to_measurable μ s) = μ.restrict s
theorem
measure_theory.measure.restrict_eq_self_of_ae_mem
{α : Type u_1}
{m0 : measurable_space α}
⦃s : set α⦄
⦃μ : measure_theory.measure α⦄
(hs : ∀ᵐ (x : α) ∂μ, x ∈ s) :
theorem
measure_theory.measure.restrict_congr_meas
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.restrict_congr_mono
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s t : set α}
(hs : s ⊆ t)
(h : μ.restrict t = ν.restrict t) :
theorem
measure_theory.measure.restrict_union_congr
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s t : set α} :
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}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s : finset ι}
{t : ι → set α} :
theorem
measure_theory.measure.restrict_bUnion_congr
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{s : set ι}
{t : ι → set α}
(hc : s.countable) :
theorem
measure_theory.measure.restrict_Inf_eq_Inf_restrict
{α : Type u_1}
{t : set α}
{m0 : measurable_space α}
{m : set (measure_theory.measure α)}
(hm : m.nonempty)
(ht : measurable_set t) :
(has_Inf.Inf m).restrict t = has_Inf.Inf ((λ (μ : measure_theory.measure α), μ.restrict t) '' m)
This lemma shows that Inf and restrict commute for measures.
Extensionality results #
theorem
measure_theory.measure.ext_iff_of_Union_eq_univ
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(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}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(hs : (⋃ (i : ι), s i) = set.univ) :
Alias of the reverse direction of measure_theory.measure.ext_iff_of_Union_eq_univ.
theorem
measure_theory.measure.ext_iff_of_bUnion_eq_univ
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{S : set ι}
{s : ι → set α}
(hc : S.countable)
(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}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{S : set ι}
{s : ι → set α}
(hc : S.countable)
(hs : (⋃ (i : ι) (H : i ∈ S), s i) = set.univ) :
Alias of the reverse direction of measure_theory.measure.ext_iff_of_bUnion_eq_univ.
theorem
measure_theory.measure.ext_iff_of_sUnion_eq_univ
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{S : set (set α)}
(hc : S.countable)
(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}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{S : set (set α)}
(hc : S.countable)
(hs : ⋃₀ S = set.univ) :
Alias of the reverse direction of measure_theory.measure.ext_iff_of_sUnion_eq_univ.
theorem
measure_theory.measure.ext_of_generate_from_of_cover
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{S T : set (set α)}
(h_gen : m0 = measurable_space.generate_from S)
(hc : T.countable)
(h_inter : is_pi_system S)
(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}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
{S T : set (set α)}
(h_gen : m0 = 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}
{m0 : measurable_space α}
{μ ν : measure_theory.measure α}
(C : set (set α))
(B : ℕ → set α)
(hA : m0 = 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
Instances for measure_theory.measure.dirac
@[protected, instance]
Equations
theorem
measure_theory.measure.le_dirac_apply
{α : Type u_1}
{s : set α}
[measurable_space α]
{a : α} :
s.indicator 1 a ≤ ⇑(measure_theory.measure.dirac a) s
@[simp]
theorem
measure_theory.measure.dirac_apply'
{α : Type u_1}
{s : set α}
[measurable_space α]
(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}
{s : set α}
[measurable_space α]
{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 : α) :
@[simp]
theorem
measure_theory.measure.restrict_singleton
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α)
(a : α) :
μ.restrict {a} = ⇑μ {a} • measure_theory.measure.dirac a
noncomputable
def
measure_theory.measure.sum
{α : Type u_1}
{ι : Type u_5}
{m0 : 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 _
Instances for measure_theory.measure.sum
theorem
measure_theory.measure.le_sum_apply
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
(f : ι → measure_theory.measure α)
(s : set α) :
@[simp]
theorem
measure_theory.measure.sum_apply
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
(f : ι → measure_theory.measure α)
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.le_sum
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
(μ : ι → measure_theory.measure α)
(i : ι) :
μ i ≤ measure_theory.measure.sum μ
@[simp]
theorem
measure_theory.measure.sum_apply_eq_zero
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
[countable ι]
{μ : ι → measure_theory.measure α}
{s : set α} :
theorem
measure_theory.measure.sum_apply_eq_zero'
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ : ι → measure_theory.measure α}
{s : set α}
(hs : measurable_set s) :
theorem
measure_theory.measure.sum_comm
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{ι' : Type u_2}
(μ : ι → ι' → measure_theory.measure α) :
measure_theory.measure.sum (λ (n : ι), measure_theory.measure.sum (μ n)) = measure_theory.measure.sum (λ (m : ι'), measure_theory.measure.sum (λ (n : ι), μ n m))
theorem
measure_theory.measure.ae_sum_iff
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
[countable ι]
{μ : ι → measure_theory.measure α}
{p : α → Prop} :
theorem
measure_theory.measure.ae_sum_iff'
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ : ι → measure_theory.measure α}
{p : α → Prop}
(h : measurable_set {x : α | p x}) :
@[simp]
theorem
measure_theory.measure.sum_fintype
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
[fintype ι]
(μ : ι → measure_theory.measure α) :
measure_theory.measure.sum μ = finset.univ.sum (λ (i : ι), μ i)
@[simp]
theorem
measure_theory.measure.sum_coe_finset
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
(s : finset ι)
(μ : ι → measure_theory.measure α) :
measure_theory.measure.sum (λ (i : ↥s), μ ↑i) = s.sum (λ (i : ι), μ i)
@[simp]
theorem
measure_theory.measure.ae_sum_eq
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
[countable ι]
(μ : ι → measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.sum_bool
{α : Type u_1}
{m0 : measurable_space α}
(f : bool → measure_theory.measure α) :
@[simp]
theorem
measure_theory.measure.sum_cond
{α : Type u_1}
{m0 : 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}
{m0 : 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)
@[simp]
theorem
measure_theory.measure.sum_of_empty
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
[is_empty ι]
(μ : ι → measure_theory.measure α) :
theorem
measure_theory.measure.sum_add_sum_compl
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
(s : set ι)
(μ : ι → measure_theory.measure α) :
measure_theory.measure.sum (λ (i : ↥s), μ ↑i) + measure_theory.measure.sum (λ (i : ↥sᶜ), μ ↑i) = measure_theory.measure.sum μ
theorem
measure_theory.measure.sum_congr
{α : Type u_1}
{m0 : measurable_space α}
{μ ν : ℕ → measure_theory.measure α}
(h : ∀ (n : ℕ), μ n = ν n) :
theorem
measure_theory.measure.sum_add_sum
{α : Type u_1}
{m0 : measurable_space α}
(μ ν : ℕ → measure_theory.measure α) :
measure_theory.measure.sum μ + measure_theory.measure.sum ν = measure_theory.measure.sum (λ (n : ℕ), μ n + ν n)
theorem
measure_theory.measure.map_eq_sum
{α : Type u_1}
{β : Type u_2}
{m0 : measurable_space α}
[measurable_space β]
[countable β]
[measurable_singleton_class β]
(μ : measure_theory.measure α)
(f : α → β)
(hf : measurable f) :
measure_theory.measure.map f μ = measure_theory.measure.sum (λ (b : β), ⇑μ (f ⁻¹' {b}) • measure_theory.measure.dirac b)
If f is a map with countable codomain, then μ.map f is a sum of Dirac measures.
@[simp]
theorem
measure_theory.measure.sum_smul_dirac
{α : Type u_1}
{m0 : measurable_space α}
[countable α]
[measurable_singleton_class α]
(μ : measure_theory.measure α) :
measure_theory.measure.sum (λ (a : α), ⇑μ {a} • measure_theory.measure.dirac a) = μ
A measure on a countable type is a sum of Dirac measures.
theorem
measure_theory.measure.tsum_indicator_apply_singleton
{α : Type u_1}
{m0 : measurable_space α}
[countable α]
[measurable_singleton_class α]
(μ : measure_theory.measure α)
(s : set α)
(hs : measurable_set s) :
Given that α is a countable, measurable space with all singleton sets measurable,
write the measure of a set s as the sum of the measure of {x} for all x ∈ s.
theorem
measure_theory.measure.restrict_Union_ae
{α : Type u_1}
{ι : Type u_5}
{m0 : measurable_space α}
{μ : measure_theory.measure α}
[countable ι]
{s : ι → set α}
(hd : pairwise (measure_theory.ae_disjoint μ on s))
(hm : ∀ (i : ι),