chore(measure_theory/measure): review API of mutually_singular (#10186)

Author: urkud

src/measure_theory/decomposition/jordan.lean

@@ -556,7 +556,7 @@ end
 lemma total_variation_mutually_singular_iff (s : signed_measure α) (μ : measure α) :
   s.total_variation ⊥ₘ μ ↔
   s.to_jordan_decomposition.pos_part ⊥ₘ μ ∧ s.to_jordan_decomposition.neg_part ⊥ₘ μ :=
-measure.mutually_singular.add_iff
+measure.mutually_singular.add_left_iff
 
 end signed_measure
 

src/measure_theory/decomposition/lebesgue.lean

@@ -288,9 +288,8 @@ begin
   { haveI := hl,
     refine (eq_singular_part ((measurable_rn_deriv μ ν).const_smul (r : ℝ≥0∞))
       (mutually_singular.smul r (have_lebesgue_decomposition_spec _ _).2.1) _).symm,
-    rw with_density_smul _ (measurable_rn_deriv _ _),
-    change _ = _ + r • _,
-    rw [← smul_add, ← have_lebesgue_decomposition_add μ ν] },
+    rw [with_density_smul _ (measurable_rn_deriv _ _), ← smul_add,
+      ← have_lebesgue_decomposition_add μ ν, ennreal.smul_def] },
   { rw [singular_part, singular_part, dif_neg hl, dif_neg, smul_zero],
     refine λ hl', hl _,
     rw ← inv_smul_smul₀ hr μ,
@@ -303,7 +302,7 @@ lemma singular_part_add (μ₁ μ₂ ν : measure α)
 begin
   refine (eq_singular_part
     ((measurable_rn_deriv μ₁ ν).add (measurable_rn_deriv μ₂ ν))
-    ((have_lebesgue_decomposition_spec _ _).2.1.add (have_lebesgue_decomposition_spec _ _).2.1)
+    ((have_lebesgue_decomposition_spec _ _).2.1.add_left (have_lebesgue_decomposition_spec _ _).2.1)
     _).symm,
   erw with_density_add (measurable_rn_deriv μ₁ ν) (measurable_rn_deriv μ₂ ν),
   conv_rhs { rw [add_assoc, add_comm (μ₂.singular_part ν), ← add_assoc, ← add_assoc] },
@@ -910,7 +909,7 @@ end
 /-- Given a signed measure `s` and a measure `μ`, `s.singular_part μ` is the signed measure
 such that `s.singular_part μ + μ.with_densityᵥ (s.rn_deriv μ) = s` and
 `s.singular_part μ` is mutually singular with respect to `μ`. -/
-def singular_part(s : signed_measure α) (μ : measure α) : signed_measure α :=
+def singular_part (s : signed_measure α) (μ : measure α) : signed_measure α :=
 (s.to_jordan_decomposition.pos_part.singular_part μ).to_signed_measure -
 (s.to_jordan_decomposition.neg_part.singular_part μ).to_signed_measure
 
@@ -955,8 +954,7 @@ begin
   rw [mutually_singular_ennreal_iff, singular_part_total_variation],
   change _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ),
   rw vector_measure.equiv_measure.right_inv μ,
-  exact measure.mutually_singular.add
-    (mutually_singular_singular_part _ _) (mutually_singular_singular_part _ _),
+  exact (mutually_singular_singular_part _ _).add_left (mutually_singular_singular_part _ _)
 end
 
 end
@@ -1024,10 +1022,10 @@ begin
   change _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) ∧
          _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
   rw [vector_measure.equiv_measure.right_inv] at htμ,
-  exact ((jordan_decomposition.mutually_singular _).symm.add
-    (htμ.1.symm.of_absolutely_continuous (with_density_absolutely_continuous _ _))).symm.add
-    ((htμ.2.symm.of_absolutely_continuous (with_density_absolutely_continuous _ _)).symm.add
-      (with_density_of_real_mutually_singular hf).symm).symm
+  exact ((jordan_decomposition.mutually_singular _).add_right
+    (htμ.1.mono_ac (refl _) (with_density_absolutely_continuous _ _))).add_left
+    ((htμ.2.symm.mono_ac (with_density_absolutely_continuous _ _) (refl _)).add_right
+    (with_density_of_real_mutually_singular hf))
 end
 
 lemma to_jordan_decomposition_eq_of_eq_add_with_density

src/measure_theory/integral/lebesgue.lean

@@ -2078,19 +2078,11 @@ begin
   set S : set α := { x | f x < 0 } with hSdef,
   have hS : measurable_set S := measurable_set_lt hf measurable_const,
   refine ⟨S, hS, _, _⟩,
-  { rw [with_density_apply _ hS, hSdef],
-    have hf0 : ∀ᵐ x ∂μ, x ∈ S → ennreal.of_real (f x) = 0,
-    { refine ae_of_all _ (λ _ hx, _),
-      rw [ennreal.of_real_eq_zero.2 (le_of_lt hx)] },
-    rw set_lintegral_congr_fun hS hf0,
-    exact lintegral_zero },
-  { rw [with_density_apply _ hS.compl, hSdef],
-    have hf0 : ∀ᵐ x ∂μ, x ∈ Sᶜ → ennreal.of_real (-f x) = 0,
-    { refine ae_of_all _ (λ x hx, _),
-      rw ennreal.of_real_eq_zero.2,
-      rwa [neg_le, neg_zero, ← not_lt] },
-    rw set_lintegral_congr_fun hS.compl hf0,
-    exact lintegral_zero },
+  { rw [with_density_apply _ hS, lintegral_eq_zero_iff hf.ennreal_of_real, eventually_eq],
+    exact (ae_restrict_mem hS).mono (λ x hx, ennreal.of_real_eq_zero.2 (le_of_lt hx)) },
+  { rw [with_density_apply _ hS.compl, lintegral_eq_zero_iff hf.neg.ennreal_of_real, eventually_eq],
+    exact (ae_restrict_mem hS.compl).mono (λ x hx, ennreal.of_real_eq_zero.2
+      (not_lt.1 $ mt neg_pos.1 hx)) },
 end
 
 lemma restrict_with_density {s : set α} (hs : measurable_set s) (f : α → ℝ≥0∞) :

src/measure_theory/measure/measure_space.lean

@@ -1213,6 +1213,9 @@ ext $ λ s hs, by simp [hs, tsum_fintype]
   (sum μ).restrict s = sum (λ i, (μ i).restrict s) :=
 ext $ λ t ht, by simp only [sum_apply, restrict_apply, ht, ht.inter hs]
 
+@[simp] lemma sum_of_empty [is_empty ι] (μ : ι → measure α) : sum μ = 0 :=
+by rw [← measure_univ_eq_zero, sum_apply _ measurable_set.univ, tsum_empty]
+
 lemma sum_congr {μ ν : ℕ → measure α} (h : ∀ n, μ n = ν n) : sum μ = sum ν :=
 by { congr, ext1 n, exact h n }
 
@@ -1339,6 +1342,8 @@ rfl.absolutely_continuous
 
 protected lemma rfl : μ ≪ μ := λ s hs, hs
 
+instance [measurable_space α] : is_refl (measure α) (≪) := ⟨λ μ, absolutely_continuous.rfl⟩
+
 @[trans] protected lemma trans (h1 : μ₁ ≪ μ₂) (h2 : μ₂ ≪ μ₃) : μ₁ ≪ μ₃ :=
 λ s hs, h1 $ h2 hs
 
@@ -1449,45 +1454,60 @@ localized "infix ` ⊥ₘ `:60 := measure_theory.measure.mutually_singular" in m
 
 namespace mutually_singular
 
-lemma zero_right : μ ⊥ₘ 0 :=
-⟨∅, measurable_set.empty, measure_empty, rfl⟩
+lemma mk {s t : set α} (hs : μ s = 0) (ht : ν t = 0) (hst : univ ⊆ s ∪ t) :
+  mutually_singular μ ν :=
+begin
+  use [to_measurable μ s, measurable_set_to_measurable _ _, (measure_to_measurable _).trans hs],
+  refine measure_mono_null (λ x hx, (hst trivial).resolve_left $ λ hxs, hx _) ht,
+  exact subset_to_measurable _ _ hxs
+end
+
+@[simp] lemma zero_right : μ ⊥ₘ 0 := ⟨∅, measurable_set.empty, measure_empty, rfl⟩
 
-lemma symm (h : ν ⊥ₘ μ) : μ ⊥ₘ ν :=
-let ⟨i, hi, his, hit⟩ := h in
-  ⟨iᶜ, measurable_set.compl hi, hit, (compl_compl i).symm ▸ his⟩
+@[symm] lemma symm (h : ν ⊥ₘ μ) : μ ⊥ₘ ν :=
+let ⟨i, hi, his, hit⟩ := h in ⟨iᶜ, hi.compl, hit, (compl_compl i).symm ▸ his⟩
 
-lemma zero_left : 0 ⊥ₘ μ :=
-zero_right.symm
+lemma comm : μ ⊥ₘ ν ↔ ν ⊥ₘ μ := ⟨λ h, h.symm, λ h, h.symm⟩
 
-lemma add (h₁ : ν₁ ⊥ₘ μ) (h₂ : ν₂ ⊥ₘ μ) : ν₁ + ν₂ ⊥ₘ μ :=
-begin
-  obtain ⟨s, hs, hs0, hs0'⟩ := h₁,
-  obtain ⟨t, ht, ht0, ht0'⟩ := h₂,
-  refine ⟨s ∩ t, hs.inter ht, _, _⟩,
-  { simp only [pi.add_apply, add_eq_zero_iff, coe_add],
-    exact ⟨measure_mono_null (inter_subset_left s t) hs0,
-           measure_mono_null (inter_subset_right s t) ht0⟩ },
-  { rw [compl_inter, ← nonpos_iff_eq_zero],
-    refine le_trans (measure_union_le _ _) _,
-    rw [hs0', ht0', zero_add],
-    exact le_refl _ }
-end
+@[simp] lemma zero_left : 0 ⊥ₘ μ := zero_right.symm
+
+lemma mono_ac (h : μ₁ ⊥ₘ ν₁) (hμ : μ₂ ≪ μ₁) (hν : ν₂ ≪ ν₁) : μ₂ ⊥ₘ ν₂ :=
+let ⟨s, hs, h₁, h₂⟩ := h in ⟨s, hs, hμ h₁, hν h₂⟩
 
-lemma add_iff : ν₁ + ν₂ ⊥ₘ μ ↔ ν₁ ⊥ₘ μ ∧ ν₂ ⊥ₘ μ :=
+lemma mono (h : μ₁ ⊥ₘ ν₁) (hμ : μ₂ ≤ μ₁) (hν : ν₂ ≤ ν₁) : μ₂ ⊥ₘ ν₂ :=
+h.mono_ac hμ.absolutely_continuous hν.absolutely_continuous
+
+@[simp] lemma sum_left {ι : Type*} [encodable ι] {μ : ι → measure α} :
+  (sum μ) ⊥ₘ ν ↔ ∀ i, μ i ⊥ₘ ν :=
 begin
-  split,
-  { rintro ⟨u, hmeas, hu₁, hu₂⟩,
-    rw [measure.add_apply, add_eq_zero_iff] at hu₁,
-    exact ⟨⟨u, hmeas, hu₁.1, hu₂⟩, u, hmeas, hu₁.2, hu₂⟩ },
-  { exact λ ⟨h₁, h₂⟩, h₁.add h₂ }
+  refine ⟨λ h i, h.mono (le_sum _ _) le_rfl, λ H, _⟩,
+  choose s hsm hsμ hsν using H,
+  refine ⟨⋂ i, s i, measurable_set.Inter hsm, _, _⟩,
+  { rw [sum_apply _ (measurable_set.Inter hsm), ennreal.tsum_eq_zero],
+    exact λ i, measure_mono_null (Inter_subset _ _) (hsμ i) },
+  { rwa [compl_Inter, measure_Union_null_iff], }
 end
 
-lemma smul (r : ℝ≥0) (h : ν ⊥ₘ μ) : r • ν ⊥ₘ μ :=
-let ⟨s, hs, hs0, hs0'⟩ := h in
-  ⟨s, hs, by simp only [coe_nnreal_smul, pi.smul_apply, hs0, smul_zero], hs0'⟩
+@[simp] lemma sum_right {ι : Type*} [encodable ι] {ν : ι → measure α} :
+  μ ⊥ₘ sum ν ↔ ∀ i, μ ⊥ₘ ν i :=
+comm.trans $ sum_left.trans $ forall_congr $ λ i, comm
+
+@[simp] lemma add_left_iff : μ₁ + μ₂ ⊥ₘ ν ↔ μ₁ ⊥ₘ ν ∧ μ₂ ⊥ₘ ν :=
+by rw [← sum_cond, sum_left, bool.forall_bool, cond, cond, and.comm]
+
+@[simp] lemma add_right_iff : μ ⊥ₘ ν₁ + ν₂ ↔ μ ⊥ₘ ν₁ ∧ μ ⊥ₘ ν₂ :=
+comm.trans $ add_left_iff.trans $ and_congr comm comm
+
+lemma add_left (h₁ : ν₁ ⊥ₘ μ) (h₂ : ν₂ ⊥ₘ μ) : ν₁ + ν₂ ⊥ₘ μ :=
+add_left_iff.2 ⟨h₁, h₂⟩
+
+lemma add_right (h₁ : μ ⊥ₘ ν₁) (h₂ : μ ⊥ₘ ν₂) : μ ⊥ₘ ν₁ + ν₂ :=
+add_right_iff.2 ⟨h₁, h₂⟩
+
+lemma smul (r : ℝ≥0∞) (h : ν ⊥ₘ μ) : r • ν ⊥ₘ μ :=
+h.mono_ac (absolutely_continuous.rfl.smul r) absolutely_continuous.rfl
 
-lemma of_absolutely_continuous (hms : ν₂ ⊥ₘ μ) (hac : ν₁ ≪ ν₂) : ν₁ ⊥ₘ μ :=
-let ⟨u, hmeas, hu₁, hu₂⟩ := hms in ⟨u, hmeas, hac hu₁, hu₂⟩
+lemma smul_nnreal (r : ℝ≥0) (h : ν ⊥ₘ μ) : r • ν ⊥ₘ μ := h.smul r
 
 end mutually_singular
 

src/topology/instances/ennreal.lean

@@ -615,6 +615,9 @@ end
 protected lemma le_tsum (a : α) : f a ≤ ∑'a, f a :=
 le_tsum' ennreal.summable a
 
+@[simp] protected lemma tsum_eq_zero : ∑' i, f i = 0 ↔ ∀ i, f i = 0 :=
+⟨λ h i, nonpos_iff_eq_zero.1 $ h ▸ ennreal.le_tsum i, λ h, by simp [h]⟩
+
 protected lemma tsum_eq_top_of_eq_top : (∃ a, f a = ∞) → ∑' a, f a = ∞
 | ⟨a, ha⟩ := top_unique $ ha ▸ ennreal.le_tsum a