feat(measure_theory): Absolute continuity (#5948)

* Define absolute continuity between measures (@mzinkevi)
* State monotonicity of `ae_measurable` w.r.t. absolute continuity
* Weaken some `measurable` assumptions in `prod.lean` to `ae_measurable`
* Some docstring fixes
* Some cleanup

src/measure_theory/borel_space.lean

@@ -671,7 +671,7 @@ begin
   rw [‹borel_space α›.measurable_eq, borel_eq_generate_Ioi α],
   apply measurable_generate_from,
   rintro _ ⟨a, rfl⟩,
-  simp only [set.preimage, mem_Ioi, lt_is_lub_iff (hg _), exists_range_iff, set_of_exists],
+  simp_rw [set.preimage, mem_Ioi, lt_is_lub_iff (hg _), exists_range_iff, set_of_exists],
   exact is_measurable.Union (λ i, hf i (is_open_lt' _).is_measurable)
 end
 
@@ -728,7 +728,7 @@ begin
   rw [‹borel_space α›.measurable_eq, borel_eq_generate_Iio α],
   apply measurable_generate_from,
   rintro _ ⟨a, rfl⟩,
-  simp only [set.preimage, mem_Iio, is_glb_lt_iff (hg _), exists_range_iff, set_of_exists],
+  simp_rw [set.preimage, mem_Iio, is_glb_lt_iff (hg _), exists_range_iff, set_of_exists],
   exact is_measurable.Union (λ i, hf i (is_open_gt' _).is_measurable)
 end
 
@@ -1273,9 +1273,9 @@ begin
   { refine measurable_of_tendsto_nnreal' u (λ i, (hf i).inf_nndist) _ hu hs, swap,
     rw [tendsto_pi], rw [tendsto_pi] at lim, intro x,
     exact ((continuous_inf_nndist_pt s).tendsto (g x)).comp (lim x) },
-    have h4s : g ⁻¹' s = (λ x, inf_nndist (g x) s) ⁻¹' {0},
-    { ext x, simp [h1s, ← mem_iff_inf_dist_zero_of_closed h1s h2s, ← nnreal.coe_eq_zero] },
-    rw [h4s], exact this (is_measurable_singleton 0),
+  have h4s : g ⁻¹' s = (λ x, inf_nndist (g x) s) ⁻¹' {0},
+  { ext x, simp [h1s, ← mem_iff_inf_dist_zero_of_closed h1s h2s, ← nnreal.coe_eq_zero] },
+  rw [h4s], exact this (is_measurable_singleton 0),
 end
 
 /-- A sequential limit of measurable functions valued in a metric space is measurable. -/

src/measure_theory/group.lean

@@ -81,7 +81,7 @@ variables [group G] [topological_space G] [topological_group G] [borel_space G]
 @[to_additive]
 lemma inv_apply (μ : measure G) {s : set G} (hs : is_measurable s) :
   μ.inv s = μ s⁻¹ :=
-by { unfold measure.inv, rw [measure.map_apply measurable_inv hs, inv_preimage] }
+measure.map_apply measurable_inv hs
 
 @[simp, to_additive] protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
 begin

src/measure_theory/haar_measure.lean

@@ -178,7 +178,7 @@ lemma index_union_eq (K₁ K₂ : compacts G) {V : set G} (hV : (interior V).non
 begin
   apply le_antisymm (index_union_le K₁ K₂ hV),
   rcases index_elim (K₁.2.union K₂.2) hV with ⟨s, h1s, h2s⟩, rw [← h2s],
-  have : ∀(K : set G) , K ⊆ (⋃ g ∈ s, (λ h, g * h) ⁻¹' V) →
+  have : ∀ (K : set G) , K ⊆ (⋃ g ∈ s, (λ h, g * h) ⁻¹' V) →
     index K V ≤ (s.filter (λ g, ((λ (h : G), g * h) ⁻¹' V ∩ K).nonempty)).card,
   { intros K hK, apply nat.Inf_le, refine ⟨_, _, rfl⟩, rw [mem_set_of_eq],
     intros g hg, rcases hK hg with ⟨_, ⟨g₀, rfl⟩, _, ⟨h1g₀, rfl⟩, h2g₀⟩,
@@ -285,18 +285,24 @@ begin
   have h2V₀ : (1 : G) ∈ V₀, { simp only [mem_Inter], rintro ⟨V, hV⟩ h2V, exact hV.2 },
   refine ⟨prehaar K₀.1 V₀, _⟩,
   split,
-  { apply prehaar_mem_haar_product K₀, use 1, rwa h1V₀.interior_eq  },
+  { apply prehaar_mem_haar_product K₀, use 1, rwa h1V₀.interior_eq },
   { simp only [mem_Inter], rintro ⟨V, hV⟩ h2V, apply subset_closure,
     apply mem_image_of_mem, rw [mem_set_of_eq],
     exact ⟨subset.trans (Inter_subset _ ⟨V, hV⟩) (Inter_subset _ h2V), h1V₀, h2V₀⟩ },
 end
 
 /-!
-### The Haar measure on compact sets
+### Lemmas about `chaar`
 -/
 
-/-- The Haar measure on compact sets, defined to be an arbitrary element in the intersection of
-  all the sets `cl_prehaar K₀ V` in `haar_product K₀`. -/
+/-- This is the "limit" of `prehaar K₀.1 U K` as `U` becomes a smaller and smaller open
+  neighborhood of `(1 : G)`. More precisely, it is defined to be an arbitrary element
+  in the intersection of all the sets `cl_prehaar K₀ V` in `haar_product K₀`.
+  This is roughly equal to the Haar measure on compact sets,
+  but it can differ slightly. We do know that
+  `haar_measure K₀ (interior K.1) ≤ chaar K₀ K ≤ haar_measure K₀ K.1`.
+  These inequalities are given by `measure_theory.measure.haar_outer_measure_le_echaar` and
+  `measure_theory.measure.echaar_le_haar_outer_measure`. -/
 def chaar (K₀ : positive_compacts G) (K : compacts G) : ℝ :=
 classical.some (nonempty_Inter_cl_prehaar K₀) K
 
@@ -313,7 +319,8 @@ by { have := chaar_mem_haar_product K₀ K (mem_univ _), rw mem_Icc at this, exa
 
 lemma chaar_empty (K₀ : positive_compacts G) : chaar K₀ ⊥ = 0 :=
 begin
-  let eval : (compacts G → ℝ) → ℝ := λ f, f ⊥, have : continuous eval := continuous_apply ⊥,
+  let eval : (compacts G → ℝ) → ℝ := λ f, f ⊥,
+  have : continuous eval := continuous_apply ⊥,
   show chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)},
   apply mem_of_subset_of_mem _ (chaar_mem_cl_prehaar K₀ ⟨set.univ, is_open_univ, mem_univ _⟩),
   unfold cl_prehaar, rw is_closed.closure_subset_iff,

src/measure_theory/integration.lean

@@ -1298,9 +1298,9 @@ by simp_rw [mul_comm, lintegral_const_mul' r f hr]
 /- A double integral of a product where each factor contains only one variable
   is a product of integrals -/
 lemma lintegral_lintegral_mul {β} [measurable_space β] {ν : measure β}
-  {f : α → ennreal} {g : β → ennreal} (hf : measurable f) (hg : measurable g) :
+  {f : α → ennreal} {g : β → ennreal} (hf : ae_measurable f μ) (hg : ae_measurable g ν) :
   ∫⁻ x, ∫⁻ y, f x * g y ∂ν ∂μ = ∫⁻ x, f x ∂μ * ∫⁻ y, g y ∂ν :=
-by simp [lintegral_const_mul _ hg, lintegral_mul_const _ hf]
+by simp [lintegral_const_mul'' _ hg, lintegral_mul_const'' _ hf]
 
 -- TODO: Need a better way of rewriting inside of a integral
 lemma lintegral_rw₁ {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ennreal) :

src/measure_theory/measure_space.lean

@@ -202,7 +202,7 @@ lemma exists_is_measurable_superset (μ : measure α) (s : set α) :
 by simpa only [← measure_eq_trim] using μ.to_outer_measure.exists_is_measurable_superset_eq_trim s
 
 /-- A measurable set `t ⊇ s` such that `μ t = μ s`. -/
-def to_measurable (μ : measure α) (s : set α) :=
+def to_measurable (μ : measure α) (s : set α) : set α :=
 classical.some (exists_is_measurable_superset μ s)
 
 lemma subset_to_measurable (μ : measure α) (s : set α) : s ⊆ to_measurable μ s :=
@@ -526,7 +526,7 @@ measure.ext $ λ s, μ.to_outer_measure.trim_eq
 end outer_measure
 
 variables [measurable_space α] [measurable_space β] [measurable_space γ]
-variables {μ μ₁ μ₂ ν ν' ν₁ ν₂ : measure α} {s s' t : set α}
+variables {μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : measure α} {s s' t : set α}
 
 namespace measure
 
@@ -739,6 +739,11 @@ begin
   exact map_apply hf ht
 end
 
+/-- Even if `s` is not measurable, `map f μ s = 0` implies that `μ (f ⁻¹' s) = 0`. -/
+lemma preimage_null_of_map_null {f : α → β} (hf : measurable f) {s : set β}
+  (hs : map f μ s = 0) : μ (f ⁻¹' s) = 0 :=
+nonpos_iff_eq_zero.mp $ (le_map_apply hf s).trans_eq hs
+
 /-- Pullback of a `measure`. If `f` sends each `measurable` set to a `measurable` set, then for each
 measurable set `s` we have `comap f μ s = μ (f '' s)`. -/
 def comap (f : α → β) : measure β →ₗ[ennreal] measure α :=
@@ -1194,6 +1199,34 @@ calc count s < ⊤ ↔ count s ≠ ⊤ : lt_top_iff_ne_top
              ... ↔ ¬s.infinite : not_congr count_apply_eq_top
              ... ↔ s.finite    : not_not
 
+/-! ### Absolute continuity -/
+
+/-- We say that `μ` is absolutely continuous with respect to `ν`, or that `μ` is dominated by `ν`,
+  if `ν(A) = 0` implies that `μ(A) = 0`. -/
+def absolutely_continuous (μ ν : measure α) : Prop :=
+∀ ⦃s : set α⦄, ν s = 0 → μ s = 0
+
+infix ` ≪ `:50 := absolutely_continuous
+
+lemma absolutely_continuous.mk (h : ∀ ⦃s : set α⦄, is_measurable s → ν s = 0 → μ s = 0) : μ ≪ ν :=
+begin
+  intros s hs,
+  rcases exists_is_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩,
+  exact measure_mono_null h1t (h h2t h3t),
+end
+
+@[refl] lemma absolutely_continuous.refl (μ : measure α) : μ ≪ μ := λ s hs, hs
+
+lemma absolutely_continuous.rfl : μ ≪ μ := λ s hs, hs
+
+lemma absolutely_continuous_of_eq (h : μ = ν) : μ ≪ ν := by rw h
+
+alias absolutely_continuous_of_eq ← eq.absolutely_continuous
+
+@[trans] lemma absolutely_continuous.trans (h1 : μ₁ ≪ μ₂) (h2 : μ₂ ≪ μ₃) : μ₁ ≪ μ₃ :=
+λ s hs, h1 $ h2 hs
+
+
 /-! ### The almost everywhere filter -/
 
 /-- The “almost everywhere” filter of co-null sets. -/
@@ -1334,14 +1367,13 @@ by simp [ae_iff, hc]
 lemma ae_add_measure_iff {p : α → Prop} {ν} : (∀ᵐ x ∂μ + ν, p x) ↔ (∀ᵐ x ∂μ, p x) ∧ ∀ᵐ x ∂ν, p x :=
 add_eq_zero_iff
 
+lemma ae_eq_comp' {ν : measure β} {f : α → β} {g g' : β → δ} (hf : measurable f)
+  (h : g =ᵐ[ν] g') (h2 : map f μ ≪ ν) : g ∘ f =ᵐ[μ] g' ∘ f :=
+preimage_null_of_map_null hf $ h2 h
+
 lemma ae_eq_comp {f : α → β} {g g' : β → δ} (hf : measurable f)
   (h : g =ᵐ[measure.map f μ] g') : g ∘ f =ᵐ[μ] g' ∘ f :=
-begin
-  rcases exists_is_measurable_superset_of_null h with ⟨t, ht, tmeas, tzero⟩,
-  refine le_antisymm _ bot_le,
-  calc μ {x | g (f x) ≠ g' (f x)} ≤ μ (f⁻¹' t) : measure_mono (λ x hx, ht hx)
-  ... = 0 : by rwa ← measure.map_apply hf tmeas
-end
+ae_eq_comp' hf h absolutely_continuous.rfl
 
 lemma le_ae_restrict : μ.ae ⊓ 𝓟 s ≤ (μ.restrict s).ae :=
 λ s hs, eventually_inf_principal.2 (ae_imp_of_ae_restrict hs)
@@ -2238,6 +2270,9 @@ lemma mono_set {s t} (h : s ⊆ t) (ht : ae_measurable f (μ.restrict t)) :
   ae_measurable f (μ.restrict s) :=
 ht.mono_measure (restrict_mono h le_rfl)
 
+protected lemma mono' (h : ae_measurable f μ) (h' : ν ≪ μ) : ae_measurable f ν :=
+⟨h.mk f, h.measurable_mk, h' h.ae_eq_mk⟩
+
 lemma ae_mem_imp_eq_mk {s} (h : ae_measurable f (μ.restrict s)) :
   ∀ᵐ x ∂μ, x ∈ s → f x = h.mk f x :=
 ae_imp_of_ae_restrict h.ae_eq_mk
@@ -2279,8 +2314,12 @@ lemma smul_measure (h : ae_measurable f μ) (c : ennreal) :
 ⟨h.mk f, h.measurable_mk, ae_smul_measure h.ae_eq_mk c⟩
 
 lemma comp_measurable [measurable_space δ] {f : α → δ} {g : δ → β}
-  (hg : ae_measurable g (measure.map f μ)) (hf : measurable f) : ae_measurable (g ∘ f) μ :=
-⟨(hg.mk g) ∘ f, hg.measurable_mk.comp hf, ae_eq_comp hf hg.ae_eq_mk⟩
+  (hg : ae_measurable g (map f μ)) (hf : measurable f) : ae_measurable (g ∘ f) μ :=
+⟨hg.mk g ∘ f, hg.measurable_mk.comp hf, ae_eq_comp hf hg.ae_eq_mk⟩
+
+lemma comp_measurable' {δ} [measurable_space δ] {ν : measure δ} {f : α → δ} {g : δ → β}
+  (hg : ae_measurable g ν) (hf : measurable f) (h : map f μ ≪ ν) : ae_measurable (g ∘ f) μ :=
+(hg.mono' h).comp_measurable hf
 
 lemma prod_mk {γ : Type*} [measurable_space γ] {f : α → β} {g : α → γ}
   (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ x, (f x, g x)) μ :=