|
| 1 | +/- |
| 2 | +Copyright (c) 2017 Johannes Hölzl. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Johannes Hölzl, Mario Carneiro |
| 5 | +-/ |
| 6 | +import Mathlib.MeasureTheory.Measure.Map |
| 7 | + |
| 8 | +/-! |
| 9 | +# Absolute Continuity of Measures |
| 10 | +
|
| 11 | +We say that `μ` is absolutely continuous with respect to `ν`, or that `μ` is dominated by `ν`, |
| 12 | +if `ν(A) = 0` implies that `μ(A) = 0`. We denote that by `μ ≪ ν`. |
| 13 | +
|
| 14 | +It is equivalent to an inequality of the almost everywhere filters of the measures: |
| 15 | +`μ ≪ ν ↔ ae μ ≤ ae ν`. |
| 16 | +
|
| 17 | +## Main definitions |
| 18 | +
|
| 19 | +* `MeasureTheory.Measure.AbsolutelyContinuous μ ν`: `μ` is absolutely continuous with respect to `ν` |
| 20 | +
|
| 21 | +## Main statements |
| 22 | +
|
| 23 | +* `ae_le_iff_absolutelyContinuous`: `ae μ ≤ ae ν ↔ μ ≪ ν` |
| 24 | +
|
| 25 | +## Notation |
| 26 | +
|
| 27 | +* `μ ≪ ν`: `MeasureTheory.Measure.AbsolutelyContinuous μ ν`. That is: `μ` is absolutely continuous |
| 28 | + with respect to `ν` |
| 29 | +
|
| 30 | +-/ |
| 31 | + |
| 32 | +variable {α β δ ι R : Type*} |
| 33 | + |
| 34 | +namespace MeasureTheory |
| 35 | + |
| 36 | +open Set ENNReal NNReal |
| 37 | + |
| 38 | +variable {mα : MeasurableSpace α} {mβ : MeasurableSpace β} |
| 39 | + {μ μ₁ μ₂ μ₃ ν ν' : Measure α} {s t : Set α} |
| 40 | + |
| 41 | +namespace Measure |
| 42 | + |
| 43 | +/-- We say that `μ` is absolutely continuous with respect to `ν`, or that `μ` is dominated by `ν`, |
| 44 | + if `ν(A) = 0` implies that `μ(A) = 0`. -/ |
| 45 | +def AbsolutelyContinuous {_m0 : MeasurableSpace α} (μ ν : Measure α) : Prop := |
| 46 | + ∀ ⦃s : Set α⦄, ν s = 0 → μ s = 0 |
| 47 | + |
| 48 | +@[inherit_doc MeasureTheory.Measure.AbsolutelyContinuous] |
| 49 | +scoped[MeasureTheory] infixl:50 " ≪ " => MeasureTheory.Measure.AbsolutelyContinuous |
| 50 | + |
| 51 | +theorem absolutelyContinuous_of_le (h : μ ≤ ν) : μ ≪ ν := fun s hs => |
| 52 | + nonpos_iff_eq_zero.1 <| hs ▸ le_iff'.1 h s |
| 53 | + |
| 54 | +alias _root_.LE.le.absolutelyContinuous := absolutelyContinuous_of_le |
| 55 | + |
| 56 | +theorem absolutelyContinuous_of_eq (h : μ = ν) : μ ≪ ν := |
| 57 | + h.le.absolutelyContinuous |
| 58 | + |
| 59 | +alias _root_.Eq.absolutelyContinuous := absolutelyContinuous_of_eq |
| 60 | + |
| 61 | +namespace AbsolutelyContinuous |
| 62 | + |
| 63 | +theorem mk (h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0) : μ ≪ ν := by |
| 64 | + intro s hs |
| 65 | + rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩ |
| 66 | + exact measure_mono_null h1t (h h2t h3t) |
| 67 | + |
| 68 | +@[refl] |
| 69 | +protected theorem refl {_m0 : MeasurableSpace α} (μ : Measure α) : μ ≪ μ := |
| 70 | + rfl.absolutelyContinuous |
| 71 | + |
| 72 | +protected theorem rfl : μ ≪ μ := fun _s hs => hs |
| 73 | + |
| 74 | +instance instIsRefl {_ : MeasurableSpace α} : IsRefl (Measure α) (· ≪ ·) := |
| 75 | + ⟨fun _ => AbsolutelyContinuous.rfl⟩ |
| 76 | + |
| 77 | +@[simp] |
| 78 | +protected lemma zero (μ : Measure α) : 0 ≪ μ := fun _ _ ↦ by simp |
| 79 | + |
| 80 | +@[trans] |
| 81 | +protected theorem trans (h1 : μ₁ ≪ μ₂) (h2 : μ₂ ≪ μ₃) : μ₁ ≪ μ₃ := fun _s hs => h1 <| h2 hs |
| 82 | + |
| 83 | +@[mono] |
| 84 | +protected theorem map (h : μ ≪ ν) {f : α → β} (hf : Measurable f) : μ.map f ≪ ν.map f := |
| 85 | + AbsolutelyContinuous.mk fun s hs => by simpa [hf, hs] using @h _ |
| 86 | + |
| 87 | +protected theorem smul_left [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : μ ≪ ν) (c : R) : |
| 88 | + c • μ ≪ ν := fun s hνs => by |
| 89 | + simp only [h hνs, smul_apply, smul_zero, ← smul_one_smul ℝ≥0∞ c (0 : ℝ≥0∞)] |
| 90 | + |
| 91 | +/-- If `μ ≪ ν`, then `c • μ ≪ c • ν`. |
| 92 | +
|
| 93 | +Earlier, this name was used for what's now called `AbsolutelyContinuous.smul_left`. -/ |
| 94 | +protected theorem smul [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : μ ≪ ν) (c : R) : |
| 95 | + c • μ ≪ c • ν := by |
| 96 | + intro s hνs |
| 97 | + rw [smul_apply, ← smul_one_smul ℝ≥0∞, smul_eq_mul, mul_eq_zero] at hνs ⊢ |
| 98 | + exact hνs.imp_right fun hs ↦ h hs |
| 99 | + |
| 100 | +@[deprecated (since := "2024-11-14")] protected alias smul_both := AbsolutelyContinuous.smul |
| 101 | + |
| 102 | +protected lemma add (h1 : μ₁ ≪ ν) (h2 : μ₂ ≪ ν') : μ₁ + μ₂ ≪ ν + ν' := by |
| 103 | + intro s hs |
| 104 | + simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢ |
| 105 | + exact ⟨h1 hs.1, h2 hs.2⟩ |
| 106 | + |
| 107 | +lemma add_left_iff {μ₁ μ₂ ν : Measure α} : |
| 108 | + μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν := by |
| 109 | + refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩ |
| 110 | + · have : ∀ s, ν s = 0 → μ₁ s = 0 ∧ μ₂ s = 0 := by intro s hs0; simpa using h hs0 |
| 111 | + exact ⟨fun s hs0 ↦ (this s hs0).1, fun s hs0 ↦ (this s hs0).2⟩ |
| 112 | + · rw [← two_smul ℝ≥0] |
| 113 | + exact AbsolutelyContinuous.rfl.smul_left 2 |
| 114 | + |
| 115 | +lemma add_left {μ₁ μ₂ ν : Measure α} (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ≪ ν) : μ₁ + μ₂ ≪ ν := |
| 116 | + Measure.AbsolutelyContinuous.add_left_iff.mpr ⟨h₁, h₂⟩ |
| 117 | + |
| 118 | +lemma add_right (h1 : μ ≪ ν) (ν' : Measure α) : μ ≪ ν + ν' := by |
| 119 | + intro s hs |
| 120 | + simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢ |
| 121 | + exact h1 hs.1 |
| 122 | + |
| 123 | +end AbsolutelyContinuous |
| 124 | + |
| 125 | +@[simp] |
| 126 | +lemma absolutelyContinuous_zero_iff : μ ≪ 0 ↔ μ = 0 := |
| 127 | + ⟨fun h ↦ measure_univ_eq_zero.mp (h rfl), fun h ↦ h.symm ▸ AbsolutelyContinuous.zero _⟩ |
| 128 | + |
| 129 | +alias absolutelyContinuous_refl := AbsolutelyContinuous.refl |
| 130 | +alias absolutelyContinuous_rfl := AbsolutelyContinuous.rfl |
| 131 | + |
| 132 | +lemma absolutelyContinuous_sum_left {μs : ι → Measure α} (hμs : ∀ i, μs i ≪ ν) : |
| 133 | + Measure.sum μs ≪ ν := |
| 134 | + AbsolutelyContinuous.mk fun s hs hs0 ↦ by simp [sum_apply _ hs, fun i ↦ hμs i hs0] |
| 135 | + |
| 136 | +lemma absolutelyContinuous_sum_right {μs : ι → Measure α} (i : ι) (hνμ : ν ≪ μs i) : |
| 137 | + ν ≪ Measure.sum μs := by |
| 138 | + refine AbsolutelyContinuous.mk fun s hs hs0 ↦ ?_ |
| 139 | + simp only [sum_apply _ hs, ENNReal.tsum_eq_zero] at hs0 |
| 140 | + exact hνμ (hs0 i) |
| 141 | + |
| 142 | +lemma smul_absolutelyContinuous {c : ℝ≥0∞} : c • μ ≪ μ := .smul_left .rfl _ |
| 143 | + |
| 144 | +theorem absolutelyContinuous_of_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hμ'_le : μ' ≤ c • μ) : |
| 145 | + μ' ≪ μ := |
| 146 | + (Measure.absolutelyContinuous_of_le hμ'_le).trans smul_absolutelyContinuous |
| 147 | + |
| 148 | +lemma absolutelyContinuous_smul {c : ℝ≥0∞} (hc : c ≠ 0) : μ ≪ c • μ := by |
| 149 | + simp [AbsolutelyContinuous, hc] |
| 150 | + |
| 151 | +theorem ae_le_iff_absolutelyContinuous : ae μ ≤ ae ν ↔ μ ≪ ν := |
| 152 | + ⟨fun h s => by |
| 153 | + rw [measure_zero_iff_ae_nmem, measure_zero_iff_ae_nmem] |
| 154 | + exact fun hs => h hs, fun h _ hs => h hs⟩ |
| 155 | + |
| 156 | +alias ⟨_root_.LE.le.absolutelyContinuous_of_ae, AbsolutelyContinuous.ae_le⟩ := |
| 157 | + ae_le_iff_absolutelyContinuous |
| 158 | + |
| 159 | +alias ae_mono' := AbsolutelyContinuous.ae_le |
| 160 | + |
| 161 | +theorem AbsolutelyContinuous.ae_eq (h : μ ≪ ν) {f g : α → δ} (h' : f =ᵐ[ν] g) : f =ᵐ[μ] g := |
| 162 | + h.ae_le h' |
| 163 | + |
| 164 | +end Measure |
| 165 | + |
| 166 | +protected theorem AEDisjoint.of_absolutelyContinuous |
| 167 | + (h : AEDisjoint μ s t) {ν : Measure α} (h' : ν ≪ μ) : |
| 168 | + AEDisjoint ν s t := h' h |
| 169 | + |
| 170 | +protected theorem AEDisjoint.of_le |
| 171 | + (h : AEDisjoint μ s t) {ν : Measure α} (h' : ν ≤ μ) : |
| 172 | + AEDisjoint ν s t := |
| 173 | + h.of_absolutelyContinuous (Measure.absolutelyContinuous_of_le h') |
| 174 | + |
| 175 | +@[mono] |
| 176 | +theorem ae_mono (h : μ ≤ ν) : ae μ ≤ ae ν := |
| 177 | + h.absolutelyContinuous.ae_le |
| 178 | + |
| 179 | +end MeasureTheory |
| 180 | + |
| 181 | +namespace MeasurableEmbedding |
| 182 | + |
| 183 | +open MeasureTheory Measure |
| 184 | + |
| 185 | +variable {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β} {μ ν : Measure α} |
| 186 | + |
| 187 | +lemma absolutelyContinuous_map (hf : MeasurableEmbedding f) (hμν : μ ≪ ν) : |
| 188 | + μ.map f ≪ ν.map f := by |
| 189 | + intro t ht |
| 190 | + rw [hf.map_apply] at ht ⊢ |
| 191 | + exact hμν ht |
| 192 | + |
| 193 | +end MeasurableEmbedding |
0 commit comments