Exact source: Mathlib/MeasureTheory/Measure/Restrict.lean
Pinned GitHub source · Raw UTF-8 source
Back to Identifying constants on an open overlap
1/-2Copyright (c) 2017 Johannes Hölzl. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Johannes Hölzl, Mario Carneiro5-/6module78public import Mathlib.MeasureTheory.Measure.Comap9public import Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving10public import Mathlib.Data.Set.Card1112/-!13# Restricting a measure to a subset or a subtype1415Given a measure `μ` on a type `α` and a subset `s` of `α`, we define a measure `μ.restrict s` as16the restriction of `μ` to `s` (still as a measure on `α`).1718We investigate how this notion interacts with usual operations on measures (sum, pushforward,19pullback), and on sets (inclusion, union, Union).2021We also study the relationship between the restriction of a measure to a subtype (given by the22pullback under `Subtype.val`) and the restriction to a set as above.23-/2425@[expose] public section2627open scoped ENNReal NNReal Topology28open Set MeasureTheory Measure Filter MeasurableSpace ENNReal Function2930variable {R α β δ γ ι : Type*}3132namespace MeasureTheory3334variable {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace γ]35variable {μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α} {s s' t : Set α}3637namespace Measure3839/-! ### Restricting a measure -/4041/-- Restrict a measure `μ` to a set `s` as an `ℝ≥0∞`-linear map. -/42@[irreducible]43noncomputable def restrictₗ {m0 : MeasurableSpace α} (s : Set α) : Measure α →ₗ[ℝ≥0∞] Measure α :=44 liftLinear (OuterMeasure.restrict s) fun μ s' hs' t => by45 suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by46 simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_sdiff_assoc]47 exact le_toOuterMeasure_caratheodory _ _ hs' _4849/-- Restrict a measure `μ` to a set `s`. -/50noncomputable def restrict {_m0 : MeasurableSpace α} (μ : Measure α) (s : Set α) : Measure α :=51 restrictₗ s μ5253@[simp]54theorem restrictₗ_apply {_m0 : MeasurableSpace α} (s : Set α) (μ : Measure α) :55 restrictₗ s μ = μ.restrict s :=56 rfl5758/-- This lemma shows that `restrict` and `toOuterMeasure` commute. Note that the LHS has a59restrict on measures and the RHS has a restrict on outer measures. -/60theorem restrict_toOuterMeasure_eq_toOuterMeasure_restrict (h : MeasurableSet s) :61 (μ.restrict s).toOuterMeasure = OuterMeasure.restrict s μ.toOuterMeasure := by62 simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,63 toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]6465theorem restrict_apply₀ (ht : NullMeasurableSet t (μ.restrict s)) : μ.restrict s t = μ (t ∩ s) := by66 rw [restrict, restrictₗ] at ht67 rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,68 coe_toOuterMeasure]6970/-- If `t` is a measurable set, then the measure of `t` with respect to the restriction of71 the measure to `s` equals the outer measure of `t ∩ s`. An alternate version requiring that `s`72 be measurable instead of `t` exists as `Measure.restrict_apply'`. -/73@[simp]74theorem restrict_apply (ht : MeasurableSet t) : μ.restrict s t = μ (t ∩ s) :=75 restrict_apply₀ ht.nullMeasurableSet7677/-- Restriction of a measure to a subset is monotone both in set and in measure. -/78theorem restrict_mono' {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ ⦃μ ν : Measure α⦄ (hs : s ≤ᵐ[μ] s')79 (hμν : μ ≤ ν) : μ.restrict s ≤ ν.restrict s' :=80 Measure.le_iff.2 fun t ht => calc81 μ.restrict s t = μ (t ∩ s) := restrict_apply ht82 _ ≤ μ (t ∩ s') := (measure_mono_ae <| hs.mono fun _x hx ⟨hxt, hxs⟩ => ⟨hxt, hx hxs⟩)83 _ ≤ ν (t ∩ s') := le_iff'.1 hμν (t ∩ s')84 _ = ν.restrict s' t := (restrict_apply ht).symm8586/-- Restriction of a measure to a subset is monotone both in set and in measure. -/87@[mono, gcongr]88theorem restrict_mono {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ (hs : s ⊆ s') ⦃μ ν : Measure α⦄89 (hμν : μ ≤ ν) : μ.restrict s ≤ ν.restrict s' :=90 restrict_mono' (ae_of_all _ hs) hμν9192theorem restrict_mono_measure {_ : MeasurableSpace α} {μ ν : Measure α} (h : μ ≤ ν) (s : Set α) :93 μ.restrict s ≤ ν.restrict s :=94 restrict_mono subset_rfl h9596theorem restrict_mono_set {_ : MeasurableSpace α} (μ : Measure α) {s t : Set α} (h : s ⊆ t) :97 μ.restrict s ≤ μ.restrict t :=98 restrict_mono h le_rfl99100theorem restrict_mono_ae (h : s ≤ᵐ[μ] t) : μ.restrict s ≤ μ.restrict t :=101 restrict_mono' h (le_refl μ)102103theorem restrict_congr_set (h : s =ᵐ[μ] t) : μ.restrict s = μ.restrict t :=104 le_antisymm (restrict_mono_ae h.le) (restrict_mono_ae h.symm.le)105106/-- If `s` is a measurable set, then the outer measure of `t` with respect to the restriction of107the measure to `s` equals the outer measure of `t ∩ s`. This is an alternate version of108`Measure.restrict_apply`, requiring that `s` is measurable instead of `t`. -/109@[simp]110theorem restrict_apply' (hs : MeasurableSet s) : μ.restrict s t = μ (t ∩ s) := by111 rw [← toOuterMeasure_apply,112 Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,113 OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]114115theorem _root_.IsCountablySpanning.null_of_forall_inter_null {C : Set (Set α)}116 (hC : IsCountablySpanning C) (ht : ∀ t ∈ C, μ (s ∩ t) = 0) :117 μ s = 0 := by118 obtain ⟨t, ht1, ht2⟩ := hC119 rw [show s = ⋃ n, s ∩ t n by rw [← inter_iUnion, ht2, inter_univ], measure_iUnion_null_iff]120 exact fun i => ht (t i) (ht1 i)121122theorem forall_measure_inter_isCountablySpanning_eq_zero {C : Set (Set α)}123 (hC : IsCountablySpanning C) : (∀ t ∈ C, μ (s ∩ t) = 0) ↔ μ s = 0 where124 mp := hC.null_of_forall_inter_null125 mpr h t _ := measure_inter_null_of_null_left t h126127theorem _root_.IsCountablySpanning.null_of_forall_restrict_null {C : Set (Set α)}128 (hC : IsCountablySpanning C) (hm : C ⊆ MeasurableSet) (ht : ∀ t ∈ C, μ.restrict t s = 0) :129 μ s = 0 := by130 rw [← forall_measure_inter_isCountablySpanning_eq_zero hC]131 intro t htc132 simpa [← μ.restrict_apply' (hm htc)] using ht t htc133134theorem restrict_apply₀' (hs : NullMeasurableSet s μ) : μ.restrict s t = μ (t ∩ s) := by135 rw [← restrict_congr_set hs.toMeasurable_ae_eq,136 restrict_apply' (measurableSet_toMeasurable _ _),137 measure_congr ((ae_eq_refl t).inter hs.toMeasurable_ae_eq)]138139theorem restrict_le_self : μ.restrict s ≤ μ :=140 Measure.le_iff.2 fun t ht => calc141 μ.restrict s t = μ (t ∩ s) := restrict_apply ht142 _ ≤ μ t := measure_mono inter_subset_left143144theorem absolutelyContinuous_restrict : μ.restrict s ≪ μ :=145 Measure.absolutelyContinuous_of_le Measure.restrict_le_self146147variable (μ)148149theorem restrict_eq_self (h : s ⊆ t) : μ.restrict t s = μ s :=150 (le_iff'.1 restrict_le_self s).antisymm <|151 calc152 μ s ≤ μ (toMeasurable (μ.restrict t) s ∩ t) :=153 measure_mono (subset_inter (subset_toMeasurable _ _) h)154 _ = μ.restrict t s := by155 rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]156157@[simp]158theorem restrict_apply_self (s : Set α) : (μ.restrict s) s = μ s :=159 restrict_eq_self μ Subset.rfl160161variable {μ}162163theorem restrict_apply_univ (s : Set α) : μ.restrict s univ = μ s := by164 rw [restrict_apply MeasurableSet.univ, Set.univ_inter]165166theorem le_restrict_apply (s t : Set α) : μ (t ∩ s) ≤ μ.restrict s t :=167 calc168 μ (t ∩ s) = μ.restrict s (t ∩ s) := (restrict_eq_self μ inter_subset_right).symm169 _ ≤ μ.restrict s t := measure_mono inter_subset_left170171theorem restrict_apply_le (s t : Set α) : μ.restrict s t ≤ μ t :=172 Measure.le_iff'.1 restrict_le_self _173174theorem restrict_apply_superset (h : s ⊆ t) : μ.restrict s t = μ s :=175 ((measure_mono (subset_univ _)).trans_eq <| restrict_apply_univ _).antisymm176 ((restrict_apply_self μ s).symm.trans_le <| measure_mono h)177178@[simp]179theorem restrict_add {_m0 : MeasurableSpace α} (μ ν : Measure α) (s : Set α) :180 (μ + ν).restrict s = μ.restrict s + ν.restrict s :=181 (restrictₗ s).map_add μ ν182183@[simp]184theorem restrict_zero {_m0 : MeasurableSpace α} (s : Set α) : (0 : Measure α).restrict s = 0 :=185 (restrictₗ s).map_zero186187@[simp]188theorem restrict_smul {_m0 : MeasurableSpace α} {R : Type*} [SMul R ℝ≥0∞]189 [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) (μ : Measure α) (s : Set α) :190 (c • μ).restrict s = c • μ.restrict s := by191 simpa only [smul_one_smul] using! (restrictₗ s).map_smul (c • 1) μ192193theorem restrict_restrict₀ (hs : NullMeasurableSet s (μ.restrict t)) :194 (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=195 ext fun u hu => by196 simp only [Set.inter_assoc, restrict_apply hu,197 restrict_apply₀ (hu.nullMeasurableSet.inter hs)]198199@[simp]200theorem restrict_restrict (hs : MeasurableSet s) : (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=201 restrict_restrict₀ hs.nullMeasurableSet202203theorem restrict_restrict_of_subset (h : s ⊆ t) : (μ.restrict t).restrict s = μ.restrict s := by204 ext1 u hu205 rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]206 exact inter_subset_right.trans h207208theorem restrict_restrict₀' (ht : NullMeasurableSet t μ) :209 (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=210 ext fun u hu => by simp only [restrict_apply hu, restrict_apply₀' ht, inter_assoc]211212theorem restrict_restrict' (ht : MeasurableSet t) :213 (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=214 restrict_restrict₀' ht.nullMeasurableSet215216theorem restrict_comm (hs : MeasurableSet s) :217 (μ.restrict t).restrict s = (μ.restrict s).restrict t := by218 rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]219220theorem restrict_apply_eq_zero (ht : MeasurableSet t) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0 := by221 rw [restrict_apply ht]222223theorem measure_inter_eq_zero_of_restrict (h : μ.restrict s t = 0) : μ (t ∩ s) = 0 :=224 nonpos_iff_eq_zero.1 (h ▸ le_restrict_apply _ _)225226theorem restrict_apply_eq_zero' (hs : MeasurableSet s) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0 := by227 rw [restrict_apply' hs]228229@[simp]230theorem restrict_eq_zero : μ.restrict s = 0 ↔ μ s = 0 := by231 rw [← measure_univ_eq_zero, restrict_apply_univ]232233/-- If `μ s ≠ 0`, then `μ.restrict s ≠ 0`, in terms of `NeZero` instances. -/234instance restrict.neZero [NeZero (μ s)] : NeZero (μ.restrict s) :=235 ⟨mt restrict_eq_zero.mp <| NeZero.ne _⟩236237theorem restrict_zero_set {s : Set α} (h : μ s = 0) : μ.restrict s = 0 :=238 restrict_eq_zero.2 h239240@[simp]241theorem restrict_empty : μ.restrict ∅ = 0 :=242 restrict_zero_set measure_empty243244@[simp]245theorem restrict_univ : μ.restrict univ = μ :=246 ext fun s hs => by simp [hs]247248theorem restrict_inter_add_sdiff₀ (s : Set α) (ht : NullMeasurableSet t μ) :249 μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s := by250 ext1 u hu251 simp only [add_apply, restrict_apply hu, ← inter_assoc, sdiff_eq]252 exact measure_inter_add_sdiff₀ (u ∩ s) ht253254@[deprecated (since := "2026-06-03")] alias restrict_inter_add_diff₀ := restrict_inter_add_sdiff₀255256theorem restrict_inter_add_sdiff (s : Set α) (ht : MeasurableSet t) :257 μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s :=258 restrict_inter_add_sdiff₀ s ht.nullMeasurableSet259260@[deprecated (since := "2026-06-03")] alias restrict_inter_add_diff := restrict_inter_add_sdiff261262theorem restrict_union_add_inter₀ (s : Set α) (ht : NullMeasurableSet t μ) :263 μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t := by264 rw [← restrict_inter_add_sdiff₀ (s ∪ t) ht, union_inter_cancel_right, union_sdiff_right, ←265 restrict_inter_add_sdiff₀ s ht, add_comm, ← add_assoc, add_right_comm]266267theorem restrict_union_add_inter (s : Set α) (ht : MeasurableSet t) :268 μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t :=269 restrict_union_add_inter₀ s ht.nullMeasurableSet270271theorem restrict_union_add_inter' (hs : MeasurableSet s) (t : Set α) :272 μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t := by273 simpa only [union_comm, inter_comm, add_comm] using restrict_union_add_inter t hs274275theorem restrict_union₀ (h : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) :276 μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t := by277 simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]278279theorem restrict_union (h : Disjoint s t) (ht : MeasurableSet t) :280 μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t :=281 restrict_union₀ h.aedisjoint ht.nullMeasurableSet282283theorem restrict_union' (h : Disjoint s t) (hs : MeasurableSet s) :284 μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t := by285 rw [union_comm, restrict_union h.symm hs, add_comm]286287@[simp]288theorem restrict_add_restrict_compl (hs : MeasurableSet s) :289 μ.restrict s + μ.restrict sᶜ = μ := by290 rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,291 restrict_univ]292293@[simp]294theorem restrict_compl_add_restrict (hs : MeasurableSet s) : μ.restrict sᶜ + μ.restrict s = μ := by295 rw [add_comm, restrict_add_restrict_compl hs]296297theorem restrict_union_le (s s' : Set α) : μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s' :=298 le_iff.2 fun t ht ↦ by299 simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s')300301theorem restrict_iUnion_apply_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s))302 (hm : ∀ i, NullMeasurableSet (s i) μ) {t : Set α} (ht : MeasurableSet t) :303 μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t := by304 simp only [restrict_apply, ht, inter_iUnion]305 exact306 measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right)307 fun i => ht.nullMeasurableSet.inter (hm i)308309theorem restrict_iUnion_apply [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjoint on s))310 (hm : ∀ i, MeasurableSet (s i)) {t : Set α} (ht : MeasurableSet t) :311 μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t :=312 restrict_iUnion_apply_ae hd.aedisjoint (fun i => (hm i).nullMeasurableSet) ht313314theorem restrict_iUnion_apply_eq_iSup [Countable ι] {s : ι → Set α} (hd : Directed (· ⊆ ·) s)315 {t : Set α} (ht : MeasurableSet t) : μ.restrict (⋃ i, s i) t = ⨆ i, μ.restrict (s i) t := by316 simp only [restrict_apply ht, inter_iUnion]317 rw [Directed.measure_iUnion]318 exacts [hd.mono_comp _ fun s₁ s₂ => inter_subset_inter_right _]319320/-- The restriction of the pushforward measure is the pushforward of the restriction. For a version321assuming only `AEMeasurable`, see `restrict_map_of_aemeasurable`. -/322theorem restrict_map {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :323 (μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=324 ext fun t ht => by simp [*, hf ht]325326theorem restrict_inter_toMeasurable (h : μ s ≠ ∞) (ht : MeasurableSet t) (hst : s ⊆ t) :327 μ.restrict (t ∩ toMeasurable μ s) = μ.restrict s := by328 ext u hu329 rw [restrict_apply hu, restrict_apply hu, inter_comm t, inter_comm, inter_assoc,330 measure_toMeasurable_inter (ht.inter hu) h]331 congr 1332 grind333334theorem restrict_toMeasurable (h : μ s ≠ ∞) : μ.restrict (toMeasurable μ s) = μ.restrict s := by335 simpa using restrict_inter_toMeasurable h MeasurableSet.univ (subset_univ _)336337theorem restrict_eq_self_of_ae_mem {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃μ : Measure α⦄338 (hs : ∀ᵐ x ∂μ, x ∈ s) : μ.restrict s = μ :=339 calc340 μ.restrict s = μ.restrict univ := restrict_congr_set (eventuallyEq_univ.mpr hs)341 _ = μ := restrict_univ342343theorem restrict_congr_meas (hs : MeasurableSet s) :344 μ.restrict s = ν.restrict s ↔ ∀ t ⊆ s, MeasurableSet t → μ t = ν t :=345 ⟨fun H t hts ht => by346 rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht], fun H =>347 ext fun t ht => by348 rw [restrict_apply ht, restrict_apply ht, H _ inter_subset_right (ht.inter hs)]⟩349350theorem restrict_congr_mono (hs : s ⊆ t) (h : μ.restrict t = ν.restrict t) :351 μ.restrict s = ν.restrict s := by352 rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]353354/-- If two measures agree on all measurable subsets of `s` and `t`, then they agree on all355measurable subsets of `s ∪ t`. -/356theorem restrict_union_congr :357 μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔358 μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t := by359 refine ⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h,360 restrict_congr_mono subset_union_right h⟩, ?_⟩361 rintro ⟨hs, ht⟩362 ext1 u hu363 simp only [restrict_apply hu, inter_union_distrib_left]364 rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩365 calc366 μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) :=367 measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl368 _ = μ US + μ ((u ∩ t) \ US) := (measure_add_sdiff hm.nullMeasurableSet _).symm369 _ = restrict μ s u + restrict μ t (u \ US) := by370 simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_sdiff_assoc]371 _ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]372 _ = ν US + ν ((u ∩ t) \ US) := by373 simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_sdiff_assoc]374 _ = ν (US ∪ u ∩ t) := measure_add_sdiff hm.nullMeasurableSet _375 _ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl376377theorem restrict_biUnion_finset_congr {s : Finset ι} {t : ι → Set α} :378 μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔379 ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i) := by380 classical381 induction s using Finset.induction_on with382 | empty => simp383 | insert i s _ hs =>384 simp only [forall_eq_or_imp, iUnion_iUnion_eq_or_left, Finset.mem_insert]385 rw [restrict_union_congr, ← hs]386387theorem restrict_iUnion_congr [Countable ι] {s : ι → Set α} :388 μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔ ∀ i, μ.restrict (s i) = ν.restrict (s i) := by389 refine ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => ?_⟩390 ext1 t ht391 have D : Directed (· ⊆ ·) fun t : Finset ι => ⋃ i ∈ t, s i :=392 Monotone.directed_le fun t₁ t₂ ht => biUnion_subset_biUnion_left ht393 rw [iUnion_eq_iUnion_finset]394 simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_biUnion_finset_congr.2 fun i _ => h i]395396theorem restrict_biUnion_congr {s : Set ι} {t : ι → Set α} (hc : s.Countable) :397 μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔398 ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i) := by399 haveI := hc.toEncodable400 simp only [biUnion_eq_iUnion, SetCoe.forall', restrict_iUnion_congr]401402theorem restrict_sUnion_congr {S : Set (Set α)} (hc : S.Countable) :403 μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s := by404 rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]405406/-- This lemma shows that `Inf` and `restrict` commute for measures. -/407theorem restrict_sInf_eq_sInf_restrict {m0 : MeasurableSpace α} {m : Set (Measure α)}408 (hm : m.Nonempty) (ht : MeasurableSet t) :409 (sInf m).restrict t = sInf ((fun μ : Measure α => μ.restrict t) '' m) := by410 ext1 s hs411 simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht),412 Set.image_image, restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ←413 Set.image_image _ toOuterMeasure, ← OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _),414 OuterMeasure.restrict_apply]415416theorem exists_mem_of_measure_ne_zero_of_ae (hs : μ s ≠ 0) {p : α → Prop}417 (hp : ∀ᵐ x ∂μ.restrict s, p x) : ∃ x, x ∈ s ∧ p x := by418 rw [← μ.restrict_apply_self, ← frequently_ae_mem_iff] at hs419 exact (hs.and_eventually hp).exists420421/-- If a quasi-measure-preserving map `f` maps a set `s` to a set `t`,422then it is quasi-measure-preserving with respect to the restrictions of the measures. -/423theorem QuasiMeasurePreserving.restrict {ν : Measure β} {f : α → β}424 (hf : QuasiMeasurePreserving f μ ν) {t : Set β} (hmaps : MapsTo f s t) :425 QuasiMeasurePreserving f (μ.restrict s) (ν.restrict t) where426 measurable := hf.measurable427 absolutelyContinuous := by428 refine AbsolutelyContinuous.mk fun u hum ↦ ?_429 suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]430 refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)431 rw [preimage_inter]432 gcongr433 assumption434435/-! ### Extensionality results -/436437/-- Two measures are equal if they have equal restrictions on a spanning collection of sets438 (formulated using `Union`). -/439theorem ext_iff_of_iUnion_eq_univ [Countable ι] {s : ι → Set α} (hs : ⋃ i, s i = univ) :440 μ = ν ↔ ∀ i, μ.restrict (s i) = ν.restrict (s i) := by441 rw [← restrict_iUnion_congr, hs, restrict_univ, restrict_univ]442443alias ⟨_, ext_of_iUnion_eq_univ⟩ := ext_iff_of_iUnion_eq_univ444445/-- Two measures are equal if they have equal restrictions on a spanning collection of sets446 (formulated using `biUnion`). -/447theorem ext_iff_of_biUnion_eq_univ {S : Set ι} {s : ι → Set α} (hc : S.Countable)448 (hs : ⋃ i ∈ S, s i = univ) : μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i) := by449 rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]450451alias ⟨_, ext_of_biUnion_eq_univ⟩ := ext_iff_of_biUnion_eq_univ452453/-- Two measures are equal if they have equal restrictions on a spanning collection of sets454 (formulated using `sUnion`). -/455theorem ext_iff_of_sUnion_eq_univ {S : Set (Set α)} (hc : S.Countable) (hs : ⋃₀ S = univ) :456 μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s :=457 ext_iff_of_biUnion_eq_univ hc <| by rwa [← sUnion_eq_biUnion]458459alias ⟨_, ext_of_sUnion_eq_univ⟩ := ext_iff_of_sUnion_eq_univ460461theorem ext_of_generateFrom_of_cover {S T : Set (Set α)} (h_gen : ‹_› = generateFrom S)462 (hc : T.Countable) (h_inter : IsPiSystem S) (hU : ⋃₀ T = univ) (htop : ∀ t ∈ T, μ t ≠ ∞)463 (ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)) (T_eq : ∀ t ∈ T, μ t = ν t) : μ = ν := by464 refine ext_of_sUnion_eq_univ hc hU fun t ht => ?_465 ext1 u hu466 simp only [restrict_apply hu]467 induction u, hu using induction_on_inter h_gen h_inter with468 | empty => simp only [Set.empty_inter, measure_empty]469 | basic u hu => exact ST_eq _ ht _ hu470 | compl u hu ihu =>471 have := T_eq t ht472 rw [Set.inter_comm] at ihu ⊢473 rwa [← measure_inter_add_sdiff t hu, ← measure_inter_add_sdiff t hu, ← ihu,474 ENNReal.add_right_inj] at this475 exact ne_top_of_le_ne_top (htop t ht) (measure_mono Set.inter_subset_left)476 | iUnion f hfd hfm ihf =>477 simp only [← restrict_apply (hfm _), ← restrict_apply (MeasurableSet.iUnion hfm)] at ihf ⊢478 simp only [measure_iUnion hfd hfm, ihf]479480/-- Two measures are equal if they are equal on the π-system generating the σ-algebra,481 and they are both finite on an increasing spanning sequence of sets in the π-system.482 This lemma is formulated using `sUnion`. -/483theorem ext_of_generateFrom_of_cover_subset {S T : Set (Set α)} (h_gen : ‹_› = generateFrom S)484 (h_inter : IsPiSystem S) (h_sub : T ⊆ S) (hc : T.Countable) (hU : ⋃₀ T = univ)485 (htop : ∀ s ∈ T, μ s ≠ ∞) (h_eq : ∀ s ∈ S, μ s = ν s) : μ = ν := by486 refine ext_of_generateFrom_of_cover h_gen hc h_inter hU htop ?_ fun t ht => h_eq t (h_sub ht)487 intro t ht s hs; rcases (s ∩ t).eq_empty_or_nonempty with H | H488 · simp only [H, measure_empty]489 · exact h_eq _ (h_inter _ hs _ (h_sub ht) H)490491/-- Two measures are equal if they are equal on the π-system generating the σ-algebra,492 and they are both finite on an increasing spanning sequence of sets in the π-system.493 This lemma is formulated using `iUnion`.494 `FiniteSpanningSetsIn.ext` is a reformulation of this lemma. -/495theorem ext_of_generateFrom_of_iUnion (C : Set (Set α)) (B : ℕ → Set α) (hA : ‹_› = generateFrom C)496 (hC : IsPiSystem C) (h1B : ⋃ i, B i = univ) (h2B : ∀ i, B i ∈ C) (hμB : ∀ i, μ (B i) ≠ ∞)497 (h_eq : ∀ s ∈ C, μ s = ν s) : μ = ν := by498 refine ext_of_generateFrom_of_cover_subset hA hC ?_ (countable_range B) h1B ?_ h_eq499 · rintro _ ⟨i, rfl⟩500 apply h2B501 · rintro _ ⟨i, rfl⟩502 apply hμB503504@[simp]505theorem restrict_sum (μ : ι → Measure α) {s : Set α} (hs : MeasurableSet s) :506 (sum μ).restrict s = sum fun i => (μ i).restrict s :=507 ext fun t ht => by simp only [sum_apply, restrict_apply, ht, ht.inter hs]508509@[simp]510theorem restrict_sum_of_countable [Countable ι] (μ : ι → Measure α) (s : Set α) :511 (sum μ).restrict s = sum fun i => (μ i).restrict s := by512 ext t ht513 simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]514515lemma AbsolutelyContinuous.restrict (h : μ ≪ ν) (s : Set α) : μ.restrict s ≪ ν.restrict s := by516 refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)517 rw [restrict_apply ht] at htν ⊢518 exact h htν519520theorem restrict_iUnion_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s))521 (hm : ∀ i, NullMeasurableSet (s i) μ) : μ.restrict (⋃ i, s i) = sum fun i => μ.restrict (s i) :=522 ext fun t ht => by simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]523524theorem restrict_iUnion [Countable ι] {s : ι → Set α} (hd : Pairwise (Disjoint on s))525 (hm : ∀ i, MeasurableSet (s i)) : μ.restrict (⋃ i, s i) = sum fun i => μ.restrict (s i) :=526 restrict_iUnion_ae hd.aedisjoint fun i => (hm i).nullMeasurableSet527528theorem restrict_biUnion {s : ι → Set α} {T : Set ι} (hT : Countable T)529 (hd : T.Pairwise (Disjoint on s)) (hm : ∀ i, MeasurableSet (s i)) :530 μ.restrict (⋃ i ∈ T, s i) = sum fun (i : T) => μ.restrict (s i) := by531 rw [Set.biUnion_eq_iUnion]532 exact restrict_iUnion (fun i j hij ↦ hd i.coe_prop j.coe_prop (Subtype.coe_ne_coe.mpr hij)) (hm ·)533534theorem restrict_biUnion_finset {s : ι → Set α} {T : Finset ι}535 (hd : (T : Set ι).Pairwise (Disjoint on s)) (hm : ∀ i, MeasurableSet (s i)) :536 μ.restrict (⋃ i ∈ T, s i) = sum fun (i : T) => μ.restrict (s i) :=537 restrict_biUnion (T := (T : Set ι)) Finite.to_countable hd hm538539theorem restrict_iUnion_le [Countable ι] {s : ι → Set α} :540 μ.restrict (⋃ i, s i) ≤ sum fun i => μ.restrict (s i) :=541 le_iff.2 fun t ht ↦ by simpa [ht, inter_iUnion] using measure_iUnion_le (t ∩ s ·)542543theorem restrict_biUnion_le {s : ι → Set α} {T : Set ι} (hT : Countable T) :544 μ.restrict (⋃ i ∈ T, s i) ≤ sum fun (i : T) => μ.restrict (s i) :=545 le_iff.2 fun t ht ↦ by simpa [ht, inter_iUnion] using measure_biUnion_le μ hT (t ∩ s ·)546547end Measure548549@[simp]550theorem ae_restrict_iUnion_eq [Countable ι] (s : ι → Set α) :551 ae (μ.restrict (⋃ i, s i)) = ⨆ i, ae (μ.restrict (s i)) :=552 le_antisymm ((ae_sum_eq fun i => μ.restrict (s i)) ▸ ae_mono restrict_iUnion_le) <|553 iSup_le fun i => ae_mono <| restrict_mono (subset_iUnion s i) le_rfl554555@[simp]556theorem ae_restrict_union_eq (s t : Set α) :557 ae (μ.restrict (s ∪ t)) = ae (μ.restrict s) ⊔ ae (μ.restrict t) := by558 simp [union_eq_iUnion, iSup_bool_eq]559560theorem ae_restrict_biUnion_eq (s : ι → Set α) {t : Set ι} (ht : t.Countable) :561 ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i)) := by562 haveI := ht.to_subtype563 rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']564565theorem ae_restrict_biUnion_finset_eq (s : ι → Set α) (t : Finset ι) :566 ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i)) :=567 ae_restrict_biUnion_eq s t.countable_toSet568569theorem ae_restrict_iUnion_iff [Countable ι] (s : ι → Set α) (p : α → Prop) :570 (∀ᵐ x ∂μ.restrict (⋃ i, s i), p x) ↔ ∀ i, ∀ᵐ x ∂μ.restrict (s i), p x := by simp571572theorem ae_restrict_union_iff (s t : Set α) (p : α → Prop) :573 (∀ᵐ x ∂μ.restrict (s ∪ t), p x) ↔ (∀ᵐ x ∂μ.restrict s, p x) ∧ ∀ᵐ x ∂μ.restrict t, p x := by simp574575theorem ae_restrict_biUnion_iff (s : ι → Set α) {t : Set ι} (ht : t.Countable) (p : α → Prop) :576 (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s i), p x := by577 simp_rw [Filter.Eventually, ae_restrict_biUnion_eq s ht, mem_iSup]578579@[simp]580theorem ae_restrict_biUnion_finset_iff (s : ι → Set α) (t : Finset ι) (p : α → Prop) :581 (∀ᵐ x ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ x ∂μ.restrict (s i), p x := by582 simp_rw [Filter.Eventually, ae_restrict_biUnion_finset_eq s, mem_iSup]583584theorem ae_eq_restrict_iUnion_iff [Countable ι] (s : ι → Set α) (f g : α → δ) :585 f =ᵐ[μ.restrict (⋃ i, s i)] g ↔ ∀ i, f =ᵐ[μ.restrict (s i)] g := by586 simp_rw [EventuallyEq, ae_restrict_iUnion_eq, eventually_iSup]587588theorem ae_eq_restrict_biUnion_iff (s : ι → Set α) {t : Set ι} (ht : t.Countable) (f g : α → δ) :589 f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g := by590 simp_rw [ae_restrict_biUnion_eq s ht, EventuallyEq, eventually_iSup]591592theorem ae_eq_restrict_biUnion_finset_iff (s : ι → Set α) (t : Finset ι) (f g : α → δ) :593 f =ᵐ[μ.restrict (⋃ i ∈ t, s i)] g ↔ ∀ i ∈ t, f =ᵐ[μ.restrict (s i)] g :=594 ae_eq_restrict_biUnion_iff s t.countable_toSet f g595596open scoped Interval in597theorem ae_restrict_uIoc_eq [LinearOrder α] (a b : α) :598 ae (μ.restrict (Ι a b)) = ae (μ.restrict (Ioc a b)) ⊔ ae (μ.restrict (Ioc b a)) := by599 simp only [uIoc_eq_union, ae_restrict_union_eq]600601open scoped Interval in602/-- See also `MeasureTheory.ae_uIoc_iff`. -/603theorem ae_restrict_uIoc_iff [LinearOrder α] {a b : α} {P : α → Prop} :604 (∀ᵐ x ∂μ.restrict (Ι a b), P x) ↔605 (∀ᵐ x ∂μ.restrict (Ioc a b), P x) ∧ ∀ᵐ x ∂μ.restrict (Ioc b a), P x := by606 rw [ae_restrict_uIoc_eq, eventually_sup]607608theorem ae_restrict_iff₀ {p : α → Prop} (hp : NullMeasurableSet { x | p x } (μ.restrict s)) :609 (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x := by610 simp only [ae_iff, ← compl_setOf, Measure.restrict_apply₀ hp.compl]611 rw [iff_iff_eq]; congr with x; simp [and_comm]612613theorem ae_restrict_iff {p : α → Prop} (hp : MeasurableSet { x | p x }) :614 (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=615 ae_restrict_iff₀ hp.nullMeasurableSet616617theorem ae_imp_of_ae_restrict {s : Set α} {p : α → Prop} (h : ∀ᵐ x ∂μ.restrict s, p x) :618 ∀ᵐ x ∂μ, x ∈ s → p x := by619 simp only [ae_iff] at h ⊢620 simpa [setOf_and, inter_comm] using measure_inter_eq_zero_of_restrict h621622theorem ae_restrict_iff'₀ {p : α → Prop} (hs : NullMeasurableSet s μ) :623 (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x := by624 simp only [ae_iff, ← compl_setOf, restrict_apply₀' hs]625 rw [iff_iff_eq]; congr with x; simp [and_comm]626627theorem ae_restrict_iff' {p : α → Prop} (hs : MeasurableSet s) :628 (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=629 ae_restrict_iff'₀ hs.nullMeasurableSet630631theorem _root_.Filter.EventuallyEq.restrict {f g : α → δ} {s : Set α} (hfg : f =ᵐ[μ] g) :632 f =ᵐ[μ.restrict s] g := by633 -- note that we cannot use `ae_restrict_iff` since we do not require measurability634 refine hfg.filter_mono ?_635 rw [Measure.ae_le_iff_absolutelyContinuous]636 exact absolutelyContinuous_restrict637638theorem ae_restrict_mem₀ (hs : NullMeasurableSet s μ) : ∀ᵐ x ∂μ.restrict s, x ∈ s :=639 (ae_restrict_iff'₀ hs).2 (Filter.Eventually.of_forall fun _ => id)640641theorem ae_restrict_mem (hs : MeasurableSet s) : ∀ᵐ x ∂μ.restrict s, x ∈ s :=642 ae_restrict_mem₀ hs.nullMeasurableSet643644theorem ae_restrict_of_forall_mem {μ : Measure α} {s : Set α}645 (hs : MeasurableSet s) {p : α → Prop} (h : ∀ x ∈ s, p x) : ∀ᵐ (x : α) ∂μ.restrict s, p x :=646 (ae_restrict_mem hs).mono h647648lemma _root_.Set.EqOn.aeEq_restrict {α β : Type*} [MeasurableSpace α] {μ : Measure α} {s : Set α}649 {f g : α → β} (h : s.EqOn f g) (hs : MeasurableSet s) : f =ᵐ[μ.restrict s] g :=650 ae_restrict_of_forall_mem hs h651652theorem ae_restrict_of_ae {s : Set α} {p : α → Prop} (h : ∀ᵐ x ∂μ, p x) : ∀ᵐ x ∂μ.restrict s, p x :=653 h.filter_mono (ae_mono Measure.restrict_le_self)654655theorem ae_restrict_of_ae_restrict_of_subset {s t : Set α} {p : α → Prop} (hst : s ⊆ t)656 (h : ∀ᵐ x ∂μ.restrict t, p x) : ∀ᵐ x ∂μ.restrict s, p x :=657 h.filter_mono (ae_mono <| Measure.restrict_mono hst (le_refl μ))658659theorem ae_of_ae_restrict_of_ae_restrict_compl (t : Set α) {p : α → Prop}660 (ht : ∀ᵐ x ∂μ.restrict t, p x) (htc : ∀ᵐ x ∂μ.restrict tᶜ, p x) : ∀ᵐ x ∂μ, p x :=661 nonpos_iff_eq_zero.1 <|662 calc663 μ { x | ¬p x } ≤ μ ({ x | ¬p x } ∩ t) + μ ({ x | ¬p x } ∩ tᶜ) :=664 measure_le_inter_add_sdiff _ _ _665 _ ≤ μ.restrict t { x | ¬p x } + μ.restrict tᶜ { x | ¬p x } :=666 add_le_add (le_restrict_apply _ _) (le_restrict_apply _ _)667 _ = 0 := by rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]668669theorem mem_map_restrict_ae_iff {β} {s : Set α} {t : Set β} {f : α → β} (hs : MeasurableSet s) :670 t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0 := by671 rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]672673@[simp] theorem ae_add_measure_iff {p : α → Prop} {ν} :674 (∀ᵐ x ∂μ + ν, p x) ↔ (∀ᵐ x ∂μ, p x) ∧ ∀ᵐ x ∂ν, p x :=675 add_eq_zero676677/-- See also `Measure.ae_sum_iff`. -/678@[simp] lemma ae_finsetSum_measure_iff {p : α → Prop} {s : Finset ι} {μ : ι → Measure α} :679 (∀ᵐ x ∂∑ i ∈ s, μ i, p x) ↔ ∀ i ∈ s, ∀ᵐ x ∂μ i, p x := by680 induction s using Finset.cons_induction <;> simp [*]681682theorem ae_eq_comp' {ν : Measure β} {f : α → β} {g g' : β → δ} (hf : AEMeasurable f μ)683 (h : g =ᵐ[ν] g') (h2 : μ.map f ≪ ν) : g ∘ f =ᵐ[μ] g' ∘ f :=684 (tendsto_ae_map hf).mono_right h2.ae_le h685686theorem Measure.QuasiMeasurePreserving.ae_eq_comp {ν : Measure β} {f : α → β} {g g' : β → δ}687 (hf : QuasiMeasurePreserving f μ ν) (h : g =ᵐ[ν] g') : g ∘ f =ᵐ[μ] g' ∘ f :=688 ae_eq_comp' hf.aemeasurable h hf.absolutelyContinuous689690theorem ae_eq_comp {f : α → β} {g g' : β → δ} (hf : AEMeasurable f μ) (h : g =ᵐ[μ.map f] g') :691 g ∘ f =ᵐ[μ] g' ∘ f :=692 ae_eq_comp' hf h AbsolutelyContinuous.rfl693694@[to_additive]695theorem div_ae_eq_one {β} [Group β] (f g : α → β) : f / g =ᵐ[μ] 1 ↔ f =ᵐ[μ] g := by696 refine ⟨fun h ↦ h.mono fun x hx ↦ ?_, fun h ↦ h.mono fun x hx ↦ ?_⟩697 · rwa [Pi.div_apply, Pi.one_apply, div_eq_one] at hx698 · rwa [Pi.div_apply, Pi.one_apply, div_eq_one]699700@[to_additive sub_nonneg_ae]701lemma one_le_div_ae {β : Type*} [Group β] [LE β] [MulRightMono β] (f g : α → β) :702 1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g := by703 refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩704 · rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha705 · rwa [Pi.one_apply, Pi.div_apply, one_le_div']706707theorem le_ae_restrict : ae μ ⊓ 𝓟 s ≤ ae (μ.restrict s) := fun _s hs =>708 eventually_inf_principal.2 (ae_imp_of_ae_restrict hs)709710@[simp]711theorem ae_restrict_eq (hs : MeasurableSet s) : ae (μ.restrict s) = ae μ ⊓ 𝓟 s := by712 ext t713 simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_setOf,714 Classical.not_imp, fun a => and_comm (a := a ∈ s) (b := a ∉ t)]715 rfl716717lemma ae_restrict_le : ae (μ.restrict s) ≤ ae μ :=718 ae_mono restrict_le_self719720theorem ae_restrict_eq_bot {s} : ae (μ.restrict s) = ⊥ ↔ μ s = 0 :=721 ae_eq_bot.trans restrict_eq_zero722723theorem ae_restrict_neBot {s} : (ae <| μ.restrict s).NeBot ↔ μ s ≠ 0 :=724 neBot_iff.trans ae_restrict_eq_bot.not725726theorem self_mem_ae_restrict {s} (hs : MeasurableSet s) : s ∈ ae (μ.restrict s) := by727 simp only [ae_restrict_eq hs, mem_principal, mem_inf_iff]728 exact ⟨_, univ_mem, s, Subset.rfl, (univ_inter s).symm⟩729730/-- If two measurable sets are `ae_eq` then any proposition that is almost everywhere true on one731is almost everywhere true on the other -/732theorem ae_restrict_of_ae_eq_of_ae_restrict {s t} (hst : s =ᵐ[μ] t) {p : α → Prop} :733 (∀ᵐ x ∂μ.restrict s, p x) → ∀ᵐ x ∂μ.restrict t, p x := by simp [Measure.restrict_congr_set hst]734735/-- If two measurable sets are `ae_eq` then any proposition that is almost everywhere true on one736is almost everywhere true on the other -/737theorem ae_restrict_congr_set {s t} (hst : s =ᵐ[μ] t) {p : α → Prop} :738 (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ.restrict t, p x :=739 ⟨ae_restrict_of_ae_eq_of_ae_restrict hst, ae_restrict_of_ae_eq_of_ae_restrict hst.symm⟩740741lemma NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const742 {β : Type*} [MeasurableSpace β] {b : β} {f : α → β} {s : Set α}743 (f_mble : NullMeasurable f (μ.restrict s)) (hs : f =ᵐ[Measure.restrict μ sᶜ] (fun _ ↦ b))744 {t : Set β} (t_mble : MeasurableSet t) (ht : b ∉ t) :745 μ (f ⁻¹' t) = μ.restrict s (f ⁻¹' t) := by746 rw [Measure.restrict_apply₀ (f_mble t_mble)]747 rw [EventuallyEq, ae_iff, Measure.restrict_apply₀] at hs748 · apply le_antisymm _ (measure_mono inter_subset_left)749 apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans750 apply (measure_union_le _ _).trans751 suffices μ ((f ⁻¹' t) ∩ sᶜ) = 0 by simp [this]752 rw [← nonpos_iff_eq_zero, ← hs]753 gcongr754 exact fun x hx hfx ↦ ht (hfx ▸ hx)755 · exact NullMeasurableSet.of_null hs756757lemma nullMeasurableSet_restrict (hs : NullMeasurableSet s μ) {t : Set α} :758 NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet (t ∩ s) μ := by759 refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩760 · obtain ⟨t', -, ht', t't⟩ : ∃ t' ⊇ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=761 h.exists_measurable_superset_ae_eq762 have A : (t' ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := by763 have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t') = (x ∈ t) :=764 (ae_restrict_iff'₀ hs).1 t't765 filter_upwards [this] with y hy766 change (y ∈ t' ∩ s) = (y ∈ t ∩ s)767 simpa only [eq_iff_iff, mem_inter_iff, and_congr_left_iff] using hy768 obtain ⟨s', -, hs', s's⟩ : ∃ s' ⊇ s, MeasurableSet s' ∧ s' =ᵐ[μ] s :=769 hs.exists_measurable_superset_ae_eq770 have B : (t' ∩ s' : Set α) =ᵐ[μ] (t' ∩ s : Set α) :=771 ae_eq_set_inter (EventuallyEq.refl _ _) s's772 exact (ht'.inter hs').nullMeasurableSet.congr (B.trans A)773 · have A : NullMeasurableSet (t \ s) (μ.restrict s) := by774 apply NullMeasurableSet.of_null775 rw [Measure.restrict_apply₀' hs]776 simp777 have B : NullMeasurableSet (t ∩ s) (μ.restrict s) :=778 h.mono_ac absolutelyContinuous_restrict779 simpa using A.union B780781lemma nullMeasurableSet_restrict_of_subset {t : Set α} (ht : t ⊆ s) :782 NullMeasurableSet t (μ.restrict s) ↔ NullMeasurableSet t μ := by783 refine ⟨fun h ↦ ?_, fun h ↦ h.mono_ac absolutelyContinuous_restrict⟩784 obtain ⟨t', t'_subs, ht', t't⟩ : ∃ t' ⊆ t, MeasurableSet t' ∧ t' =ᵐ[μ.restrict s] t :=785 h.exists_measurable_subset_ae_eq786 have : ∀ᵐ x ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t) := by787 apply ae_imp_of_ae_restrict788 filter_upwards [t't] with x hx using by simpa using! hx789 have : t' =ᵐ[μ] t := by790 filter_upwards [this] with x hx791 change (x ∈ t') = (x ∈ t)792 simp only [eq_iff_iff]793 tauto794 exact ht'.nullMeasurableSet.congr this795796namespace Measure797798section Subtype799800/-! ### Subtype of a measure space -/801802section ComapAnyMeasure803804theorem MeasurableSet.nullMeasurableSet_subtype_coe {t : Set s} (hs : NullMeasurableSet s μ)805 (ht : MeasurableSet t) : NullMeasurableSet ((↑) '' t) μ := by806 rw [Subtype.instMeasurableSpace, comap_eq_generateFrom] at ht807 induction t, ht using generateFrom_induction with808 | hC t' ht' =>809 obtain ⟨s', hs', rfl⟩ := ht'810 rw [Subtype.image_preimage_coe]811 exact hs.inter (hs'.nullMeasurableSet)812 | empty => simp only [image_empty, nullMeasurableSet_empty]813 | compl t' _ ht' =>814 simp only [← range_sdiff_image Subtype.coe_injective, Subtype.range_coe_subtype, setOf_mem_eq]815 exact hs.diff ht'816 | iUnion f _ hf =>817 rw [image_iUnion]818 exact .iUnion hf819820theorem NullMeasurableSet.subtype_coe {t : Set s} (hs : NullMeasurableSet s μ)821 (ht : NullMeasurableSet t (μ.comap Subtype.val)) : NullMeasurableSet (((↑) : s → α) '' t) μ :=822 NullMeasurableSet.image _ μ Subtype.coe_injective823 (fun _ => MeasurableSet.nullMeasurableSet_subtype_coe hs) ht824825theorem measure_subtype_coe_le_comap (hs : NullMeasurableSet s μ) (t : Set s) :826 μ (((↑) : s → α) '' t) ≤ μ.comap Subtype.val t :=827 le_comap_apply _ _ Subtype.coe_injective (fun _ =>828 MeasurableSet.nullMeasurableSet_subtype_coe hs) _829830theorem measure_subtype_coe_eq_zero_of_comap_eq_zero (hs : NullMeasurableSet s μ) {t : Set s}831 (ht : μ.comap Subtype.val t = 0) : μ (((↑) : s → α) '' t) = 0 :=832 eq_bot_iff.mpr <| (measure_subtype_coe_le_comap hs t).trans ht.le833834end ComapAnyMeasure835836section MeasureSpace837838variable {u : Set δ} [MeasureSpace δ] {p : δ → Prop}839840/-- In a measure space, one can restrict the measure to a subtype to get a new measure space.841Not registered as an instance, as there are other natural choices such as the normalized restriction842for a probability measure, or the subspace measure when restricting to a vector subspace. Enable843locally if needed with `attribute [local instance] Measure.Subtype.measureSpace`. -/844@[instance_reducible]845noncomputable def Subtype.measureSpace : MeasureSpace (Subtype p) where846 volume := Measure.comap Subtype.val volume847848attribute [local instance] Subtype.measureSpace849850theorem Subtype.volume_def : (volume : Measure u) = volume.comap Subtype.val :=851 rfl852853theorem Subtype.volume_univ (hu : NullMeasurableSet u) : volume (univ : Set u) = volume u := by854 rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]855 · simp only [image_univ, Subtype.range_coe_subtype, setOf_mem_eq]856 · exact Subtype.coe_injective857 · exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu858859theorem volume_subtype_coe_le_volume (hu : NullMeasurableSet u) (t : Set u) :860 volume (((↑) : u → δ) '' t) ≤ volume t :=861 measure_subtype_coe_le_comap hu t862863theorem volume_subtype_coe_eq_zero_of_volume_eq_zero (hu : NullMeasurableSet u) {t : Set u}864 (ht : volume t = 0) : volume (((↑) : u → δ) '' t) = 0 :=865 measure_subtype_coe_eq_zero_of_comap_eq_zero hu ht866867end MeasureSpace868869end Subtype870871end Measure872873end MeasureTheory874875open MeasureTheory Measure876877namespace MeasurableEmbedding878879variable {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β}880881section882variable (hf : MeasurableEmbedding f)883include hf884885theorem map_comap (μ : Measure β) : (comap f μ).map f = μ.restrict (range f) := by886 ext1 t ht887 rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),888 image_preimage_eq_inter_range, Measure.restrict_apply ht]889890theorem comap_apply (μ : Measure β) (s : Set α) : comap f μ s = μ (f '' s) :=891 calc892 comap f μ s = comap f μ (f ⁻¹' f '' s) := by rw [hf.injective.preimage_image]893 _ = (comap f μ).map f (f '' s) := (hf.map_apply _ _).symm894 _ = μ (f '' s) := by895 rw [hf.map_comap, restrict_apply' hf.measurableSet_range,896 inter_eq_self_of_subset_left (image_subset_range _ _)]897898theorem comap_map (μ : Measure α) : (map f μ).comap f = μ := by899 ext t _900 rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]901902theorem ae_map_iff {p : β → Prop} {μ : Measure α} : (∀ᵐ x ∂μ.map f, p x) ↔ ∀ᵐ x ∂μ, p (f x) := by903 simp only [ae_iff, hf.map_apply, preimage_setOf_eq]904905theorem restrict_map (μ : Measure α) (s : Set β) :906 (μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=907 Measure.ext fun t ht => by simp [hf.map_apply, ht, hf.measurable ht]908909protected theorem comap_preimage (μ : Measure β) (s : Set β) :910 μ.comap f (f ⁻¹' s) = μ (s ∩ range f) := by911 rw [← hf.map_apply, hf.map_comap, restrict_apply' hf.measurableSet_range]912913lemma comap_restrict (μ : Measure β) (s : Set β) :914 (μ.restrict s).comap f = (μ.comap f).restrict (f ⁻¹' s) := by915 ext t ht916 rw [Measure.restrict_apply ht, comap_apply hf, comap_apply hf,917 Measure.restrict_apply (hf.measurableSet_image.2 ht), image_inter_preimage]918919lemma restrict_comap (μ : Measure β) (s : Set α) :920 (μ.comap f).restrict s = (μ.restrict (f '' s)).comap f := by921 rw [comap_restrict hf, preimage_image_eq _ hf.injective]922923end924925theorem _root_.MeasurableEquiv.restrict_map (e : α ≃ᵐ β) (μ : Measure α) (s : Set β) :926 (μ.map e).restrict s = (μ.restrict <| e ⁻¹' s).map e :=927 e.measurableEmbedding.restrict_map _ _928929lemma _root_.MeasurableEquiv.comap_apply (e : α ≃ᵐ β) (μ : Measure β) (s : Set α) :930 comap e μ s = μ (e.symm ⁻¹' s) := by931 rw [e.measurableEmbedding.comap_apply, e.image_eq_preimage_symm]932933end MeasurableEmbedding934935lemma MeasureTheory.Measure.map_eq_comap {_ : MeasurableSpace α} {_ : MeasurableSpace β} {f : α → β}936 {g : β → α} {μ : Measure α} (hf : Measurable f) (hg : MeasurableEmbedding g)937 (hμg : ∀ᵐ a ∂μ, a ∈ Set.range g) (hfg : ∀ a, f (g a) = a) : μ.map f = μ.comap g := by938 ext s hs939 rw [map_apply hf hs, hg.comap_apply, ← measure_sdiff_null hμg]940 congr941 simp942 grind943944section Subtype945946theorem comap_subtype_coe_apply {_m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s)947 (μ : Measure α) (t : Set s) : comap (↑) μ t = μ ((↑) '' t) :=948 (MeasurableEmbedding.subtype_coe hs).comap_apply _ _949950theorem map_comap_subtype_coe {m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s)951 (μ : Measure α) : (comap (↑) μ).map ((↑) : s → α) = μ.restrict s := by952 rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]953954theorem ae_restrict_iff_subtype {m0 : MeasurableSpace α} {μ : Measure α} {s : Set α}955 (hs : MeasurableSet s) {p : α → Prop} :956 (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ (x : s) ∂comap ((↑) : s → α) μ, p x := by957 rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).ae_map_iff]958959variable [MeasureSpace α] {s t : Set α}960961/-!962### Volume on `s : Set α`963964Note the instance is provided earlier as `Subtype.measureSpace`.965-/966attribute [local instance] Subtype.measureSpace967968theorem volume_set_coe_def (s : Set α) : (volume : Measure s) = comap ((↑) : s → α) volume :=969 rfl970971theorem MeasurableSet.map_coe_volume {s : Set α} (hs : MeasurableSet s) :972 volume.map ((↑) : s → α) = restrict volume s := by973 rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]974975theorem volume_image_subtype_coe {s : Set α} (hs : MeasurableSet s) (t : Set s) :976 volume ((↑) '' t : Set α) = volume t :=977 (comap_subtype_coe_apply hs volume t).symm978979@[simp]980theorem volume_preimage_coe (hs : NullMeasurableSet s) (ht : MeasurableSet t) :981 volume (((↑) : s → α) ⁻¹' t) = volume (t ∩ s) := by982 rw [volume_set_coe_def,983 comap_apply₀ _ _ Subtype.coe_injective984 (fun h => MeasurableSet.nullMeasurableSet_subtype_coe hs)985 (measurable_subtype_coe ht).nullMeasurableSet,986 image_preimage_eq_inter_range, Subtype.range_coe]987988end Subtype989990section Piecewise991992variable [MeasurableSpace α] {μ : Measure α} {s t : Set α} {f g : α → β}993994theorem piecewise_ae_eq_restrict [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :995 piecewise s f g =ᵐ[μ.restrict s] f := by996 rw [ae_restrict_eq hs]997 exact (piecewise_eqOn s f g).eventuallyEq.filter_mono inf_le_right998999theorem piecewise_ae_eq_restrict_compl [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :1000 piecewise s f g =ᵐ[μ.restrict sᶜ] g := by1001 rw [ae_restrict_eq hs.compl]1002 exact (piecewise_eqOn_compl s f g).eventuallyEq.filter_mono inf_le_right10031004theorem piecewise_ae_eq_of_ae_eq_set [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)]1005 (hst : s =ᵐ[μ] t) : s.piecewise f g =ᵐ[μ] t.piecewise f g :=1006 hst.mem_iff.mono fun x hx => by simp [piecewise, hx]10071008end Piecewise10091010section IndicatorFunction10111012variable [MeasurableSpace α] {μ : Measure α} {s t : Set α} {f : α → β}10131014theorem mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem [Zero β] {t : Set β}1015 (ht : (0 : β) ∈ t) (hs : MeasurableSet s) :1016 t ∈ Filter.map (s.indicator f) (ae μ) ↔ t ∈ Filter.map f (ae <| μ.restrict s) := by1017 classical1018 simp_rw [mem_map, mem_ae_iff]1019 rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]1020 simp_rw [Set.compl_union, Set.compl_inter]1021 change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 01022 simp only [ht, ← Set.compl_eq_univ_sdiff, compl_compl, if_true,1023 Set.preimage_const]1024 simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]10251026theorem mem_map_indicator_ae_iff_of_zero_notMem [Zero β] {t : Set β} (ht : (0 : β) ∉ t) :1027 t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0 := by1028 classical1029 rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]1030 change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 01031 simp only [ht, if_false, Set.compl_empty, Set.empty_sdiff, Set.inter_univ, Set.preimage_const]10321033theorem map_restrict_ae_le_map_indicator_ae [Zero β] (hs : MeasurableSet s) :1034 Filter.map f (ae <| μ.restrict s) ≤ Filter.map (s.indicator f) (ae μ) := by1035 intro t1036 by_cases ht : (0 : β) ∈ t1037 · rw [mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem ht hs]1038 exact id1039 rw [mem_map_indicator_ae_iff_of_zero_notMem ht, mem_map_restrict_ae_iff hs]1040 exact fun h => measure_mono_null (Set.inter_subset_left.trans Set.subset_union_left) h10411042variable [Zero β]10431044theorem indicator_ae_eq_restrict (hs : MeasurableSet s) : indicator s f =ᵐ[μ.restrict s] f := by1045 classical exact piecewise_ae_eq_restrict hs10461047theorem indicator_ae_eq_restrict_compl (hs : MeasurableSet s) :1048 indicator s f =ᵐ[μ.restrict sᶜ] 0 := by1049 classical exact piecewise_ae_eq_restrict_compl hs10501051theorem indicator_ae_eq_of_restrict_compl_ae_eq_zero (hs : MeasurableSet s)1052 (hf : f =ᵐ[μ.restrict sᶜ] 0) : s.indicator f =ᵐ[μ] f := by1053 rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at hf1054 filter_upwards [hf] with x hx1055 by_cases hxs : x ∈ s1056 · simp only [hxs, Set.indicator_of_mem]1057 · simp only [hx hxs, Pi.zero_apply, Set.indicator_apply_eq_zero, imp_true_iff]10581059theorem indicator_ae_eq_zero_of_restrict_ae_eq_zero (hs : MeasurableSet s)1060 (hf : f =ᵐ[μ.restrict s] 0) : s.indicator f =ᵐ[μ] 0 := by1061 rw [Filter.EventuallyEq, ae_restrict_iff' hs] at hf1062 filter_upwards [hf] with x hx1063 by_cases hxs : x ∈ s1064 · simp only [hxs, hx hxs, Set.indicator_of_mem]1065 · simp [hxs]10661067theorem indicator_ae_eq_of_ae_eq_set (hst : s =ᵐ[μ] t) : s.indicator f =ᵐ[μ] t.indicator f := by1068 classical exact piecewise_ae_eq_of_ae_eq_set hst10691070theorem indicator_meas_zero (hs : μ s = 0) : indicator s f =ᵐ[μ] 0 :=1071 indicator_empty' f ▸ indicator_ae_eq_of_ae_eq_set (ae_eq_empty.2 hs)10721073theorem ae_eq_restrict_iff_indicator_ae_eq {g : α → β} (hs : MeasurableSet s) :1074 f =ᵐ[μ.restrict s] g ↔ s.indicator f =ᵐ[μ] s.indicator g := by1075 rw [Filter.EventuallyEq, ae_restrict_iff' hs]1076 refine ⟨fun h => ?_, fun h => ?_⟩ <;> filter_upwards [h] with x hx1077 · by_cases hxs : x ∈ s1078 · simp [hxs, hx hxs]1079 · simp [hxs]1080 · intro hxs1081 simpa [hxs] using hx10821083end IndicatorFunction10841085section Sum10861087open Finset in1088/-- An upper bound on a sum of restrictions of a measure `μ`. This can be used to compare1089`∫ x ∈ X, f x ∂μ` with `∑ i, ∫ x ∈ (s i), f x ∂μ`, where `s` is a cover of `X`. -/1090lemma MeasureTheory.Measure.sum_restrict_le {_ : MeasurableSpace α}1091 {μ : Measure α} {s : ι → Set α} {M : ℕ} (hs_meas : ∀ i, MeasurableSet (s i))1092 (hs : ∀ y, {i | y ∈ s i}.encard ≤ M) :1093 Measure.sum (fun i ↦ μ.restrict (s i)) ≤ M • μ.restrict (⋃ i, s i) := by1094 classical1095 refine le_iff.mpr (fun t ht ↦ le_of_eq_of_le (sum_apply _ ht) ?_)1096 refine ENNReal.summable.tsum_le_of_sum_le (fun F ↦ ?_)1097 -- `P` is a partition of `⋃ i ∈ F, s i` indexed by `C ∈ Cs` (nonempty subsets of `F`).1098 -- `P` is a partition of `s i` when restricted to `C ∈ G i` (subsets of `F` containing `i`).1099 let P (C : Finset ι) := (⋂ i ∈ C, s i) ∩ (⋂ i ∈ (F \ C), (s i)ᶜ)1100 let Cs := F.powerset \ {∅}1101 let G (i : ι) := { C | C ∈ F.powerset ∧ i ∈ C }1102 have P_meas C : MeasurableSet (P C) :=1103 measurableSet_biInter C (fun i _ ↦ hs_meas i) |>.inter <|1104 measurableSet_biInter _ (fun i _ ↦ (hs_meas i).compl)1105 have P_cover {i : ι} (hi : i ∈ F) : s i ⊆ ⋃ C ∈ G i, P C := by1106 refine fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_1107 · exact ⟨Finset.mem_powerset.mpr (filter_subset _ F), mem_filter.mpr ⟨hi, hx⟩⟩1108 · simp_rw [P, mem_inter_iff, mem_iInter, Finset.mem_sdiff, mem_filter]; tauto1109 have iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i := by1110 intro x hx1111 simp_rw [Cs, Finset.mem_sdiff, mem_iUnion] at hx1112 have ⟨C, ⟨_, C_nonempty⟩, hxC⟩ := hx1113 have ⟨i, hi⟩ := Finset.nonempty_iff_ne_empty.mpr <| Finset.notMem_singleton.mp C_nonempty1114 exact ⟨s i, ⟨i, rfl⟩, hxC.1 (s i) ⟨i, by simp [hi]⟩⟩1115 have P_subset_s {i : ι} {C : Finset ι} (hiC : i ∈ C) : P C ⊆ s i := by1116 intro x hx1117 simp only [P, mem_inter_iff, mem_iInter] at hx1118 exact hx.1 i hiC1119 have mem_C {i} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i) : i ∈ C := by1120 rw [mem_inter_iff, mem_iInter₂, mem_iInter₂] at hx1121 exact of_not_not fun h ↦ hx.2 i (mem_sdiff.mpr ⟨hi, h⟩) hxs1122 have C_subset_C {C₁ C₂} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂) : C₁ ⊆ C₂ :=1123 fun i hi ↦ mem_C (mem_powerset.mp (sdiff_subset hC₁) hi) hx.2 <| P_subset_s hi hx.11124 calc ∑ i ∈ F, (μ.restrict (s i)) t1125 _ ≤ ∑ i ∈ F, Measure.sum (fun (C : G i) ↦ μ.restrict (P C)) t :=1126 F.sum_le_sum fun i hi ↦ (restrict_mono_set μ (P_cover hi) t).trans <|1127 restrict_biUnion_le ((finite_toSet F.powerset).subset (sep_subset _ _)).countable t1128 _ = ∑ i ∈ F, ∑' (C : G i), μ.restrict (P C) t := by simp_rw [Measure.sum_apply _ ht]1129 _ = ∑' C, ∑ i ∈ F, (G i).indicator (fun C ↦ μ.restrict (P C) t) C := by1130 rw [Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)]1131 congr with i1132 rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]1133 _ = ∑ C ∈ Cs, ∑ i ∈ F, (C : Set ι).indicator (fun _ ↦ (μ.restrict (P C)) t) i := by1134 rw [sum_eq_tsum_indicator]1135 congr with C1136 by_cases hC : C ∈ F.powerset <;> by_cases hC' : C = ∅ <;>1137 simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]1138 _ = ∑ C ∈ Cs, {a ∈ F | a ∈ C}.card • μ.restrict (P C) t := by simp [indicator]; rfl1139 _ ≤ ∑ C ∈ Cs, M • μ.restrict (P C) t := by1140 refine sum_le_sum fun C hC ↦ ?_1141 by_cases hPC : P C = ∅1142 · simp [hPC]1143 have hCM : (C : Set ι).encard ≤ M :=1144 have ⟨x, hx⟩ := Set.nonempty_iff_ne_empty.mpr hPC1145 (encard_mono (mem_iInter₂.mp hx.1)).trans (hs x)1146 exact nsmul_le_nsmul_left zero_le <| calc {a ∈ F | a ∈ C}.card1147 _ ≤ C.card := card_mono <| fun i hi ↦ (F.mem_filter.mp hi).21148 _ = (C : Set ι).ncard := (ncard_coe_finset C).symm1149 _ ≤ M := ENat.toNat_le_of_le_coe hCM1150 _ = M • (μ.restrict (⋃ C ∈ Cs, (P C)) t) := by1151 rw [← smul_sum, ← Cs.tsum_subtype, μ.restrict_biUnion_finset _ P_meas, Measure.sum_apply _ ht]1152 refine fun C₁ hC₁ C₂ hC₂ hC ↦ Set.disjoint_iff.mpr fun x hx ↦ hC <| ?_1153 exact subset_antisymm (C_subset_C hC₁ hx) (C_subset_C hC₂ (Set.inter_comm _ _ ▸ hx))1154 _ ≤ (M • μ.restrict (⋃ i, s i)) t := by1155 rw [Measure.smul_apply]1156 exact nsmul_le_nsmul_right (μ.restrict_mono_set iUnion_P t) M11571158end Sum