Restricting a measure to a subset or a subtype #
Given a measure μ on a type α and a subset s of α, we define a measure μ.restrict s as
the restriction of μ to s (still as a measure on α).
We investigate how this notion interacts with usual operations on measures (sum, pushforward, pullback), and on sets (inclusion, union, Union).
We also study the relationship between the restriction of a measure to a subtype (given by the
pullback under Subtype.val) and the restriction to a set as above.
Restricting a measure #
noncomputable def
MeasureTheory.Measure.restrictₗ
{α : Type u_2}
{m0 : MeasurableSpace α}
(s : Set α)
:
Restrict a measure μ to a set s as an ℝ≥0∞-linear map.
Equations
Instances For
noncomputable def
MeasureTheory.Measure.restrict
{α : Type u_2}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(s : Set α)
:
Restrict a measure μ to a set s.
Equations
- μ.restrict s = (MeasureTheory.Measure.restrictₗ s) μ
Instances For
@[simp]
theorem
MeasureTheory.Measure.restrictₗ_apply
{α : Type u_2}
{_m0 : MeasurableSpace α}
(s : Set α)
(μ : MeasureTheory.Measure α)
:
(MeasureTheory.Measure.restrictₗ s) μ = μ.restrict s
theorem
MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : MeasurableSet s)
:
↑(μ.restrict s) = (MeasureTheory.OuterMeasure.restrict s) ↑μ
This lemma shows that restrict and toOuterMeasure commute. Note that the LHS has a
restrict on measures and the RHS has a restrict on outer measures.
theorem
MeasureTheory.Measure.restrict_apply₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(ht : MeasureTheory.NullMeasurableSet t (μ.restrict s))
:
@[simp]
theorem
MeasureTheory.Measure.restrict_apply
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(ht : MeasurableSet 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
MeasureTheory.Measure.restrict_mono'
{α : Type u_2}
{_m0 : MeasurableSpace α}
⦃s : Set α⦄
⦃s' : Set α⦄
⦃μ : MeasureTheory.Measure α⦄
⦃ν : MeasureTheory.Measure α⦄
(hs : s ≤ᶠ[MeasureTheory.Measure.ae μ] s')
(hμν : μ ≤ ν)
:
μ.restrict s ≤ ν.restrict s'
Restriction of a measure to a subset is monotone both in set and in measure.
theorem
MeasureTheory.Measure.restrict_mono
{α : Type u_2}
{_m0 : MeasurableSpace α}
⦃s : Set α⦄
⦃s' : Set α⦄
(hs : s ⊆ s')
⦃μ : MeasureTheory.Measure α⦄
⦃ν : MeasureTheory.Measure α⦄
(hμν : μ ≤ ν)
:
μ.restrict s ≤ ν.restrict s'
Restriction of a measure to a subset is monotone both in set and in measure.
theorem
MeasureTheory.Measure.restrict_mono_ae
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : s ≤ᶠ[MeasureTheory.Measure.ae μ] t)
:
μ.restrict s ≤ μ.restrict t
theorem
MeasureTheory.Measure.restrict_congr_set
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : s =ᶠ[MeasureTheory.Measure.ae μ] t)
:
μ.restrict s = μ.restrict t
@[simp]
theorem
MeasureTheory.Measure.restrict_apply'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : MeasurableSet 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
MeasureTheory.Measure.restrict_apply₀'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
theorem
MeasureTheory.Measure.restrict_le_self
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
μ.restrict s ≤ μ
theorem
MeasureTheory.Measure.restrict_eq_self
{α : Type u_2}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{s : Set α}
{t : Set α}
(h : s ⊆ t)
:
↑↑(μ.restrict t) s = ↑↑μ s
@[simp]
theorem
MeasureTheory.Measure.restrict_apply_self
{α : Type u_2}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(s : Set α)
:
↑↑(μ.restrict s) s = ↑↑μ s
theorem
MeasureTheory.Measure.restrict_apply_univ
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Set α)
:
↑↑(μ.restrict s) Set.univ = ↑↑μ s
theorem
MeasureTheory.Measure.le_restrict_apply
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Set α)
(t : Set α)
:
theorem
MeasureTheory.Measure.restrict_apply_le
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Set α)
(t : Set α)
:
↑↑(μ.restrict s) t ≤ ↑↑μ t
theorem
MeasureTheory.Measure.restrict_apply_superset
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : s ⊆ t)
:
↑↑(μ.restrict s) t = ↑↑μ s
@[simp]
theorem
MeasureTheory.Measure.restrict_add
{α : Type u_2}
{_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure α)
(s : Set α)
:
@[simp]
theorem
MeasureTheory.Measure.restrict_zero
{α : Type u_2}
{_m0 : MeasurableSpace α}
(s : Set α)
:
0.restrict s = 0
@[simp]
theorem
MeasureTheory.Measure.restrict_smul
{α : Type u_2}
{_m0 : MeasurableSpace α}
(c : ENNReal)
(μ : MeasureTheory.Measure α)
(s : Set α)
:
theorem
MeasureTheory.Measure.restrict_restrict₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : MeasureTheory.NullMeasurableSet s (μ.restrict t))
:
@[simp]
theorem
MeasureTheory.Measure.restrict_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.restrict_restrict_of_subset
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : s ⊆ t)
:
(μ.restrict t).restrict s = μ.restrict s
theorem
MeasureTheory.Measure.restrict_restrict₀'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(ht : MeasureTheory.NullMeasurableSet t μ)
:
theorem
MeasureTheory.Measure.restrict_restrict'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.restrict_comm
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : MeasurableSet s)
:
(μ.restrict t).restrict s = (μ.restrict s).restrict t
theorem
MeasureTheory.Measure.restrict_apply_eq_zero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.measure_inter_eq_zero_of_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : ↑↑(μ.restrict s) t = 0)
:
theorem
MeasureTheory.Measure.restrict_apply_eq_zero'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.restrict_eq_zero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
instance
MeasureTheory.Measure.restrict.neZero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
[NeZero (↑↑μ s)]
:
NeZero (μ.restrict s)
If μ s ≠ 0, then μ.restrict s ≠ 0, in terms of NeZero instances.
Equations
- ⋯ = ⋯
theorem
MeasureTheory.Measure.restrict_zero_set
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : ↑↑μ s = 0)
:
μ.restrict s = 0
@[simp]
theorem
MeasureTheory.Measure.restrict_empty
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
@[simp]
theorem
MeasureTheory.Measure.restrict_univ
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
:
μ.restrict Set.univ = μ
theorem
MeasureTheory.Measure.restrict_inter_add_diff₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasureTheory.NullMeasurableSet t μ)
:
theorem
MeasureTheory.Measure.restrict_inter_add_diff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.restrict_union_add_inter₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasureTheory.NullMeasurableSet t μ)
:
theorem
MeasureTheory.Measure.restrict_union_add_inter
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{t : Set α}
(s : Set α)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.restrict_union_add_inter'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(t : Set α)
:
theorem
MeasureTheory.Measure.restrict_union₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : MeasureTheory.AEDisjoint μ s t)
(ht : MeasureTheory.NullMeasurableSet t μ)
:
theorem
MeasureTheory.Measure.restrict_union
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : Disjoint s t)
(ht : MeasurableSet t)
:
theorem
MeasureTheory.Measure.restrict_union'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(h : Disjoint s t)
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.restrict_add_restrict_compl
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
@[simp]
theorem
MeasureTheory.Measure.restrict_compl_add_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
theorem
MeasureTheory.Measure.restrict_union_le
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Set α)
(s' : Set α)
:
theorem
MeasureTheory.Measure.restrict_iUnion_apply_ae
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Pairwise (MeasureTheory.AEDisjoint μ on s))
(hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
{t : Set α}
(ht : MeasurableSet t)
:
↑↑(μ.restrict (⋃ (i : ι), s i)) t = ∑' (i : ι), ↑↑(μ.restrict (s i)) t
theorem
MeasureTheory.Measure.restrict_iUnion_apply
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Pairwise (Disjoint on s))
(hm : ∀ (i : ι), MeasurableSet (s i))
{t : Set α}
(ht : MeasurableSet t)
:
↑↑(μ.restrict (⋃ (i : ι), s i)) t = ∑' (i : ι), ↑↑(μ.restrict (s i)) t
theorem
MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Directed (fun (x x_1 : Set α) => x ⊆ x_1) s)
{t : Set α}
(ht : MeasurableSet t)
:
↑↑(μ.restrict (⋃ (i : ι), s i)) t = ⨆ (i : ι), ↑↑(μ.restrict (s i)) t
theorem
MeasureTheory.Measure.restrict_map
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
(hf : Measurable f)
{s : Set β}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
The restriction of the pushforward measure is the pushforward of the restriction. For a version
assuming only AEMeasurable, see restrict_map_of_aemeasurable.
theorem
MeasureTheory.Measure.restrict_toMeasurable
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(h : ↑↑μ s ≠ ⊤)
:
μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
theorem
MeasureTheory.Measure.restrict_eq_self_of_ae_mem
{α : Type u_2}
{_m0 : MeasurableSpace α}
⦃s : Set α⦄
⦃μ : MeasureTheory.Measure α⦄
(hs : ∀ᵐ (x : α) ∂μ, x ∈ s)
:
μ.restrict s = μ
theorem
MeasureTheory.Measure.restrict_congr_meas
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, MeasurableSet t → ↑↑μ t = ↑↑ν t
theorem
MeasureTheory.Measure.restrict_congr_mono
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
(hs : s ⊆ t)
(h : μ.restrict t = ν.restrict t)
:
μ.restrict s = ν.restrict s
theorem
MeasureTheory.Measure.restrict_union_congr
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{s : Set α}
{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
MeasureTheory.Measure.restrict_finset_biUnion_congr
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{s : Finset ι}
{t : ι → Set α}
:
theorem
MeasureTheory.Measure.restrict_iUnion_congr
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
:
theorem
MeasureTheory.Measure.restrict_biUnion_congr
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{s : Set ι}
{t : ι → Set α}
(hc : Set.Countable s)
:
theorem
MeasureTheory.Measure.restrict_sUnion_congr
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set (Set α)}
(hc : Set.Countable S)
:
theorem
MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict
{α : Type u_2}
{t : Set α}
{m0 : MeasurableSpace α}
{m : Set (MeasureTheory.Measure α)}
(hm : Set.Nonempty m)
(ht : MeasurableSet t)
:
(sInf m).restrict t = sInf ((fun (μ : MeasureTheory.Measure α) => μ.restrict t) '' m)
This lemma shows that Inf and restrict commute for measures.
theorem
MeasureTheory.Measure.exists_mem_of_measure_ne_zero_of_ae
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : ↑↑μ s ≠ 0)
{p : α → Prop}
(hp : ∀ᵐ (x : α) ∂μ.restrict s, p x)
:
∃ x ∈ s, p x
Extensionality results #
theorem
MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.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
MeasureTheory.Measure.ext_of_iUnion_eq_univ
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hs : ⋃ (i : ι), s i = Set.univ)
:
Alias of the reverse direction of MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ.
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using Union).
theorem
MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set ι}
{s : ι → Set α}
(hc : Set.Countable S)
(hs : ⋃ i ∈ S, s i = Set.univ)
:
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using biUnion).
theorem
MeasureTheory.Measure.ext_of_biUnion_eq_univ
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set ι}
{s : ι → Set α}
(hc : Set.Countable S)
(hs : ⋃ i ∈ S, s i = Set.univ)
:
Alias of the reverse direction of MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ.
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using biUnion).
theorem
MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set (Set α)}
(hc : Set.Countable S)
(hs : ⋃₀ S = Set.univ)
:
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using sUnion).
theorem
MeasureTheory.Measure.ext_of_sUnion_eq_univ
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set (Set α)}
(hc : Set.Countable S)
(hs : ⋃₀ S = Set.univ)
:
Alias of the reverse direction of MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ.
Two measures are equal if they have equal restrictions on a spanning collection of sets
(formulated using sUnion).
theorem
MeasureTheory.Measure.ext_of_generateFrom_of_cover
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set (Set α)}
{T : Set (Set α)}
(h_gen : m0 = MeasurableSpace.generateFrom S)
(hc : Set.Countable T)
(h_inter : IsPiSystem S)
(hU : ⋃₀ T = Set.univ)
(htop : ∀ t ∈ T, ↑↑μ t ≠ ⊤)
(ST_eq : ∀ t ∈ T, ∀ s ∈ S, ↑↑μ (s ∩ t) = ↑↑ν (s ∩ t))
(T_eq : ∀ t ∈ T, ↑↑μ t = ↑↑ν t)
:
μ = ν
theorem
MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
{S : Set (Set α)}
{T : Set (Set α)}
(h_gen : m0 = MeasurableSpace.generateFrom S)
(h_inter : IsPiSystem S)
(h_sub : T ⊆ S)
(hc : Set.Countable T)
(hU : ⋃₀ T = Set.univ)
(htop : ∀ s ∈ T, ↑↑μ s ≠ ⊤)
(h_eq : ∀ s ∈ S, ↑↑μ s = ↑↑ν s)
:
μ = ν
Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using sUnion.
theorem
MeasureTheory.Measure.ext_of_generateFrom_of_iUnion
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(C : Set (Set α))
(B : ℕ → Set α)
(hA : m0 = MeasurableSpace.generateFrom C)
(hC : IsPiSystem C)
(h1B : ⋃ (i : ℕ), B i = Set.univ)
(h2B : ∀ (i : ℕ), B i ∈ C)
(hμB : ∀ (i : ℕ), ↑↑μ (B i) ≠ ⊤)
(h_eq : ∀ s ∈ C, ↑↑μ s = ↑↑ν s)
:
μ = ν
Two measures are equal if they are equal on the π-system generating the σ-algebra,
and they are both finite on an increasing spanning sequence of sets in the π-system.
This lemma is formulated using iUnion.
FiniteSpanningSetsIn.ext is a reformulation of this lemma.
@[simp]
theorem
MeasureTheory.Measure.restrict_sum
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
(μ : ι → MeasureTheory.Measure α)
{s : Set α}
(hs : MeasurableSet s)
:
(MeasureTheory.Measure.sum μ).restrict s = MeasureTheory.Measure.sum fun (i : ι) => (μ i).restrict s
@[simp]
theorem
MeasureTheory.Measure.restrict_sum_of_countable
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
[Countable ι]
(μ : ι → MeasureTheory.Measure α)
(s : Set α)
:
(MeasureTheory.Measure.sum μ).restrict s = MeasureTheory.Measure.sum fun (i : ι) => (μ i).restrict s
theorem
MeasureTheory.Measure.AbsolutelyContinuous.restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure α}
(h : MeasureTheory.Measure.AbsolutelyContinuous μ ν)
(s : Set α)
:
MeasureTheory.Measure.AbsolutelyContinuous (μ.restrict s) (ν.restrict s)
theorem
MeasureTheory.Measure.restrict_iUnion_ae
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Pairwise (MeasureTheory.AEDisjoint μ on s))
(hm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ)
:
μ.restrict (⋃ (i : ι), s i) = MeasureTheory.Measure.sum fun (i : ι) => μ.restrict (s i)
theorem
MeasureTheory.Measure.restrict_iUnion
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
(hd : Pairwise (Disjoint on s))
(hm : ∀ (i : ι), MeasurableSet (s i))
:
μ.restrict (⋃ (i : ι), s i) = MeasureTheory.Measure.sum fun (i : ι) => μ.restrict (s i)
theorem
MeasureTheory.Measure.restrict_iUnion_le
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
{s : ι → Set α}
:
μ.restrict (⋃ (i : ι), s i) ≤ MeasureTheory.Measure.sum fun (i : ι) => μ.restrict (s i)
@[simp]
theorem
MeasureTheory.ae_restrict_iUnion_eq
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
(s : ι → Set α)
:
MeasureTheory.Measure.ae (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), MeasureTheory.Measure.ae (μ.restrict (s i))
@[simp]
theorem
MeasureTheory.ae_restrict_union_eq
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Set α)
(t : Set α)
:
MeasureTheory.Measure.ae (μ.restrict (s ∪ t)) = MeasureTheory.Measure.ae (μ.restrict s) ⊔ MeasureTheory.Measure.ae (μ.restrict t)
theorem
MeasureTheory.ae_restrict_biUnion_eq
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : ι → Set α)
{t : Set ι}
(ht : Set.Countable t)
:
MeasureTheory.Measure.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.Measure.ae (μ.restrict (s i))
theorem
MeasureTheory.ae_restrict_biUnion_finset_eq
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : ι → Set α)
(t : Finset ι)
:
MeasureTheory.Measure.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.Measure.ae (μ.restrict (s i))
theorem
MeasureTheory.ae_restrict_iUnion_iff
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
(s : ι → Set α)
(p : α → Prop)
:
(∀ᵐ (x : α) ∂μ.restrict (⋃ (i : ι), s i), p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ.restrict (s i), p x
theorem
MeasureTheory.ae_restrict_union_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : Set α)
(t : Set α)
(p : α → Prop)
:
theorem
MeasureTheory.ae_restrict_biUnion_iff
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : ι → Set α)
{t : Set ι}
(ht : Set.Countable t)
(p : α → Prop)
:
(∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
@[simp]
theorem
MeasureTheory.ae_restrict_biUnion_finset_iff
{α : Type u_2}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : ι → Set α)
(t : Finset ι)
(p : α → Prop)
:
(∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
theorem
MeasureTheory.ae_eq_restrict_iUnion_iff
{α : Type u_2}
{δ : Type u_4}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[Countable ι]
(s : ι → Set α)
(f : α → δ)
(g : α → δ)
:
f =ᶠ[MeasureTheory.Measure.ae (μ.restrict (⋃ (i : ι), s i))] g ↔ ∀ (i : ι), f =ᶠ[MeasureTheory.Measure.ae (μ.restrict (s i))] g
theorem
MeasureTheory.ae_eq_restrict_biUnion_iff
{α : Type u_2}
{δ : Type u_4}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : ι → Set α)
{t : Set ι}
(ht : Set.Countable t)
(f : α → δ)
(g : α → δ)
:
f =ᶠ[MeasureTheory.Measure.ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[MeasureTheory.Measure.ae (μ.restrict (s i))] g
theorem
MeasureTheory.ae_eq_restrict_biUnion_finset_iff
{α : Type u_2}
{δ : Type u_4}
{ι : Type u_6}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(s : ι → Set α)
(t : Finset ι)
(f : α → δ)
(g : α → δ)
:
f =ᶠ[MeasureTheory.Measure.ae (μ.restrict (⋃ i ∈ t, s i))] g ↔ ∀ i ∈ t, f =ᶠ[MeasureTheory.Measure.ae (μ.restrict (s i))] g
theorem
MeasureTheory.ae_restrict_uIoc_eq
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[LinearOrder α]
(a : α)
(b : α)
:
MeasureTheory.Measure.ae (μ.restrict (Ι a b)) = MeasureTheory.Measure.ae (μ.restrict (Set.Ioc a b)) ⊔ MeasureTheory.Measure.ae (μ.restrict (Set.Ioc b a))
theorem
MeasureTheory.ae_restrict_uIoc_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[LinearOrder α]
{a : α}
{b : α}
{P : α → Prop}
:
See also MeasureTheory.ae_uIoc_iff.
theorem
MeasureTheory.ae_restrict_iff₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{p : α → Prop}
(hp : MeasureTheory.NullMeasurableSet {x : α | p x} (μ.restrict s))
:
theorem
MeasureTheory.ae_restrict_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{p : α → Prop}
(hp : MeasurableSet {x : α | p x})
:
theorem
MeasureTheory.ae_imp_of_ae_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{p : α → Prop}
(h : ∀ᵐ (x : α) ∂μ.restrict s, p x)
:
∀ᵐ (x : α) ∂μ, x ∈ s → p x
theorem
MeasureTheory.ae_restrict_iff'₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{p : α → Prop}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
theorem
MeasureTheory.ae_restrict_iff'
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{p : α → Prop}
(hs : MeasurableSet s)
:
theorem
Filter.EventuallyEq.restrict
{α : Type u_2}
{δ : Type u_4}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → δ}
{g : α → δ}
{s : Set α}
(hfg : f =ᶠ[MeasureTheory.Measure.ae μ] g)
:
f =ᶠ[MeasureTheory.Measure.ae (μ.restrict s)] g
theorem
MeasureTheory.ae_restrict_mem₀
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
theorem
MeasureTheory.ae_restrict_mem
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
theorem
MeasureTheory.ae_restrict_of_ae
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{p : α → Prop}
(h : ∀ᵐ (x : α) ∂μ, p x)
:
∀ᵐ (x : α) ∂μ.restrict s, p x
theorem
MeasureTheory.ae_restrict_of_ae_restrict_of_subset
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
{p : α → Prop}
(hst : s ⊆ t)
(h : ∀ᵐ (x : α) ∂μ.restrict t, p x)
:
∀ᵐ (x : α) ∂μ.restrict s, p x
theorem
MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(t : Set α)
{p : α → Prop}
(ht : ∀ᵐ (x : α) ∂μ.restrict t, p x)
(htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x)
:
∀ᵐ (x : α) ∂μ, p x
theorem
MeasureTheory.mem_map_restrict_ae_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
{s : Set α}
{t : Set β}
{f : α → β}
(hs : MeasurableSet s)
:
t ∈ Filter.map f (MeasureTheory.Measure.ae (μ.restrict s)) ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
theorem
MeasureTheory.ae_smul_measure
{R : Type u_1}
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
[Monoid R]
[DistribMulAction R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(h : ∀ᵐ (x : α) ∂μ, p x)
(c : R)
:
∀ᵐ (x : α) ∂c • μ, p x
theorem
MeasureTheory.ae_add_measure_iff
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
{ν : MeasureTheory.Measure α}
:
theorem
MeasureTheory.ae_eq_comp'
{α : Type u_2}
{β : Type u_3}
{δ : Type u_4}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → β}
{g : β → δ}
{g' : β → δ}
(hf : AEMeasurable f μ)
(h : g =ᶠ[MeasureTheory.Measure.ae ν] g')
(h2 : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.map f μ) ν)
:
g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g' ∘ f
theorem
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp
{α : Type u_2}
{β : Type u_3}
{δ : Type u_4}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → β}
{g : β → δ}
{g' : β → δ}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν)
(h : g =ᶠ[MeasureTheory.Measure.ae ν] g')
:
g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g' ∘ f
theorem
MeasureTheory.ae_eq_comp
{α : Type u_2}
{β : Type u_3}
{δ : Type u_4}
{m0 : MeasurableSpace α}
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{f : α → β}
{g : β → δ}
{g' : β → δ}
(hf : AEMeasurable f μ)
(h : g =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.map f μ)] g')
:
g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g' ∘ f
theorem
MeasureTheory.sub_ae_eq_zero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddGroup β]
(f : α → β)
(g : α → β)
:
f - g =ᶠ[MeasureTheory.Measure.ae μ] 0 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] g
theorem
MeasureTheory.div_ae_eq_one
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[Group β]
(f : α → β)
(g : α → β)
:
f / g =ᶠ[MeasureTheory.Measure.ae μ] 1 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] g
theorem
MeasureTheory.sub_nonneg_ae
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[AddGroup β]
[LE β]
[CovariantClass β β (Function.swap fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1]
(f : α → β)
(g : α → β)
:
0 ≤ᶠ[MeasureTheory.Measure.ae μ] g - f ↔ f ≤ᶠ[MeasureTheory.Measure.ae μ] g
theorem
MeasureTheory.one_le_div_ae
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[Group β]
[LE β]
[CovariantClass β β (Function.swap fun (x x_1 : β) => x * x_1) fun (x x_1 : β) => x ≤ x_1]
(f : α → β)
(g : α → β)
:
1 ≤ᶠ[MeasureTheory.Measure.ae μ] g / f ↔ f ≤ᶠ[MeasureTheory.Measure.ae μ] g
theorem
MeasureTheory.le_ae_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
MeasureTheory.Measure.ae μ ⊓ Filter.principal s ≤ MeasureTheory.Measure.ae (μ.restrict s)
@[simp]
theorem
MeasureTheory.ae_restrict_eq
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.Measure.ae (μ.restrict s) = MeasureTheory.Measure.ae μ ⊓ Filter.principal s
theorem
MeasureTheory.ae_restrict_eq_bot
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
MeasureTheory.Measure.ae (μ.restrict s) = ⊥ ↔ ↑↑μ s = 0
theorem
MeasureTheory.ae_restrict_neBot
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
:
Filter.NeBot (MeasureTheory.Measure.ae (μ.restrict s)) ↔ ↑↑μ s ≠ 0
theorem
MeasureTheory.self_mem_ae_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
:
s ∈ MeasureTheory.Measure.ae (μ.restrict s)
theorem
MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : α → Prop}
{t : α → Prop}
(hst : s =ᶠ[MeasureTheory.Measure.ae μ] t)
{p : α → Prop}
:
(∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x
If two measurable sets are ae_eq then any proposition that is almost everywhere true on one is almost everywhere true on the other
theorem
MeasureTheory.ae_restrict_congr_set
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : α → Prop}
{t : α → Prop}
(hst : s =ᶠ[MeasureTheory.Measure.ae μ] t)
{p : α → Prop}
:
(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict t, p x
If two measurable sets are ae_eq then any proposition that is almost everywhere true on one is almost everywhere true on the other
theorem
MeasureTheory.measure_setOf_frequently_eq_zero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : ℕ → α → Prop}
(hp : ∑' (i : ℕ), ↑↑μ {x : α | p i x} ≠ ⊤)
:
A version of the Borel-Cantelli lemma: if pᵢ is a sequence of predicates such that
∑ μ {x | pᵢ x} is finite, then the measure of x such that pᵢ x holds frequently as i → ∞ (or
equivalently, pᵢ x holds for infinitely many i) is equal to zero.
theorem
MeasureTheory.ae_eventually_not_mem
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : ℕ → Set α}
(hs : ∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤)
:
∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ s n
A version of the Borel-Cantelli lemma: if sᵢ is a sequence of sets such that
∑ μ sᵢ exists, then for almost all x, x does not belong to almost all sᵢ.
theorem
MeasureTheory.NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{β : Type u_7}
[MeasurableSpace β]
{b : β}
{f : α → β}
{s : Set α}
(f_mble : MeasureTheory.NullMeasurable f (μ.restrict s))
(hs : f =ᶠ[MeasureTheory.Measure.ae (μ.restrict sᶜ)] fun (x : α) => b)
{t : Set β}
(t_mble : MeasurableSet t)
(ht : b ∉ t)
:
Subtype of a measure space #
theorem
MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set ↑s}
(hs : MeasureTheory.NullMeasurableSet s μ)
(ht : MeasurableSet t)
:
MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
theorem
MeasureTheory.Measure.NullMeasurableSet.subtype_coe
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set ↑s}
(hs : MeasureTheory.NullMeasurableSet s μ)
(ht : MeasureTheory.NullMeasurableSet t (MeasureTheory.Measure.comap Subtype.val μ))
:
MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
theorem
MeasureTheory.Measure.measure_subtype_coe_le_comap
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
(t : Set ↑s)
:
↑↑μ (Subtype.val '' t) ≤ ↑↑(MeasureTheory.Measure.comap Subtype.val μ) t
theorem
MeasureTheory.Measure.measure_subtype_coe_eq_zero_of_comap_eq_zero
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasureTheory.NullMeasurableSet s μ)
{t : Set ↑s}
(ht : ↑↑(MeasureTheory.Measure.comap Subtype.val μ) t = 0)
:
noncomputable def
MeasureTheory.Measure.Subtype.measureSpace
{δ : Type u_4}
[MeasureTheory.MeasureSpace δ]
{p : δ → Prop}
:
In a measure space, one can restrict the measure to a subtype to get a new measure space.
Not registered as an instance, as there are other natural choices such as the normalized restriction
for a probability measure, or the subspace measure when restricting to a vector subspace. Enable
locally if needed with attribute [local instance] Measure.Subtype.measureSpace.
Equations
- MeasureTheory.Measure.Subtype.measureSpace = MeasureTheory.MeasureSpace.mk (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)
Instances For
theorem
MeasureTheory.Measure.Subtype.volume_def
{δ : Type u_4}
{u : Set δ}
[MeasureTheory.MeasureSpace δ]
:
MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
theorem
MeasureTheory.Measure.Subtype.volume_univ
{δ : Type u_4}
{u : Set δ}
[MeasureTheory.MeasureSpace δ]
(hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume)
:
↑↑MeasureTheory.volume Set.univ = ↑↑MeasureTheory.volume u
theorem
MeasureTheory.Measure.volume_subtype_coe_le_volume
{δ : Type u_4}
{u : Set δ}
[MeasureTheory.MeasureSpace δ]
(hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume)
(t : Set ↑u)
:
theorem
MeasureTheory.Measure.volume_subtype_coe_eq_zero_of_volume_eq_zero
{δ : Type u_4}
{u : Set δ}
[MeasureTheory.MeasureSpace δ]
(hu : MeasureTheory.NullMeasurableSet u MeasureTheory.volume)
{t : Set ↑u}
(ht : ↑↑MeasureTheory.volume t = 0)
:
theorem
MeasurableEmbedding.map_comap
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure β)
:
MeasureTheory.Measure.map f (MeasureTheory.Measure.comap f μ) = μ.restrict (Set.range f)
theorem
MeasurableEmbedding.comap_apply
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure β)
(s : Set α)
:
↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s)
theorem
MeasurableEmbedding.comap_map
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure α)
:
theorem
MeasurableEmbedding.ae_map_iff
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
{p : β → Prop}
{μ : MeasureTheory.Measure α}
:
(∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
theorem
MeasurableEmbedding.restrict_map
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure α)
(s : Set β)
:
(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
theorem
MeasurableEmbedding.comap_preimage
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure β)
(s : Set β)
:
↑↑(MeasureTheory.Measure.comap f μ) (f ⁻¹' s) = ↑↑μ (s ∩ Set.range f)
theorem
MeasurableEmbedding.comap_restrict
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure β)
(s : Set β)
:
MeasureTheory.Measure.comap f (μ.restrict s) = (MeasureTheory.Measure.comap f μ).restrict (f ⁻¹' s)
theorem
MeasurableEmbedding.restrict_comap
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
{f : α → β}
(hf : MeasurableEmbedding f)
(μ : MeasureTheory.Measure β)
(s : Set α)
:
(MeasureTheory.Measure.comap f μ).restrict s = MeasureTheory.Measure.comap f (μ.restrict (f '' s))
theorem
MeasurableEquiv.restrict_map
{α : Type u_2}
{β : Type u_3}
{m0 : MeasurableSpace α}
{m1 : MeasurableSpace β}
(e : α ≃ᵐ β)
(μ : MeasureTheory.Measure α)
(s : Set β)
:
(MeasureTheory.Measure.map (⇑e) μ).restrict s = MeasureTheory.Measure.map (⇑e) (μ.restrict (⇑e ⁻¹' s))
theorem
comap_subtype_coe_apply
{α : Type u_2}
{_m0 : MeasurableSpace α}
{s : Set α}
(hs : MeasurableSet s)
(μ : MeasureTheory.Measure α)
(t : Set ↑s)
:
↑↑(MeasureTheory.Measure.comap Subtype.val μ) t = ↑↑μ (Subtype.val '' t)
theorem
map_comap_subtype_coe
{α : Type u_2}
{m0 : MeasurableSpace α}
{s : Set α}
(hs : MeasurableSet s)
(μ : MeasureTheory.Measure α)
:
MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val μ) = μ.restrict s
theorem
ae_restrict_iff_subtype
{α : Type u_2}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
{p : α → Prop}
:
(∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : ↑s) ∂MeasureTheory.Measure.comap Subtype.val μ, p ↑x
Volume on s : Set α #
Note the instance is provided earlier as Subtype.measureSpace.
theorem
volume_set_coe_def
{α : Type u_2}
[MeasureTheory.MeasureSpace α]
(s : Set α)
:
MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
theorem
MeasurableSet.map_coe_volume
{α : Type u_2}
[MeasureTheory.MeasureSpace α]
{s : Set α}
(hs : MeasurableSet s)
:
MeasureTheory.Measure.map Subtype.val MeasureTheory.volume = MeasureTheory.volume.restrict s
theorem
volume_image_subtype_coe
{α : Type u_2}
[MeasureTheory.MeasureSpace α]
{s : Set α}
(hs : MeasurableSet s)
(t : Set ↑s)
:
@[simp]
theorem
volume_preimage_coe
{α : Type u_2}
[MeasureTheory.MeasureSpace α]
{s : Set α}
{t : Set α}
(hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume)
(ht : MeasurableSet t)
:
theorem
piecewise_ae_eq_restrict
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
{g : α → β}
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
Set.piecewise s f g =ᶠ[MeasureTheory.Measure.ae (μ.restrict s)] f
theorem
piecewise_ae_eq_restrict_compl
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
{g : α → β}
[DecidablePred fun (x : α) => x ∈ s]
(hs : MeasurableSet s)
:
Set.piecewise s f g =ᶠ[MeasureTheory.Measure.ae (μ.restrict sᶜ)] g
theorem
piecewise_ae_eq_of_ae_eq_set
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
{f : α → β}
{g : α → β}
[DecidablePred fun (x : α) => x ∈ s]
[DecidablePred fun (x : α) => x ∈ t]
(hst : s =ᶠ[MeasureTheory.Measure.ae μ] t)
:
Set.piecewise s f g =ᶠ[MeasureTheory.Measure.ae μ] Set.piecewise t f g
theorem
mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
{t : Set β}
(ht : 0 ∈ t)
(hs : MeasurableSet s)
:
t ∈ Filter.map (Set.indicator s f) (MeasureTheory.Measure.ae μ) ↔ t ∈ Filter.map f (MeasureTheory.Measure.ae (μ.restrict s))
theorem
mem_map_indicator_ae_iff_of_zero_nmem
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
{t : Set β}
(ht : 0 ∉ t)
:
t ∈ Filter.map (Set.indicator s f) (MeasureTheory.Measure.ae μ) ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
theorem
map_restrict_ae_le_map_indicator_ae
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
(hs : MeasurableSet s)
:
Filter.map f (MeasureTheory.Measure.ae (μ.restrict s)) ≤ Filter.map (Set.indicator s f) (MeasureTheory.Measure.ae μ)
theorem
indicator_ae_eq_restrict
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
(hs : MeasurableSet s)
:
Set.indicator s f =ᶠ[MeasureTheory.Measure.ae (μ.restrict s)] f
theorem
indicator_ae_eq_restrict_compl
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
(hs : MeasurableSet s)
:
Set.indicator s f =ᶠ[MeasureTheory.Measure.ae (μ.restrict sᶜ)] 0
theorem
indicator_ae_eq_of_restrict_compl_ae_eq_zero
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
(hs : MeasurableSet s)
(hf : f =ᶠ[MeasureTheory.Measure.ae (μ.restrict sᶜ)] 0)
:
theorem
indicator_ae_eq_zero_of_restrict_ae_eq_zero
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
(hs : MeasurableSet s)
(hf : f =ᶠ[MeasureTheory.Measure.ae (μ.restrict s)] 0)
:
theorem
indicator_ae_eq_of_ae_eq_set
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{t : Set α}
{f : α → β}
[Zero β]
(hst : s =ᶠ[MeasureTheory.Measure.ae μ] t)
:
theorem
indicator_meas_zero
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
(hs : ↑↑μ s = 0)
:
theorem
ae_eq_restrict_iff_indicator_ae_eq
{α : Type u_2}
{β : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
{f : α → β}
[Zero β]
{g : α → β}
(hs : MeasurableSet s)
:
f =ᶠ[MeasureTheory.Measure.ae (μ.restrict s)] g ↔ Set.indicator s f =ᶠ[MeasureTheory.Measure.ae μ] Set.indicator s g