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 α) : MeasureTheory.Measure α →ₗ[ENNReal] MeasureTheory.Measure α

Restrict a measure μ to a set s as an ℝ≥0∞-linear map.

Equations

• MeasureTheory.Measure.restrictₗ s = MeasureTheory.Measure.liftLinear (MeasureTheory.OuterMeasure.restrict s) ⋯

noncomputable def MeasureTheory.Measure.restrict {α : Type u_2} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α) : MeasureTheory.Measure α

Restrict a measure μ to a set s.

Equations

• μ.restrict s = (MeasureTheory.Measure.restrictₗ s) μ

@[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).toOuterMeasure = (MeasureTheory.OuterMeasure.restrict s) μ.toOuterMeasure

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)) : (μ.restrict s) t = μ (t ∩ s)

@[simp]

theorem MeasureTheory.Measure.restrict_apply {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasurableSet t) : (μ.restrict s) t = μ (t ∩ s)

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 ≤ᵐ[μ] 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 ≤ᵐ[μ] t) : μ.restrict s ≤ μ.restrict t

theorem MeasureTheory.Measure.restrict_congr_set {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : s =ᵐ[μ] 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) : (μ.restrict s) t = μ (t ∩ 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 μ) : (μ.restrict s) t = μ (t ∩ 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 α) : μ (t ∩ s) ≤ (μ.restrict s) t

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 α) : (μ + ν).restrict s = μ.restrict s + ν.restrict s

@[simp]

theorem MeasureTheory.Measure.restrict_zero {α : Type u_2} {_m0 : MeasurableSpace α} (s : Set α) : MeasureTheory.Measure.restrict 0 s = 0

@[simp]

theorem MeasureTheory.Measure.restrict_smul {α : Type u_2} {_m0 : MeasurableSpace α} (c : ENNReal) (μ : MeasureTheory.Measure α) (s : Set α) : (c • μ).restrict s = c • μ.restrict s

theorem MeasureTheory.Measure.restrict_restrict₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s (μ.restrict t)) : (μ.restrict t).restrict s = μ.restrict (s ∩ t)

@[simp]

theorem MeasureTheory.Measure.restrict_restrict {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) : (μ.restrict t).restrict s = μ.restrict (s ∩ t)

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 μ) : (μ.restrict t).restrict s = μ.restrict (s ∩ t)

theorem MeasureTheory.Measure.restrict_restrict' {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (ht : MeasurableSet t) : (μ.restrict t).restrict s = μ.restrict (s ∩ 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) : (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

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) : μ (t ∩ s) = 0

theorem MeasureTheory.Measure.restrict_apply_eq_zero' {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (hs : MeasurableSet s) : (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

@[simp]

theorem MeasureTheory.Measure.restrict_eq_zero {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : μ.restrict s = 0 ↔ μ s = 0

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 α} : μ.restrict ∅ = 0

@[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 μ) : μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

theorem MeasureTheory.Measure.restrict_inter_add_diff {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s

theorem MeasureTheory.Measure.restrict_union_add_inter₀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasureTheory.NullMeasurableSet t μ) : μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

theorem MeasureTheory.Measure.restrict_union_add_inter {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α) (ht : MeasurableSet t) : μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

theorem MeasureTheory.Measure.restrict_union_add_inter' {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (t : Set α) : μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

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 μ) : μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

theorem MeasureTheory.Measure.restrict_union {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : Disjoint s t) (ht : MeasurableSet t) : μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

theorem MeasureTheory.Measure.restrict_union' {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set α} (h : Disjoint s t) (hs : MeasurableSet s) : μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

@[simp]

theorem MeasureTheory.Measure.restrict_add_restrict_compl {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : μ.restrict s + μ.restrict sᶜ = μ

@[simp]

theorem MeasureTheory.Measure.restrict_compl_add_restrict {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : μ.restrict sᶜ + μ.restrict s = μ

theorem MeasureTheory.Measure.restrict_union_le {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (s' : Set α) : μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s'

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 α} : μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t

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 α} : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

theorem MeasureTheory.Measure.restrict_iUnion_congr {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α} : μ.restrict (⋃ (i : ι), s i) = ν.restrict (⋃ (i : ι), s i) ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

theorem MeasureTheory.Measure.restrict_biUnion_congr {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set ι} {t : ι → Set α} (hc : s.Countable) : μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i)

theorem MeasureTheory.Measure.restrict_sUnion_congr {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {S : Set (Set α)} (hc : S.Countable) : μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

theorem MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict {α : Type u_2} {t : Set α} {m0 : MeasurableSpace α} {m : Set (MeasureTheory.Measure α)} (hm : m.Nonempty) (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) : μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)

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) : (∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)) → μ = ν

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 : S.Countable) (hs : ⋃ i ∈ S, s i = Set.univ) : μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)

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 : S.Countable) (hs : ⋃ i ∈ S, s i = Set.univ) : (∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)) → μ = ν

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 : S.Countable) (hs : ⋃₀ S = Set.univ) : μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s

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 : S.Countable) (hs : ⋃₀ S = Set.univ) : (∀ s ∈ S, μ.restrict s = ν.restrict s) → μ = ν

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 : T.Countable) (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 : T.Countable) (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 : μ.AbsolutelyContinuous ν) (s : Set α) : (μ.restrict s).AbsolutelyContinuous (ν.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.ae (μ.restrict (⋃ (i : ι), s i)) = ⨆ (i : ι), MeasureTheory.ae (μ.restrict (s i))

@[simp]

theorem MeasureTheory.ae_restrict_union_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α) (t : Set α) : MeasureTheory.ae (μ.restrict (s ∪ t)) = MeasureTheory.ae (μ.restrict s) ⊔ MeasureTheory.ae (μ.restrict t)

theorem MeasureTheory.ae_restrict_biUnion_eq {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι} (ht : t.Countable) : MeasureTheory.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.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.ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, MeasureTheory.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) : (∀ᵐ (x : α) ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ (x : α) ∂μ.restrict s, p x) ∧ ∀ᵐ (x : α) ∂μ.restrict t, p x

theorem MeasureTheory.ae_restrict_biUnion_iff {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι} (ht : t.Countable) (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 =ᵐ[μ.restrict (⋃ (i : ι), s i)] g ↔ ∀ (i : ι), f =ᵐ[μ.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 : t.Countable) (f : α → δ) (g : α → δ) : f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.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 =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g

theorem MeasureTheory.ae_restrict_uIoc_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] (a : α) (b : α) : MeasureTheory.ae (μ.restrict (Ι a b)) = MeasureTheory.ae (μ.restrict (Set.Ioc a b)) ⊔ MeasureTheory.ae (μ.restrict (Set.Ioc b a))

theorem MeasureTheory.ae_restrict_uIoc_iff {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] {a : α} {b : α} {P : α → Prop} : (∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔ (∀ᵐ (x : α) ∂μ.restrict (Set.Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Set.Ioc b a), P x

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)) : (∀ᵐ (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} (hp : MeasurableSet {x : α | p x}) : (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → 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 μ) : (∀ᵐ (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 : MeasurableSet s) : (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

theorem Filter.EventuallyEq.restrict {α : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → δ} {g : α → δ} {s : Set α} (hfg : f =ᵐ[μ] g) : f =ᵐ[μ.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.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 α} : (∀ᵐ (x : α) ∂μ + ν, p x) ↔ (∀ᵐ (x : α) ∂μ, p x) ∧ ∀ᵐ (x : α) ∂ν, p x

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 =ᵐ[ν] g') (h2 : (MeasureTheory.Measure.map f μ).AbsolutelyContinuous ν) : g ∘ f =ᵐ[μ] 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 =ᵐ[ν] g') : g ∘ f =ᵐ[μ] 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.map f μ] g') : g ∘ f =ᵐ[μ] g' ∘ f

theorem MeasureTheory.sub_ae_eq_zero {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [AddGroup β] (f : α → β) (g : α → β) : f - g =ᵐ[μ] 0 ↔ f =ᵐ[μ] g

theorem MeasureTheory.div_ae_eq_one {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [Group β] (f : α → β) (g : α → β) : f / g =ᵐ[μ] 1 ↔ f =ᵐ[μ] 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 ≤ᵐ[μ] g - f ↔ f ≤ᵐ[μ] 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 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g

theorem MeasureTheory.le_ae_restrict {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.ae μ ⊓ Filter.principal s ≤ MeasureTheory.ae (μ.restrict s)

@[simp]

theorem MeasureTheory.ae_restrict_eq {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.ae (μ.restrict s) = MeasureTheory.ae μ ⊓ Filter.principal s

theorem MeasureTheory.ae_restrict_eq_bot {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : MeasureTheory.ae (μ.restrict s) = ⊥ ↔ μ s = 0

theorem MeasureTheory.ae_restrict_neBot {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} : (MeasureTheory.ae (μ.restrict s)).NeBot ↔ μ s ≠ 0

theorem MeasureTheory.self_mem_ae_restrict {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : s ∈ MeasureTheory.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 =ᵐ[μ] 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 =ᵐ[μ] 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} ≠ ⊤) : μ {x : α | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0

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 =ᵐ[μ.restrict sᶜ] fun (x : α) => b) {t : Set β} (t_mble : MeasurableSet t) (ht : b ∉ t) : μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' 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) : μ (Subtype.val '' t) = 0

noncomputable def MeasureTheory.Measure.Subtype.measureSpace {δ : Type u_4} [MeasureTheory.MeasureSpace δ] {p : δ → Prop} : MeasureTheory.MeasureSpace (Subtype p)

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)

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) : MeasureTheory.volume (Subtype.val '' t) ≤ MeasureTheory.volume t

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) : MeasureTheory.volume (Subtype.val '' 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 α) : MeasureTheory.Measure.comap f (MeasureTheory.Measure.map f μ) = μ

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) : MeasureTheory.volume (Subtype.val '' t) = MeasureTheory.volume t

@[simp]

theorem volume_preimage_coe {α : Type u_2} [MeasureTheory.MeasureSpace α] {s : Set α} {t : Set α} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (ht : MeasurableSet t) : MeasureTheory.volume (Subtype.val ⁻¹' t) = MeasureTheory.volume (t ∩ s)

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) : s.piecewise f g =ᵐ[μ.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) : s.piecewise f g =ᵐ[μ.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 =ᵐ[μ] t) : s.piecewise f g =ᵐ[μ] t.piecewise 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 (s.indicator f) (MeasureTheory.ae μ) ↔ t ∈ Filter.map f (MeasureTheory.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 (s.indicator f) (MeasureTheory.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.ae (μ.restrict s)) ≤ Filter.map (s.indicator f) (MeasureTheory.ae μ)

theorem indicator_ae_eq_restrict {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : MeasurableSet s) : s.indicator f =ᵐ[μ.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) : s.indicator f =ᵐ[μ.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 =ᵐ[μ.restrict sᶜ] 0) : s.indicator f =ᵐ[μ] f

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 =ᵐ[μ.restrict s] 0) : s.indicator f =ᵐ[μ] 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 =ᵐ[μ] t) : s.indicator f =ᵐ[μ] t.indicator f

theorem indicator_meas_zero {α : Type u_2} {β : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β} [Zero β] (hs : μ s = 0) : s.indicator f =ᵐ[μ] 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 =ᵐ[μ.restrict s] g ↔ s.indicator f =ᵐ[μ] s.indicator g