Measure spaces #
The definition of a measure and a measure space are in MeasureTheory.MeasureSpaceDef, 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 MeasureSpaceDef, and to
be available in MeasureSpace (through MeasurableSpace).
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∞.
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.ofMeasurableandOuterMeasure.toMeasureare 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.ofMeasurableis a way to define a measure by only giving its value on measurable sets and proving the properties (1) and (2) mentioned above.OuterMeasure.toMeasureis 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_generateFrom_of_iUnion: 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_generateFrom_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_generateFrom_of_iUnionusingC ∪ {univ}, but is easier to work with.
A MeasureSpace 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
instance
MeasureTheory.ae_isMeasurablyGenerated
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
(MeasureTheory.ae μ).IsMeasurablyGenerated
theorem
MeasureTheory.ae_uIoc_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[LinearOrder α]
{a b : α}
{P : α → Prop}
:
See also MeasureTheory.ae_restrict_uIoc_iff.
theorem
MeasureTheory.measure_union
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(hd : Disjoint s₁ s₂)
(h : MeasurableSet s₂)
:
theorem
MeasureTheory.measure_union'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(hd : Disjoint s₁ s₂)
(h : MeasurableSet s₁)
:
theorem
MeasureTheory.measure_inter_add_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.measure_diff_add_inter
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.measure_union_add_inter
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.measure_union_add_inter'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(t : Set α)
:
theorem
MeasureTheory.measure_symmDiff_eq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(ht : MeasureTheory.NullMeasurableSet t μ)
:
theorem
MeasureTheory.measure_symmDiff_le
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s t u : Set α)
:
theorem
MeasureTheory.measure_add_measure_compl
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : MeasurableSet s)
:
theorem
MeasureTheory.measure_biUnion₀
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set β}
{f : β → Set α}
(hs : s.Countable)
(hd : s.Pairwise (MeasureTheory.AEDisjoint μ on f))
(h : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ)
:
μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
theorem
MeasureTheory.measure_biUnion
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set β}
{f : β → Set α}
(hs : s.Countable)
(hd : s.PairwiseDisjoint f)
(h : ∀ b ∈ s, MeasurableSet (f b))
:
μ (⋃ b ∈ s, f b) = ∑' (p : ↑s), μ (f ↑p)
theorem
MeasureTheory.measure_sUnion₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{S : Set (Set α)}
(hs : S.Countable)
(hd : S.Pairwise (MeasureTheory.AEDisjoint μ))
(h : ∀ s ∈ S, MeasureTheory.NullMeasurableSet s μ)
:
theorem
MeasureTheory.measure_sUnion
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{S : Set (Set α)}
(hs : S.Countable)
(hd : S.Pairwise Disjoint)
(h : ∀ s ∈ S, MeasurableSet s)
:
theorem
MeasureTheory.measure_biUnion_finset₀
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Finset ι}
{f : ι → Set α}
(hd : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on f))
(hm : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ)
:
μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
theorem
MeasureTheory.measure_biUnion_finset
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Finset ι}
{f : ι → Set α}
(hd : (↑s).PairwiseDisjoint f)
(hm : ∀ b ∈ s, MeasurableSet (f b))
:
μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p)
theorem
MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀
{α : Type u_1}
{ι : Type u_8}
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{As : ι → Set α}
(As_mble : ∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ)
(As_disj : Pairwise (MeasureTheory.AEDisjoint μ on As))
:
∑' (i : ι), μ (As i) ≤ μ (⋃ (i : ι), As i)
The measure of an a.e. disjoint union (even uncountable) of null-measurable sets is at least the sum of the measures of the sets.
theorem
MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint
{α : Type u_1}
{ι : Type u_8}
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{As : ι → Set α}
(As_mble : ∀ (i : ι), MeasurableSet (As i))
(As_disj : Pairwise (Disjoint on As))
:
∑' (i : ι), μ (As i) ≤ μ (⋃ (i : ι), As i)
The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of the measures of the sets.
theorem
MeasureTheory.tsum_measure_preimage_singleton
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set β}
(hs : s.Countable)
{f : α → β}
(hf : ∀ y ∈ s, MeasurableSet (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
MeasureTheory.measure_preimage_eq_zero_iff_of_countable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set β}
{f : α → β}
(hs : s.Countable)
:
theorem
MeasureTheory.sum_measure_preimage_singleton
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Finset β)
{f : α → β}
(hf : ∀ y ∈ s, MeasurableSet (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
MeasureTheory.measure_diff_null'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h : μ (s₁ ∩ s₂) = 0)
:
theorem
MeasureTheory.measure_add_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(t : Set α)
:
theorem
MeasureTheory.measure_diff'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(hm : MeasureTheory.NullMeasurableSet t μ)
(h_fin : μ t ≠ ⊤)
:
theorem
MeasureTheory.measure_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
(h : s₂ ⊆ s₁)
(h₂ : MeasureTheory.NullMeasurableSet s₂ μ)
(h_fin : μ s₂ ≠ ⊤)
:
theorem
MeasureTheory.le_measure_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ : Set α}
:
theorem
MeasureTheory.measure_eq_top_iff_of_symmDiff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hμst : μ (symmDiff s t) ≠ ⊤)
:
If the measure of the symmetric difference of two sets is finite, then one has infinite measure if and only if the other one does.
theorem
MeasureTheory.measure_ne_top_iff_of_symmDiff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hμst : μ (symmDiff s t) ≠ ⊤)
:
If the measure of the symmetric difference of two sets is finite, then one has finite measure if and only if the other one does.
theorem
MeasureTheory.measure_diff_lt_of_lt_add
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(hst : s ⊆ t)
(hs' : μ s ≠ ⊤)
{ε : ENNReal}
(h : μ t < μ s + ε)
:
theorem
MeasureTheory.measure_diff_le_iff_le_add
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(hst : s ⊆ t)
(hs' : μ s ≠ ⊤)
{ε : ENNReal}
:
theorem
MeasureTheory.measure_eq_measure_of_null_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hst : s ⊆ t)
(h_nulldiff : μ (t \ s) = 0)
:
μ s = μ t
theorem
MeasureTheory.measure_eq_measure_of_between_null_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ s₃ : Set α}
(h12 : s₁ ⊆ s₂)
(h23 : s₂ ⊆ s₃)
(h_nulldiff : μ (s₃ \ s₁) = 0)
:
theorem
MeasureTheory.measure_eq_measure_smaller_of_between_null_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ s₃ : Set α}
(h12 : s₁ ⊆ s₂)
(h23 : s₂ ⊆ s₃)
(h_nulldiff : μ (s₃ \ s₁) = 0)
:
μ s₁ = μ s₂
theorem
MeasureTheory.measure_eq_measure_larger_of_between_null_diff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ s₃ : Set α}
(h12 : s₁ ⊆ s₂)
(h23 : s₂ ⊆ s₃)
(h_nulldiff : μ (s₃ \ s₁) = 0)
:
μ s₂ = μ s₃
theorem
MeasureTheory.measure_compl₀
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.NullMeasurableSet s μ)
(hs : μ s ≠ ⊤)
:
theorem
MeasureTheory.measure_compl
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h₁ : MeasurableSet s)
(h_fin : μ s ≠ ⊤)
:
theorem
MeasureTheory.measure_inter_conull'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(ht : μ (s \ t) = 0)
:
theorem
MeasureTheory.measure_inter_conull
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(ht : μ tᶜ = 0)
:
@[simp]
theorem
MeasureTheory.union_ae_eq_left_iff_ae_subset
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
:
@[simp]
theorem
MeasureTheory.union_ae_eq_right_iff_ae_subset
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
:
theorem
MeasureTheory.ae_eq_of_ae_subset_of_measure_ge
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h₁ : s ≤ᵐ[μ] t)
(h₂ : μ t ≤ μ s)
(hsm : MeasureTheory.NullMeasurableSet s μ)
(ht : μ t ≠ ⊤)
:
theorem
MeasureTheory.ae_eq_of_subset_of_measure_ge
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h₁ : s ⊆ t)
(h₂ : μ t ≤ μ s)
(hsm : MeasureTheory.NullMeasurableSet s μ)
(ht : μ t ≠ ⊤)
:
If s ⊆ t, μ t ≤ μ s, μ t ≠ ∞, and s is measurable, then s =ᵐ[μ] t.
theorem
MeasureTheory.measure_iUnion_congr_of_subset
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Sort u_8}
[Countable ι]
{s t : ι → Set α}
(hsub : ∀ (i : ι), s i ⊆ t i)
(h_le : ∀ (i : ι), μ (t i) ≤ μ (s i))
:
μ (⋃ (i : ι), s i) = μ (⋃ (i : ι), t i)
theorem
MeasureTheory.measure_union_congr_of_subset
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s₁ s₂ t₁ t₂ : Set α}
(hs : s₁ ⊆ s₂)
(hsμ : μ s₂ ≤ μ s₁)
(ht : t₁ ⊆ t₂)
(htμ : μ t₂ ≤ μ t₁)
:
@[simp]
theorem
MeasureTheory.measure_iUnion_toMeasurable
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Sort u_8}
[Countable ι]
(s : ι → Set α)
:
μ (⋃ (i : ι), MeasureTheory.toMeasurable μ (s i)) = μ (⋃ (i : ι), s i)
theorem
MeasureTheory.measure_biUnion_toMeasurable
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{I : Set β}
(hc : I.Countable)
(s : β → Set α)
:
μ (⋃ b ∈ I, MeasureTheory.toMeasurable μ (s b)) = μ (⋃ b ∈ I, s b)
@[simp]
theorem
MeasureTheory.measure_toMeasurable_union
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
:
μ (MeasureTheory.toMeasurable μ s ∪ t) = μ (s ∪ t)
@[simp]
theorem
MeasureTheory.measure_union_toMeasurable
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
:
μ (s ∪ MeasureTheory.toMeasurable μ t) = μ (s ∪ t)
theorem
MeasureTheory.sum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Finset ι}
{t : ι → Set α}
(h : ∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ)
(H : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on t))
:
∑ i ∈ s, μ (t i) ≤ μ Set.univ
theorem
MeasureTheory.tsum_measure_le_measure_univ
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : ι → Set α}
(hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(H : Pairwise (MeasureTheory.AEDisjoint μ on s))
:
∑' (i : ι), μ (s i) ≤ μ Set.univ
theorem
MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{s : ι → Set α}
(hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (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
MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{s : Finset ι}
{t : ι → Set α}
(h : ∀ i ∈ s, MeasureTheory.NullMeasurableSet (t i) μ)
(H : μ Set.univ < ∑ i ∈ s, μ (t i))
:
Pigeonhole principle for measure spaces: if s is a Finset and
∑ i ∈ s, μ (t i) > μ univ, then one of the intersections t i ∩ t j is not empty.
theorem
MeasureTheory.nonempty_inter_of_measure_lt_add
{α : Type u_1}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{s t u : Set α}
(ht : MeasurableSet t)
(h's : s ⊆ u)
(h't : t ⊆ u)
(h : μ u < μ s + μ t)
:
(s ∩ t).Nonempty
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
MeasureTheory.nonempty_inter_of_measure_lt_add'
{α : Type u_1}
{m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{s t u : Set α}
(hs : MeasurableSet s)
(h's : s ⊆ u)
(h't : t ⊆ u)
(h : μ u < μ s + μ t)
:
(s ∩ t).Nonempty
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
Directed.measure_iUnion
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s)
:
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)
Continuity from below: the measure of the union of a directed sequence of (not necessarily measurable) sets is the supremum of the measures.
@[deprecated Directed.measure_iUnion]
theorem
MeasureTheory.measure_iUnion_eq_iSup
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s)
:
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)
Alias of Directed.measure_iUnion.
Continuity from below: the measure of the union of a directed sequence of (not necessarily measurable) sets is the supremum of the measures.
theorem
Monotone.measure_iUnion
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hs : Monotone s)
:
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)
Continuity from below:
the measure of the union of a monotone family of sets is equal to the supremum of their measures.
The theorem assumes that the atTop filter on the index set is countably generated,
so it works for a family indexed by a countable type, as well as ℝ.
theorem
Antitone.measure_iUnion
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≥ x2]
[Filter.atBot.IsCountablyGenerated]
{s : ι → Set α}
(hs : Antitone s)
:
μ (⋃ (i : ι), s i) = ⨆ (i : ι), μ (s i)
theorem
MeasureTheory.measure_iUnion_eq_iSup_accumulate
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Filter.atTop.IsCountablyGenerated]
{f : ι → Set α}
:
μ (⋃ (i : ι), f i) = ⨆ (i : ι), μ (Set.Accumulate f i)
Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the supremum of the measures of the partial unions.
@[deprecated MeasureTheory.measure_iUnion_eq_iSup_accumulate]
theorem
MeasureTheory.measure_iUnion_eq_iSup'
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Filter.atTop.IsCountablyGenerated]
{f : ι → Set α}
:
μ (⋃ (i : ι), f i) = ⨆ (i : ι), μ (Set.Accumulate f i)
Alias of MeasureTheory.measure_iUnion_eq_iSup_accumulate.
Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the supremum of the measures of the partial unions.
theorem
MeasureTheory.measure_biUnion_eq_iSup
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : ι → Set α}
{t : Set ι}
(ht : t.Countable)
(hd : DirectedOn ((fun (x1 x2 : Set α) => x1 ⊆ x2) on s) t)
:
μ (⋃ i ∈ t, s i) = ⨆ i ∈ t, μ (s i)
theorem
Directed.measure_iInter
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s)
(hfin : ∃ (i : ι), μ (s i) ≠ ⊤)
:
μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)
Continuity from above: the measure of the intersection of a directed downwards countable family of measurable sets is the infimum of the measures.
@[deprecated Directed.measure_iInter]
theorem
MeasureTheory.measure_iInter_eq_iInf
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hd : Directed (fun (x1 x2 : Set α) => x1 ⊇ x2) s)
(hfin : ∃ (i : ι), μ (s i) ≠ ⊤)
:
μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)
Alias of Directed.measure_iInter.
Continuity from above: the measure of the intersection of a directed downwards countable family of measurable sets is the infimum of the measures.
theorem
Monotone.measure_iInter
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≥ x2]
[Filter.atBot.IsCountablyGenerated]
{s : ι → Set α}
(hs : Monotone s)
(hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hfin : ∃ (i : ι), μ (s i) ≠ ⊤)
:
μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)
Continuity from above:
the measure of the intersection of a monotone family of measurable sets
indexed by a type with countably generated atBot filter
is equal to the infimum of the measures.
theorem
Antitone.measure_iInter
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hs : Antitone s)
(hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hfin : ∃ (i : ι), μ (s i) ≠ ⊤)
:
μ (⋂ (i : ι), s i) = ⨅ (i : ι), μ (s i)
Continuity from above:
the measure of the intersection of an antitone family of measurable sets
indexed by a type with countably generated atTop filter
is equal to the infimum of the measures.
theorem
MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le
{α : Type u_8}
{ι : Type u_9}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{f : ι → Set α}
(h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ)
(hfin : ∃ (i : ι), μ (f i) ≠ ⊤)
:
Continuity from above: the measure of the intersection of a sequence of measurable sets is the infimum of the measures of the partial intersections.
@[deprecated MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le]
theorem
MeasureTheory.measure_iInter_eq_iInf'
{α : Type u_8}
{ι : Type u_9}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{f : ι → Set α}
(h : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ)
(hfin : ∃ (i : ι), μ (f i) ≠ ⊤)
:
Alias of MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le.
Continuity from above: the measure of the intersection of a sequence of measurable sets is the infimum of the measures of the partial intersections.
theorem
MeasureTheory.tendsto_measure_iUnion_atTop
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hm : Monotone s)
:
Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋃ (n : ι), s n)))
Continuity from below: the measure of the union of an increasing sequence of (not necessarily measurable) sets is the limit of the measures.
@[deprecated MeasureTheory.tendsto_measure_iUnion_atTop]
theorem
MeasureTheory.tendsto_measure_iUnion
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hm : Monotone s)
:
Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋃ (n : ι), s n)))
Alias of MeasureTheory.tendsto_measure_iUnion_atTop.
Continuity from below: the measure of the union of an increasing sequence of (not necessarily measurable) sets is the limit of the measures.
theorem
MeasureTheory.tendsto_measure_iUnion_atBot
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[Filter.atBot.IsCountablyGenerated]
{s : ι → Set α}
(hm : Antitone s)
:
Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋃ (n : ι), s n)))
theorem
MeasureTheory.tendsto_measure_iUnion_accumulate
{α : Type u_8}
{ι : Type u_9}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → Set α}
:
Filter.Tendsto (fun (i : ι) => μ (Set.Accumulate f i)) Filter.atTop (nhds (μ (⋃ (i : ι), f i)))
Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the limit of the measures of the partial unions.
@[deprecated MeasureTheory.tendsto_measure_iUnion_accumulate]
theorem
MeasureTheory.tendsto_measure_iUnion'
{α : Type u_8}
{ι : Type u_9}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : ι → Set α}
:
Filter.Tendsto (fun (i : ι) => μ (Set.Accumulate f i)) Filter.atTop (nhds (μ (⋃ (i : ι), f i)))
Alias of MeasureTheory.tendsto_measure_iUnion_accumulate.
Continuity from below: the measure of the union of a sequence of (not necessarily measurable) sets is the limit of the measures of the partial unions.
theorem
MeasureTheory.tendsto_measure_iInter_atTop
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hm : Antitone s)
(hf : ∃ (i : ι), μ (s i) ≠ ⊤)
:
Filter.Tendsto (⇑μ ∘ s) Filter.atTop (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.
@[deprecated MeasureTheory.tendsto_measure_iInter_atTop]
theorem
MeasureTheory.tendsto_measure_iInter
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[Filter.atTop.IsCountablyGenerated]
{s : ι → Set α}
(hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hm : Antitone s)
(hf : ∃ (i : ι), μ (s i) ≠ ⊤)
:
Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋂ (n : ι), s n)))
Alias of MeasureTheory.tendsto_measure_iInter_atTop.
Continuity from above: the measure of the intersection of a decreasing sequence of measurable sets is the limit of the measures.
theorem
MeasureTheory.tendsto_measure_iInter_atBot
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder ι]
[Filter.atBot.IsCountablyGenerated]
{s : ι → Set α}
(hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
(hm : Monotone s)
(hf : ∃ (i : ι), μ (s i) ≠ ⊤)
:
Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋂ (n : ι), s n)))
Continuity from above: the measure of the intersection of an increasing sequence of measurable sets is the limit of the measures.
theorem
MeasureTheory.tendsto_measure_iInter_le
{α : Type u_8}
{ι : Type u_9}
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
[Preorder ι]
{f : ι → Set α}
(hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (f i) μ)
(hf : ∃ (i : ι), μ (f i) ≠ ⊤)
:
Filter.Tendsto (fun (i : ι) => μ (⋂ (j : ι), ⋂ (_ : j ≤ i), f j)) Filter.atTop (nhds (μ (⋂ (i : ι), f i)))
Continuity from above: the measure of the intersection of a sequence of measurable sets such that one has finite measure is the limit of the measures of the partial intersections.
theorem
MeasureTheory.tendsto_measure_biInter_gt
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_8}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[DenselyOrdered ι]
[FirstCountableTopology ι]
{s : ι → Set α}
{a : ι}
(hs : ∀ r > a, MeasureTheory.NullMeasurableSet (s r) μ)
(hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j)
(hf : ∃ r > a, μ (s r) ≠ ⊤)
:
Filter.Tendsto (⇑μ ∘ s) (nhdsWithin a (Set.Ioi a)) (nhds (μ (⋂ (r : ι), ⋂ (_ : 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
MeasureTheory.measure_if
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{x : β}
{t : Set β}
{s : Set α}
[Decidable (x ∈ t)]
:
def
MeasureTheory.OuterMeasure.toMeasure
{α : Type u_1}
[ms : MeasurableSpace α]
(m : MeasureTheory.OuterMeasure α)
(h : ms ≤ m.caratheodory)
:
Obtain a measure by giving an outer measure where all sets in the σ-algebra are Carathéodory measurable.
Equations
- m.toMeasure h = MeasureTheory.Measure.ofMeasurable (fun (s : Set α) (x : MeasurableSet s) => m s) ⋯ ⋯
Instances For
theorem
MeasureTheory.le_toOuterMeasure_caratheodory
{α : Type u_1}
[ms : MeasurableSpace α]
(μ : MeasureTheory.Measure α)
:
ms ≤ μ.caratheodory
@[simp]
theorem
MeasureTheory.toMeasure_toOuterMeasure
{α : Type u_1}
[ms : MeasurableSpace α]
(m : MeasureTheory.OuterMeasure α)
(h : ms ≤ m.caratheodory)
:
(m.toMeasure h).toOuterMeasure = m.trim
@[simp]
theorem
MeasureTheory.toMeasure_apply
{α : Type u_1}
[ms : MeasurableSpace α]
(m : MeasureTheory.OuterMeasure α)
(h : ms ≤ m.caratheodory)
{s : Set α}
(hs : MeasurableSet s)
:
(m.toMeasure h) s = m s
theorem
MeasureTheory.le_toMeasure_apply
{α : Type u_1}
[ms : MeasurableSpace α]
(m : MeasureTheory.OuterMeasure α)
(h : ms ≤ m.caratheodory)
(s : Set α)
:
m s ≤ (m.toMeasure h) s
theorem
MeasureTheory.toMeasure_apply₀
{α : Type u_1}
[ms : MeasurableSpace α]
(m : MeasureTheory.OuterMeasure α)
(h : ms ≤ m.caratheodory)
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s (m.toMeasure h))
:
(m.toMeasure h) s = m s
@[simp]
theorem
MeasureTheory.toOuterMeasure_toMeasure
{α : Type u_1}
[ms : MeasurableSpace α]
{μ : MeasureTheory.Measure α}
:
μ.toMeasure ⋯ = μ
@[simp]
theorem
MeasureTheory.boundedBy_measure
{α : Type u_1}
[ms : MeasurableSpace α]
(μ : MeasureTheory.Measure α)
:
MeasureTheory.OuterMeasure.boundedBy ⇑μ = μ.toOuterMeasure
theorem
MeasureTheory.Measure.measure_inter_eq_of_measure_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t u : Set α}
(hs : MeasurableSet 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
MeasureTheory.Measure.measure_toMeasurable_inter
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasurableSet s)
(ht : μ t ≠ ⊤)
:
μ (MeasureTheory.toMeasurable μ t ∩ s) = μ (t ∩ s)
The measurable superset toMeasurable μ t of t (which has the same measure as t)
satisfies, for any measurable set s, the equality μ (toMeasurable μ t ∩ s) = μ (u ∩ s).
Here, we require that the measure of t is finite. The conclusion holds without this assumption
when the measure is s-finite (for example when it is σ-finite),
see measure_toMeasurable_inter_of_sFinite.
The ℝ≥0∞-module of measures #
Equations
- MeasureTheory.Measure.instZero = { zero := { toOuterMeasure := 0, m_iUnion := ⋯, trim_le := ⋯ } }
@[simp]
@[simp]
@[simp]
theorem
MeasureTheory.OuterMeasure.toMeasure_zero
{α : Type u_1}
[ms : MeasurableSpace α]
(h : ms ≤ MeasureTheory.OuterMeasure.caratheodory 0)
:
@[simp]
theorem
MeasureTheory.OuterMeasure.toMeasure_eq_zero
{α : Type u_1}
{ms : MeasurableSpace α}
{μ : MeasureTheory.OuterMeasure α}
(h : ms ≤ μ.caratheodory)
:
theorem
MeasureTheory.Measure.apply_eq_zero_of_isEmpty
{α : Type u_1}
[IsEmpty α]
{x✝ : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(s : Set α)
:
μ s = 0
instance
MeasureTheory.Measure.instSubsingleton
{α : Type u_1}
[IsEmpty α]
{m : MeasurableSpace α}
:
theorem
MeasureTheory.Measure.eq_zero_of_isEmpty
{α : Type u_1}
[IsEmpty α]
{_m : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
μ = 0
Equations
- MeasureTheory.Measure.instInhabited = { default := 0 }
Equations
- MeasureTheory.Measure.instAdd = { add := fun (μ₁ μ₂ : MeasureTheory.Measure α) => { toOuterMeasure := μ₁.toOuterMeasure + μ₂.toOuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } }
@[simp]
theorem
MeasureTheory.Measure.add_toOuterMeasure
{α : Type u_1}
{_m : MeasurableSpace α}
(μ₁ μ₂ : MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.coe_add
{α : Type u_1}
{_m : MeasurableSpace α}
(μ₁ μ₂ : MeasureTheory.Measure α)
:
theorem
MeasureTheory.Measure.add_apply
{α : Type u_1}
{_m : MeasurableSpace α}
(μ₁ μ₂ : MeasureTheory.Measure α)
(s : Set α)
:
instance
MeasureTheory.Measure.instSMul
{α : Type u_1}
{R : Type u_6}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{x✝ : MeasurableSpace α}
:
SMul R (MeasureTheory.Measure α)
Equations
- MeasureTheory.Measure.instSMul = { smul := fun (c : R) (μ : MeasureTheory.Measure α) => { toOuterMeasure := c • μ.toOuterMeasure, m_iUnion := ⋯, trim_le := ⋯ } }
@[simp]
theorem
MeasureTheory.Measure.smul_toOuterMeasure
{α : Type u_1}
{R : Type u_6}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{_m : MeasurableSpace α}
(c : R)
(μ : MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.coe_smul
{α : Type u_1}
{R : Type u_6}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{_m : MeasurableSpace α}
(c : R)
(μ : MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.smul_apply
{α : Type u_1}
{R : Type u_6}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{_m : MeasurableSpace α}
(c : R)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
instance
MeasureTheory.Measure.instSMulCommClass
{α : Type u_1}
{R : Type u_6}
{R' : Type u_7}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[SMul R' ENNReal]
[IsScalarTower R' ENNReal ENNReal]
[SMulCommClass R R' ENNReal]
{x✝ : MeasurableSpace α}
:
SMulCommClass R R' (MeasureTheory.Measure α)
instance
MeasureTheory.Measure.instIsScalarTower
{α : Type u_1}
{R : Type u_6}
{R' : Type u_7}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[SMul R' ENNReal]
[IsScalarTower R' ENNReal ENNReal]
[SMul R R']
[IsScalarTower R R' ENNReal]
{x✝ : MeasurableSpace α}
:
IsScalarTower R R' (MeasureTheory.Measure α)
instance
MeasureTheory.Measure.instIsCentralScalar
{α : Type u_1}
{R : Type u_6}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[SMul Rᵐᵒᵖ ENNReal]
[IsCentralScalar R ENNReal]
{x✝ : MeasurableSpace α}
:
instance
MeasureTheory.Measure.instNoZeroSMulDivisors
{α : Type u_1}
{R : Type u_6}
{m0 : MeasurableSpace α}
[Zero R]
[SMulWithZero R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[NoZeroSMulDivisors R ENNReal]
:
instance
MeasureTheory.Measure.instMulAction
{α : Type u_1}
{R : Type u_6}
[Monoid R]
[MulAction R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{x✝ : MeasurableSpace α}
:
Equations
- MeasureTheory.Measure.instMulAction = Function.Injective.mulAction MeasureTheory.Measure.toOuterMeasure ⋯ ⋯
Equations
- MeasureTheory.Measure.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.Measure.toOuterMeasure ⋯ ⋯ ⋯ ⋯
def
MeasureTheory.Measure.coeAddHom
{α : Type u_1}
{x✝ : MeasurableSpace α}
:
MeasureTheory.Measure α →+ Set α → ENNReal
Coercion to function as an additive monoid homomorphism.
Equations
- MeasureTheory.Measure.coeAddHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
MeasureTheory.Measure.coe_finset_sum
{α : Type u_1}
{ι : Type u_5}
{_m : MeasurableSpace α}
(I : Finset ι)
(μ : ι → MeasureTheory.Measure α)
:
⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i)
theorem
MeasureTheory.Measure.finset_sum_apply
{α : Type u_1}
{ι : Type u_5}
{m : MeasurableSpace α}
(I : Finset ι)
(μ : ι → MeasureTheory.Measure α)
(s : Set α)
:
(∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s
instance
MeasureTheory.Measure.instDistribMulAction
{α : Type u_1}
{R : Type u_6}
[Monoid R]
[DistribMulAction R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{x✝ : MeasurableSpace α}
:
Equations
- MeasureTheory.Measure.instDistribMulAction = Function.Injective.distribMulAction { toFun := MeasureTheory.Measure.toOuterMeasure, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
instance
MeasureTheory.Measure.instModule
{α : Type u_1}
{R : Type u_6}
[Semiring R]
[Module R ENNReal]
[IsScalarTower R ENNReal ENNReal]
{x✝ : MeasurableSpace α}
:
Module R (MeasureTheory.Measure α)
Equations
- MeasureTheory.Measure.instModule = Function.Injective.module R { toFun := MeasureTheory.Measure.toOuterMeasure, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
@[simp]
theorem
MeasureTheory.Measure.coe_nnreal_smul_apply
{α : Type u_1}
{_m : MeasurableSpace α}
(c : NNReal)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
@[simp]
theorem
MeasureTheory.Measure.nnreal_smul_coe_apply
{α : Type u_1}
{_m : MeasurableSpace α}
(c : NNReal)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
theorem
MeasureTheory.Measure.ae_smul_measure
{α : Type u_1}
{R : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : ∀ᵐ (x : α) ∂μ, p x)
(c : R)
:
∀ᵐ (x : α) ∂c • μ, p x
theorem
MeasureTheory.Measure.ae_smul_measure_le
{α : Type u_1}
{R : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(c : R)
:
MeasureTheory.ae (c • μ) ≤ MeasureTheory.ae μ
theorem
MeasureTheory.Measure.ae_smul_measure_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{R : Type u_8}
[Zero R]
[SMulWithZero R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[NoZeroSMulDivisors R ENNReal]
{c : R}
{p : α → Prop}
(hc : c ≠ 0)
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.ae_smul_measure_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{R : Type u_8}
[Zero R]
[SMulWithZero R ENNReal]
[IsScalarTower R ENNReal ENNReal]
[NoZeroSMulDivisors R ENNReal]
{c : R}
(hc : c ≠ 0)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.ae (c • μ) = MeasureTheory.ae μ
theorem
MeasureTheory.Measure.measure_eq_left_of_subset_of_measure_add_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s t : Set α}
(h : (μ + ν) t ≠ ⊤)
(h' : s ⊆ t)
(h'' : (μ + ν) s = (μ + ν) t)
:
μ s = μ t
theorem
MeasureTheory.Measure.measure_eq_right_of_subset_of_measure_add_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s t : Set α}
(h : (μ + ν) t ≠ ⊤)
(h' : s ⊆ t)
(h'' : (μ + ν) s = (μ + ν) t)
:
ν s = ν t
theorem
MeasureTheory.Measure.measure_toMeasurable_add_inter_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasurableSet s)
(ht : (μ + ν) t ≠ ⊤)
:
μ (MeasureTheory.toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)
theorem
MeasureTheory.Measure.measure_toMeasurable_add_inter_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s t : Set α}
(hs : MeasurableSet s)
(ht : (μ + ν) t ≠ ⊤)
:
ν (MeasureTheory.toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s)
The complete lattice of measures #
Measures are partially ordered.
Equations
- MeasureTheory.Measure.instPartialOrder = PartialOrder.mk ⋯
theorem
MeasureTheory.Measure.toOuterMeasure_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.le_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ : MeasureTheory.Measure α}
:
μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → μ₁ s ≤ μ₂ s
theorem
MeasureTheory.Measure.le_intro
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ : MeasureTheory.Measure α}
(h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s)
:
μ₁ ≤ μ₂
theorem
MeasureTheory.Measure.le_iff'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.lt_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.lt_iff'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.le_add_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν ν' : MeasureTheory.Measure α}
(h : μ ≤ ν)
:
theorem
MeasureTheory.Measure.le_add_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν ν' : MeasureTheory.Measure α}
(h : μ ≤ ν)
:
theorem
MeasureTheory.Measure.sInf_caratheodory
{α : Type u_1}
{m0 : MeasurableSpace α}
{m : Set (MeasureTheory.Measure α)}
(s : Set α)
(hs : MeasurableSet s)
:
Equations
- MeasureTheory.Measure.instInfSet = { sInf := fun (m : Set (MeasureTheory.Measure α)) => (sInf (MeasureTheory.Measure.toOuterMeasure '' m)).toMeasure ⋯ }
theorem
MeasureTheory.Measure.sInf_apply
{α : Type u_1}
{m0 : MeasurableSpace α}
{s : Set α}
{m : Set (MeasureTheory.Measure α)}
(hs : MeasurableSet s)
:
Equations
- MeasureTheory.Measure.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯
Equations
- MeasureTheory.Measure.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
MeasureTheory.Measure.inf_apply
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
@[simp]
@[simp]
@[simp]
theorem
MeasureTheory.Measure.top_add
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.add_top
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.zero_le
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
0 ≤ μ
theorem
MeasureTheory.Measure.nonpos_iff_eq_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.measure_univ_eq_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.measure_univ_ne_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
instance
MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NeZero μ]
:
NeZero (μ Set.univ)
@[simp]
theorem
MeasureTheory.Measure.measure_univ_pos
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.nonempty_of_neZero
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[NeZero μ]
:
Nonempty α
Pushforward and pullback #
def
MeasureTheory.Measure.liftLinear
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
(f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β)
(hf : ∀ (μ : MeasureTheory.Measure α), inst✝ ≤ (f μ.toOuterMeasure).caratheodory)
:
Lift a linear map between OuterMeasure spaces such that for each measure μ every measurable
set is caratheodory-measurable w.r.t. f μ to a linear map between Measure spaces.
Equations
- MeasureTheory.Measure.liftLinear f hf = { toFun := fun (μ : MeasureTheory.Measure α) => (f μ.toOuterMeasure).toMeasure ⋯, map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
MeasureTheory.Measure.liftLinear_apply₀
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
(hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
{s : Set β}
(hs : MeasureTheory.NullMeasurableSet s ((MeasureTheory.Measure.liftLinear f hf) μ))
:
((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
@[simp]
theorem
MeasureTheory.Measure.liftLinear_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
(hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
{s : Set β}
(hs : MeasurableSet s)
:
((MeasureTheory.Measure.liftLinear f hf) μ) s = (f μ.toOuterMeasure) s
theorem
MeasureTheory.Measure.le_liftLinear_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β}
(hf : ∀ (μ : MeasureTheory.Measure α), mβ ≤ (f μ.toOuterMeasure).caratheodory)
(s : Set β)
:
(f μ.toOuterMeasure) s ≤ ((MeasureTheory.Measure.liftLinear f hf) μ) s
def
MeasureTheory.Measure.mapₗ
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
:
The pushforward of a measure as a linear map. It is defined to be 0 if f is not
a measurable function.
Equations
- MeasureTheory.Measure.mapₗ f = if hf : Measurable f then MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.map f) ⋯ else 0
Instances For
theorem
MeasureTheory.Measure.mapₗ_congr
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
(h : f =ᵐ[μ] g)
:
(MeasureTheory.Measure.mapₗ f) μ = (MeasureTheory.Measure.mapₗ g) μ
@[irreducible]
def
MeasureTheory.Measure.map
{α : Type u_8}
{β : Type u_9}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : MeasureTheory.Measure α)
:
The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere
measurable function.
Equations
- MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
Instances For
theorem
MeasureTheory.Measure.map_def
{α : Type u_8}
{β : Type u_9}
[MeasurableSpace α]
[MeasurableSpace β]
(f : α → β)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.Measure.map f μ = if hf : AEMeasurable f μ then (MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ else 0
theorem
MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
(MeasureTheory.Measure.mapₗ (AEMeasurable.mk f hf)) μ = MeasureTheory.Measure.map f μ
theorem
MeasureTheory.Measure.mapₗ_apply_of_measurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
(hf : Measurable f)
(μ : MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.map_add
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
(μ ν : MeasureTheory.Measure α)
{f : α → β}
(hf : Measurable f)
:
MeasureTheory.Measure.map f (μ + ν) = MeasureTheory.Measure.map f μ + MeasureTheory.Measure.map f ν
@[simp]
theorem
MeasureTheory.Measure.map_zero
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
(f : α → β)
:
MeasureTheory.Measure.map f 0 = 0
@[simp]
theorem
MeasureTheory.Measure.map_of_not_aemeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{f : α → β}
{μ : MeasureTheory.Measure α}
(hf : ¬AEMeasurable f μ)
:
MeasureTheory.Measure.map f μ = 0
theorem
MeasureTheory.Measure.map_congr
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f g : α → β}
(h : f =ᵐ[μ] g)
:
@[simp]
theorem
MeasureTheory.Measure.map_smul
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{R : Type u_8}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(c : R)
(μ : MeasureTheory.Measure α)
(f : α → β)
:
MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
@[deprecated MeasureTheory.Measure.map_smul]
theorem
MeasureTheory.Measure.map_smul_nnreal
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
(c : NNReal)
(μ : MeasureTheory.Measure α)
(f : α → β)
:
MeasureTheory.Measure.map f (c • μ) = c • MeasureTheory.Measure.map f μ
theorem
MeasureTheory.Measure.map_apply₀
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.map f μ))
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
@[simp]
theorem
MeasureTheory.Measure.map_apply_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
We can evaluate the pushforward on measurable sets. For non-measurable sets, see
MeasureTheory.Measure.le_map_apply and MeasurableEquiv.map_apply.
@[simp]
theorem
MeasureTheory.Measure.map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
theorem
MeasureTheory.Measure.map_toOuterMeasure
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
(MeasureTheory.Measure.map f μ).toOuterMeasure = ((MeasureTheory.OuterMeasure.map f) μ.toOuterMeasure).trim
@[simp]
theorem
MeasureTheory.Measure.map_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
MeasureTheory.Measure.map f μ = 0 ↔ μ = 0
@[simp]
theorem
MeasureTheory.Measure.mapₗ_eq_zero_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
:
(MeasureTheory.Measure.mapₗ f) μ = 0 ↔ μ = 0
theorem
MeasureTheory.Measure.measure_preimage_of_map_eq_self
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → α}
(hf : MeasureTheory.Measure.map f μ = μ)
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
If map f μ = μ, then the measure of the preimage of any null measurable set s
is equal to the measure of s.
Note that this lemma does not assume (a.e.) measurability of f.
theorem
MeasureTheory.Measure.map_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
MeasureTheory.Measure.map f μ ≠ 0 ↔ μ ≠ 0
theorem
MeasureTheory.Measure.mapₗ_ne_zero_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
:
(MeasureTheory.Measure.mapₗ f) μ ≠ 0 ↔ μ ≠ 0
@[simp]
theorem
MeasureTheory.Measure.map_id
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.Measure.map id μ = μ
@[simp]
theorem
MeasureTheory.Measure.map_id'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.Measure.map (fun (x : α) => x) μ = μ
theorem
MeasureTheory.Measure.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{g : β → γ}
{f : α → β}
(hg : Measurable g)
(hf : Measurable f)
:
MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
Mapping a measure twice is the same as mapping the measure with the composition. This version is
for measurable functions. See map_map_of_aemeasurable when they are just ae measurable.
theorem
MeasureTheory.Measure.map_mono
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : MeasureTheory.Measure α}
{f : α → β}
(h : μ ≤ ν)
(hf : Measurable f)
:
theorem
MeasureTheory.Measure.le_map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(s : Set β)
:
μ (f ⁻¹' s) ≤ (MeasureTheory.Measure.map f μ) s
Even if s is not measurable, we can bound map f μ s from below.
See also MeasurableEquiv.map_apply.
theorem
MeasureTheory.Measure.le_map_apply_image
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
(s : Set α)
:
μ s ≤ (MeasureTheory.Measure.map f μ) (f '' s)
theorem
MeasureTheory.Measure.preimage_null_of_map_null
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : (MeasureTheory.Measure.map f μ) s = 0)
:
Even if s is not measurable, map f μ s = 0 implies that μ (f ⁻¹' s) = 0.
theorem
MeasureTheory.Measure.tendsto_ae_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
:
noncomputable def
MeasureTheory.Measure.sum
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(f : ι → MeasureTheory.Measure α)
:
Sum of an indexed family of measures.
Equations
- MeasureTheory.Measure.sum f = (MeasureTheory.OuterMeasure.sum fun (i : ι) => (f i).toOuterMeasure).toMeasure ⋯
Instances For
theorem
MeasureTheory.Measure.le_sum_apply
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(f : ι → MeasureTheory.Measure α)
(s : Set α)
:
∑' (i : ι), (f i) s ≤ (MeasureTheory.Measure.sum f) s
@[simp]
theorem
MeasureTheory.Measure.sum_apply
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(f : ι → MeasureTheory.Measure α)
{s : Set α}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
theorem
MeasureTheory.Measure.sum_apply₀
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(f : ι → MeasureTheory.Measure α)
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.sum f))
:
(MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
For the next theorem, the countability assumption is necessary. For a counterexample, consider
an uncountable space, with a distinguished point x₀, and the sigma-algebra made of countable sets
not containing x₀, and their complements. All points but x₀ are measurable.
Consider the sum of the Dirac masses at points different from x₀, and s = {x₀}. For any Dirac
mass δ_x, we have δ_x (x₀) = 0, so ∑' x, δ_x (x₀) = 0. On the other hand, the measure
sum δ_x gives mass one to each point different from x₀, so it gives infinite mass to any
measurable set containing x₀ (as such a set is uncountable), and by outer regularity one gets
sum δ_x {x₀} = ∞.
theorem
MeasureTheory.Measure.sum_apply_of_countable
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[Countable ι]
(f : ι → MeasureTheory.Measure α)
(s : Set α)
:
(MeasureTheory.Measure.sum f) s = ∑' (i : ι), (f i) s
theorem
MeasureTheory.Measure.le_sum
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(μ : ι → MeasureTheory.Measure α)
(i : ι)
:
μ i ≤ MeasureTheory.Measure.sum μ
@[simp]
theorem
MeasureTheory.Measure.sum_apply_eq_zero
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[Countable ι]
{μ : ι → MeasureTheory.Measure α}
{s : Set α}
:
(MeasureTheory.Measure.sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
theorem
MeasureTheory.Measure.sum_apply_eq_zero'
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{μ : ι → MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0
@[simp]
theorem
MeasureTheory.Measure.sum_eq_zero
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{f : ι → MeasureTheory.Measure α}
:
MeasureTheory.Measure.sum f = 0 ↔ ∀ (i : ι), f i = 0
@[simp]
theorem
MeasureTheory.Measure.sum_zero
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
:
(MeasureTheory.Measure.sum fun (x : ι) => 0) = 0
theorem
MeasureTheory.Measure.sum_sum
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{ι' : Type u_8}
(μ : ι → ι' → MeasureTheory.Measure α)
:
(MeasureTheory.Measure.sum fun (n : ι) => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun (p : ι × ι') => μ p.1 p.2
theorem
MeasureTheory.Measure.sum_comm
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{ι' : Type u_8}
(μ : ι → ι' → MeasureTheory.Measure α)
:
(MeasureTheory.Measure.sum fun (n : ι) => MeasureTheory.Measure.sum (μ n)) = MeasureTheory.Measure.sum fun (m : ι') => MeasureTheory.Measure.sum fun (n : ι) => μ n m
theorem
MeasureTheory.Measure.ae_sum_iff
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[Countable ι]
{μ : ι → MeasureTheory.Measure α}
{p : α → Prop}
:
(∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
theorem
MeasureTheory.Measure.ae_sum_iff'
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{μ : ι → MeasureTheory.Measure α}
{p : α → Prop}
(h : MeasurableSet {x : α | p x})
:
(∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
@[simp]
theorem
MeasureTheory.Measure.sum_fintype
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[Fintype ι]
(μ : ι → MeasureTheory.Measure α)
:
MeasureTheory.Measure.sum μ = ∑ i : ι, μ i
theorem
MeasureTheory.Measure.sum_coe_finset
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(s : Finset ι)
(μ : ι → MeasureTheory.Measure α)
:
(MeasureTheory.Measure.sum fun (i : { x : ι // x ∈ s }) => μ ↑i) = ∑ i ∈ s, μ i
@[simp]
theorem
MeasureTheory.Measure.ae_sum_eq
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[Countable ι]
(μ : ι → MeasureTheory.Measure α)
:
MeasureTheory.ae (MeasureTheory.Measure.sum μ) = ⨆ (i : ι), MeasureTheory.ae (μ i)
theorem
MeasureTheory.Measure.sum_bool
{α : Type u_1}
{m0 : MeasurableSpace α}
(f : Bool → MeasureTheory.Measure α)
:
MeasureTheory.Measure.sum f = f true + f false
theorem
MeasureTheory.Measure.sum_cond
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ ν : MeasureTheory.Measure α)
:
(MeasureTheory.Measure.sum fun (b : Bool) => bif b then μ else ν) = μ + ν
@[simp]
theorem
MeasureTheory.Measure.sum_of_isEmpty
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[IsEmpty ι]
(μ : ι → MeasureTheory.Measure α)
:
@[deprecated MeasureTheory.Measure.sum_of_isEmpty]
theorem
MeasureTheory.Measure.sum_of_empty
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
[IsEmpty ι]
(μ : ι → MeasureTheory.Measure α)
:
Alias of MeasureTheory.Measure.sum_of_isEmpty.
theorem
MeasureTheory.Measure.sum_add_sum_compl
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
(s : Set ι)
(μ : ι → MeasureTheory.Measure α)
:
((MeasureTheory.Measure.sum fun (i : ↑s) => μ ↑i) + MeasureTheory.Measure.sum fun (i : ↑sᶜ) => μ ↑i) = MeasureTheory.Measure.sum μ
theorem
MeasureTheory.Measure.sum_congr
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : ℕ → MeasureTheory.Measure α}
(h : ∀ (n : ℕ), μ n = ν n)
:
theorem
MeasureTheory.Measure.sum_add_sum
{α : Type u_1}
{m0 : MeasurableSpace α}
{ι : Type u_8}
(μ ν : ι → MeasureTheory.Measure α)
:
MeasureTheory.Measure.sum μ + MeasureTheory.Measure.sum ν = MeasureTheory.Measure.sum fun (n : ι) => μ n + ν n
@[simp]
theorem
MeasureTheory.Measure.sum_comp_equiv
{α : Type u_1}
{m0 : MeasurableSpace α}
{ι : Type u_8}
{ι' : Type u_9}
(e : ι' ≃ ι)
(m : ι → MeasureTheory.Measure α)
:
@[simp]
theorem
MeasureTheory.Measure.sum_extend_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{ι : Type u_8}
{ι' : Type u_9}
{f : ι → ι'}
(hf : Function.Injective f)
(m : ι → MeasureTheory.Measure α)
:
Absolute continuity #
def
MeasureTheory.Measure.AbsolutelyContinuous
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ ν : MeasureTheory.Measure α)
:
We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν,
if ν(A) = 0 implies that μ(A) = 0.
Instances For
We say that μ is absolutely continuous with respect to ν, or that μ is dominated by ν,
if ν(A) = 0 implies that μ(A) = 0.
Equations
- MeasureTheory.«term_≪_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_≪_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪ ") (Lean.ParserDescr.cat `term 51))
Instances For
theorem
MeasureTheory.Measure.absolutelyContinuous_of_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ ≤ ν)
:
μ.AbsolutelyContinuous ν
theorem
LE.le.absolutelyContinuous
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ ≤ ν)
:
μ.AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.absolutelyContinuous_of_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ = ν)
:
μ.AbsolutelyContinuous ν
theorem
Eq.absolutelyContinuous
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ = ν)
:
μ.AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.mk
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0)
:
μ.AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.refl
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
μ.AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.AbsolutelyContinuous.rfl
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
μ.AbsolutelyContinuous μ
instance
MeasureTheory.Measure.AbsolutelyContinuous.instIsRefl
{α : Type u_1}
{x✝ : MeasurableSpace α}
:
IsRefl (MeasureTheory.Measure α) fun (x1 x2 : MeasureTheory.Measure α) => x1.AbsolutelyContinuous x2
@[simp]
theorem
MeasureTheory.Measure.AbsolutelyContinuous.zero
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.trans
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ μ₃ : MeasureTheory.Measure α}
(h1 : μ₁.AbsolutelyContinuous μ₂)
(h2 : μ₂.AbsolutelyContinuous μ₃)
:
μ₁.AbsolutelyContinuous μ₃
theorem
MeasureTheory.Measure.AbsolutelyContinuous.map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ ν : MeasureTheory.Measure α}
(h : μ.AbsolutelyContinuous ν)
{f : α → β}
(hf : Measurable f)
:
(MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
theorem
MeasureTheory.Measure.AbsolutelyContinuous.smul_left
{α : Type u_1}
{R : Type u_6}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : μ.AbsolutelyContinuous ν)
(c : R)
:
(c • μ).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.smul
{α : Type u_1}
{R : Type u_6}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : μ.AbsolutelyContinuous ν)
(c : R)
:
If μ ≪ ν, then c • μ ≪ c • ν.
Earlier, this name was used for what's now called AbsolutelyContinuous.smul_left.
@[deprecated MeasureTheory.Measure.AbsolutelyContinuous.smul]
theorem
MeasureTheory.Measure.AbsolutelyContinuous.smul_both
{α : Type u_1}
{R : Type u_6}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : μ.AbsolutelyContinuous ν)
(c : R)
:
Alias of MeasureTheory.Measure.AbsolutelyContinuous.smul.
If μ ≪ ν, then c • μ ≪ c • ν.
Earlier, this name was used for what's now called AbsolutelyContinuous.smul_left.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ ν ν' : MeasureTheory.Measure α}
(h1 : μ₁.AbsolutelyContinuous ν)
(h2 : μ₂.AbsolutelyContinuous ν')
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ ν : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add_left
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ₁ μ₂ ν : MeasureTheory.Measure α}
(h₁ : μ₁.AbsolutelyContinuous ν)
(h₂ : μ₂.AbsolutelyContinuous ν)
:
(μ₁ + μ₂).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.add_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h1 : μ.AbsolutelyContinuous ν)
(ν' : MeasureTheory.Measure α)
:
μ.AbsolutelyContinuous (ν + ν')
@[simp]
theorem
MeasureTheory.Measure.absolutelyContinuous_zero_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
theorem
MeasureTheory.Measure.absolutelyContinuous_refl
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
μ.AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.absolutelyContinuous_rfl
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
μ.AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.absolutelyContinuous_sum_left
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
{μs : ι → MeasureTheory.Measure α}
(hμs : ∀ (i : ι), (μs i).AbsolutelyContinuous ν)
:
(MeasureTheory.Measure.sum μs).AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.absolutelyContinuous_sum_right
{α : Type u_1}
{ι : Type u_5}
{m0 : MeasurableSpace α}
{ν : MeasureTheory.Measure α}
{μs : ι → MeasureTheory.Measure α}
(i : ι)
(hνμ : ν.AbsolutelyContinuous (μs i))
:
ν.AbsolutelyContinuous (MeasureTheory.Measure.sum μs)
theorem
MeasureTheory.Measure.smul_absolutelyContinuous
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{c : ENNReal}
:
(c • μ).AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.absolutelyContinuous_of_le_smul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ μ' : MeasureTheory.Measure α}
{c : ENNReal}
(hμ'_le : μ' ≤ c • μ)
:
μ'.AbsolutelyContinuous μ
theorem
MeasureTheory.Measure.absolutelyContinuous_smul
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{c : ENNReal}
(hc : c ≠ 0)
:
μ.AbsolutelyContinuous (c • μ)
theorem
MeasureTheory.Measure.ae_le_iff_absolutelyContinuous
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
MeasureTheory.ae μ ≤ MeasureTheory.ae ν ↔ μ.AbsolutelyContinuous ν
theorem
MeasureTheory.Measure.AbsolutelyContinuous.ae_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
μ.AbsolutelyContinuous ν → MeasureTheory.ae μ ≤ MeasureTheory.ae ν
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
theorem
LE.le.absolutelyContinuous_of_ae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
MeasureTheory.ae μ ≤ MeasureTheory.ae ν → μ.AbsolutelyContinuous ν
Alias of the forward direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
theorem
MeasureTheory.Measure.ae_mono'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
:
μ.AbsolutelyContinuous ν → MeasureTheory.ae μ ≤ MeasureTheory.ae ν
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
Alias of the reverse direction of MeasureTheory.Measure.ae_le_iff_absolutelyContinuous.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.ae_eq
{α : Type u_1}
{δ : Type u_4}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ.AbsolutelyContinuous ν)
{f g : α → δ}
(h' : f =ᵐ[ν] g)
:
theorem
MeasureTheory.AEDisjoint.of_absolutelyContinuous
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h : MeasureTheory.AEDisjoint μ s t)
{ν : MeasureTheory.Measure α}
(h' : ν.AbsolutelyContinuous μ)
:
MeasureTheory.AEDisjoint ν s t
theorem
MeasureTheory.AEDisjoint.of_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s t : Set α}
(h : MeasureTheory.AEDisjoint μ s t)
{ν : MeasureTheory.Measure α}
(h' : ν ≤ μ)
:
MeasureTheory.AEDisjoint ν s t
Quasi measure preserving maps (a.k.a. non-singular maps) #
structure
MeasureTheory.Measure.QuasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m0 : MeasurableSpace α}
(f : α → β)
(μa : MeasureTheory.Measure α := by volume_tac)
(μb : MeasureTheory.Measure β := by volume_tac)
:
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.
- measurable : Measurable f
- absolutelyContinuous : (MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb
Instances For
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.id
{α : Type u_1}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
theorem
Measurable.quasiMeasurePreserving
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{f : α → β}
{_m0 : MeasurableSpace α}
(hf : Measurable f)
(μ : MeasureTheory.Measure α)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono_left
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa μa' : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(ha : μa'.AbsolutelyContinuous μa)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono_right
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb μb' : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(ha : μb.AbsolutelyContinuous μb')
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.mono
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa μa' : MeasureTheory.Measure α}
{μb μb' : MeasureTheory.Measure β}
{f : α → β}
(ha : μa'.AbsolutelyContinuous μa)
(hb : μb.AbsolutelyContinuous μb')
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
[MeasurableSpace γ]
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{μc : MeasureTheory.Measure γ}
{g : β → γ}
{f : α → β}
(hg : MeasureTheory.Measure.QuasiMeasurePreserving g μb μc)
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
MeasureTheory.Measure.QuasiMeasurePreserving (g ∘ f) μa μc
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.iterate
{α : Type u_1}
{m0 : MeasurableSpace α}
{μa : MeasureTheory.Measure α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μa)
(n : ℕ)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.aemeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
AEMeasurable f μa
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{R : Type u_8}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(c : R)
:
MeasureTheory.Measure.QuasiMeasurePreserving f (c • μa) (c • μb)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
Filter.Tendsto f (MeasureTheory.ae μa) (MeasureTheory.ae μb)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
{p : β → Prop}
(hg : ∀ᵐ (x : β) ∂μb, p x)
:
∀ᵐ (x : α) ∂μa, p (f x)
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq
{α : Type u_1}
{β : Type u_2}
{δ : Type u_4}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
{g₁ g₂ : β → δ}
(hg : g₁ =ᵐ[μb] g₂)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
{s : Set β}
(hs : μb s = 0)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{s t : Set β}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(h : s ≤ᵐ[μb] t)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{s t : Set β}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
(h : s =ᵐ[μb] t)
:
theorem
MeasureTheory.NullMeasurableSet.preimage
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μa : MeasureTheory.Measure α}
{μb : MeasureTheory.Measure β}
{f : α → β}
{s : Set β}
(hs : MeasureTheory.NullMeasurableSet s μb)
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μa μb)
:
MeasureTheory.NullMeasurableSet (f ⁻¹' s) μa
The preimage of a null measurable set under a (quasi) measure preserving map is a null measurable set.
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(k : ℕ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{e : α ≃ α}
(he : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e) μ μ)
(he' : MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) μ μ)
(k : ℤ)
(hs : ⇑e '' s =ᵐ[μ] s)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
Filter.limsup (fun (n : ℕ) => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
Filter.liminf (fun (n : ℕ) => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → α}
(h : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : f ⁻¹' s =ᵐ[μ] s)
:
For a quasi measure preserving self-map f, if a null measurable set s is a.e. invariant,
then it is a.e. equal to a measurable invariant set.
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq
{G : Type u_8}
{α : Type u_9}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(g : G)
(h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g⁻¹ • x) μ μ)
(h_ae_eq : s =ᵐ[μ] t)
:
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.vadd_ae_eq_of_ae_eq
{G : Type u_8}
{α : Type u_9}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{s t : Set α}
{μ : MeasureTheory.Measure α}
(g : G)
(h_qmp : MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => -g +ᵥ x) μ μ)
(h_ae_eq : s =ᵐ[μ] t)
:
theorem
MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one
{G : Type u_8}
{α : Type u_9}
[Group G]
[MulAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h_ae_disjoint : ∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s)
(h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g • x) μ μ)
:
Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g • s)
theorem
MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_zero
{G : Type u_8}
{α : Type u_9}
[AddGroup G]
[AddAction G α]
{x✝ : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h_ae_disjoint : ∀ (g : G), g ≠ 0 → MeasureTheory.AEDisjoint μ (g +ᵥ s) s)
(h_qmp : ∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun (x : α) => g +ᵥ x) μ μ)
:
Pairwise (MeasureTheory.AEDisjoint μ on fun (g : G) => g +ᵥ s)
def
MeasureTheory.Measure.cofinite
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
:
Filter α
The filter of sets s such that sᶜ has finite measure.
Equations
- μ.cofinite = Filter.comk (fun (x : Set α) => μ x < ⊤) ⋯ ⋯ ⋯
Instances For
theorem
MeasureTheory.Measure.mem_cofinite
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
theorem
MeasureTheory.Measure.compl_mem_cofinite
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
theorem
MeasureTheory.Measure.eventually_cofinite
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
:
instance
MeasureTheory.Measure.cofinite.instIsMeasurablyGenerated
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
μ.cofinite.IsMeasurablyGenerated
theorem
AEMeasurable.nullMeasurable
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(h : AEMeasurable f μ)
:
theorem
AEMeasurable.nullMeasurableSet_preimage
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
{s : Set β}
(hf : AEMeasurable f μ)
(hs : MeasurableSet s)
:
MeasureTheory.NullMeasurableSet (f ⁻¹' s) μ
theorem
MeasureTheory.NullMeasurableSet.mono_ac
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.NullMeasurableSet s μ)
(hle : ν.AbsolutelyContinuous μ)
:
theorem
MeasureTheory.NullMeasurableSet.mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
{s : Set α}
(h : MeasureTheory.NullMeasurableSet s μ)
(hle : ν ≤ μ)
:
theorem
MeasureTheory.AEDisjoint.preimage
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → β}
{s t : Set β}
(ht : MeasureTheory.AEDisjoint ν s t)
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν)
:
MeasureTheory.AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)
@[simp]
theorem
MeasureTheory.ae_eq_bot
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
MeasureTheory.ae μ = ⊥ ↔ μ = 0
@[simp]
theorem
MeasureTheory.ae_neBot
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
(MeasureTheory.ae μ).NeBot ↔ μ ≠ 0
instance
MeasureTheory.Measure.ae.neBot
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NeZero μ]
:
(MeasureTheory.ae μ).NeBot
@[simp]
theorem
MeasureTheory.ae_mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
(h : μ ≤ ν)
:
theorem
MeasureTheory.mem_ae_map_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : MeasurableSet s)
:
s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ) ↔ f ⁻¹' s ∈ MeasureTheory.ae μ
theorem
MeasureTheory.mem_ae_of_mem_ae_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{s : Set β}
(hs : s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ))
:
f ⁻¹' s ∈ MeasureTheory.ae μ
theorem
MeasureTheory.ae_map_iff
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{p : β → Prop}
(hp : MeasurableSet {x : β | p x})
:
(∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
theorem
MeasureTheory.ae_of_ae_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{mβ : MeasurableSpace β}
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : AEMeasurable f μ)
{p : β → Prop}
(h : ∀ᵐ (y : β) ∂MeasureTheory.Measure.map f μ, p y)
:
∀ᵐ (x : α) ∂μ, p (f x)
theorem
MeasureTheory.ae_map_mem_range
{α : Type u_1}
{β : Type u_2}
{mβ : MeasurableSpace β}
{m0 : MeasurableSpace α}
(f : α → β)
(hf : MeasurableSet (Set.range f))
(μ : MeasureTheory.Measure α)
:
∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, x ∈ Set.range f
theorem
MeasureTheory.biSup_measure_Iic
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Preorder α]
{s : Set α}
(hsc : s.Countable)
(hst : ∀ (x : α), ∃ y ∈ s, x ≤ y)
(hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
MeasureTheory.tendsto_measure_Ico_atTop
{α : Type u_1}
{m0 : MeasurableSpace α}
[Preorder α]
[NoMaxOrder α]
[Filter.atTop.IsCountablyGenerated]
(μ : MeasureTheory.Measure α)
(a : α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Ico a x)) Filter.atTop (nhds (μ (Set.Ici a)))
theorem
MeasureTheory.tendsto_measure_Ioc_atBot
{α : Type u_1}
{m0 : MeasurableSpace α}
[Preorder α]
[NoMinOrder α]
[Filter.atBot.IsCountablyGenerated]
(μ : MeasureTheory.Measure α)
(a : α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Ioc x a)) Filter.atBot (nhds (μ (Set.Iic a)))
theorem
MeasureTheory.tendsto_measure_Iic_atTop
{α : Type u_1}
{m0 : MeasurableSpace α}
[Preorder α]
[Filter.atTop.IsCountablyGenerated]
(μ : MeasureTheory.Measure α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Iic x)) Filter.atTop (nhds (μ Set.univ))
theorem
MeasureTheory.tendsto_measure_Ici_atBot
{α : Type u_1}
{m0 : MeasurableSpace α}
[Preorder α]
[Filter.atBot.IsCountablyGenerated]
(μ : MeasureTheory.Measure α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Ici x)) Filter.atBot (nhds (μ Set.univ))
theorem
MeasureTheory.Iio_ae_eq_Iic'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioi_ae_eq_Ici'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioo_ae_eq_Ioc'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a b : α}
(hb : μ {b} = 0)
:
theorem
MeasureTheory.Ioc_ae_eq_Icc'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a b : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioo_ae_eq_Ico'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a b : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioo_ae_eq_Icc'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a b : α}
(ha : μ {a} = 0)
(hb : μ {b} = 0)
:
theorem
MeasureTheory.Ico_ae_eq_Icc'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a b : α}
(hb : μ {b} = 0)
:
theorem
MeasureTheory.Ico_ae_eq_Ioc'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[PartialOrder α]
{a b : α}
(ha : μ {a} = 0)
(hb : μ {b} = 0)
:
theorem
MeasurableEmbedding.map_apply
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure α)
(s : Set β)
:
(MeasureTheory.Measure.map f μ) s = μ (f ⁻¹' s)
theorem
MeasurableEmbedding.absolutelyContinuous_map
{α : Type u_1}
{β : Type u_2}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
{μ ν : MeasureTheory.Measure α}
(hf : MeasurableEmbedding f)
(hμν : μ.AbsolutelyContinuous ν)
:
(MeasureTheory.Measure.map f μ).AbsolutelyContinuous (MeasureTheory.Measure.map f ν)
Interactions of measurable equivalences and measures
theorem
MeasurableEquiv.map_apply
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
(f : α ≃ᵐ β)
(s : Set β)
:
(MeasureTheory.Measure.map (⇑f) μ) s = μ (⇑f ⁻¹' s)
If we map a measure along a measurable equivalence, we can compute the measure on all sets (not just the measurable ones).
@[simp]
theorem
MeasurableEquiv.map_symm_map
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ
@[simp]
theorem
MeasurableEquiv.map_map_symm
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{ν : MeasureTheory.Measure β}
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.map (⇑e.symm) ν) = ν
theorem
MeasurableEquiv.map_measurableEquiv_injective
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(e : α ≃ᵐ β)
:
theorem
MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.map (⇑e) μ = ν ↔ MeasureTheory.Measure.map (⇑e.symm) ν = μ
theorem
MeasurableEquiv.map_ae
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(f : α ≃ᵐ β)
(μ : MeasureTheory.Measure α)
:
Filter.map (⇑f) (MeasureTheory.ae μ) = MeasureTheory.ae (MeasureTheory.Measure.map (⇑f) μ)
theorem
MeasurableEquiv.quasiMeasurePreserving_symm
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
(e : α ≃ᵐ β)
:
MeasureTheory.Measure.QuasiMeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ