remove lemmas merged to mathlib; refactor absolutelyContinous_compProd

TestingLowerBounds/SoonInMathlib/RadonNikodym.lean

@@ -402,70 +402,7 @@ lemma rnDeriv_measure_compProd_right' (μ : Measure α) (κ η : kernel α γ)
   filter_upwards [ha, h a] with b hb1 hb2
   rw [hb1, hb2]
 
-lemma Measure.absolutelyContinuous_compProd_left_iff
-    {μ ν : Measure α} {κ : kernel α γ}
-    [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsMarkovKernel κ]  :
-    μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν := by
-  refine ⟨fun h ↦ ?_, fun h ↦ Measure.absolutelyContinuous_compProd_left h _⟩
-  refine Measure.AbsolutelyContinuous.mk (fun s hs hs0 ↦ ?_)
-  have h1 : (ν ⊗ₘ κ) (s ×ˢ univ) = 0 := by
-    rw [Measure.compProd_apply_prod hs MeasurableSet.univ]
-    exact set_lintegral_measure_zero _ _ hs0
-  have h2 := h h1
-  rw [Measure.compProd_apply_prod hs MeasurableSet.univ] at h2
-  simpa using h2
-
-lemma Measure.absolutelyContinuous_add_left_iff (μ₁ μ₂ ν : Measure α) :
-    μ₁ + μ₂ ≪ ν ↔ μ₁ ≪ ν ∧ μ₂ ≪ ν := by
-  refine ⟨fun h ↦ ?_, fun h ↦ (h.1.add h.2).trans ?_⟩
-  · constructor
-    · intro s hs0
-      specialize h hs0
-      simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] at h
-      exact h.1
-    · intro s hs0
-      specialize h hs0
-      simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] at h
-      exact h.2
-  · refine Measure.absolutelyContinuous_of_le_smul (c := 2) (le_of_eq ?_)
-    ext
-    simp only [Measure.add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply,
-      Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, smul_eq_mul]
-    rw [two_mul]
-
-lemma eq_zero_of_absolutelyContinuous_of_mutuallySingular {μ η : Measure α}
-    (h_ac : μ ≪ η) (h_ms : μ ⟂ₘ η) :
-    μ = 0 := by
-  let s := h_ms.nullSet
-  suffices μ s = 0 ∧ μ sᶜ = 0 by
-    suffices μ univ = 0 by
-      rwa [Measure.measure_univ_eq_zero] at this
-    rw [← union_compl_self s, measure_union disjoint_compl_right h_ms.measurableSet_nullSet.compl,
-      this.1, this.2, add_zero]
-  exact ⟨h_ms.measure_nullSet, h_ac h_ms.measure_compl_nullSet⟩
-
-lemma Measure.absolutelyContinuous_compProd_right_iff
-    {μ : Measure α} {κ η : kernel α γ}
-    [SFinite μ] [IsFiniteKernel κ] [IsFiniteKernel η] :
-    μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a := by
-  refine ⟨fun h ↦ ?_, fun h ↦ Measure.absolutelyContinuous_compProd_right _ h⟩
-  suffices ∀ᵐ a ∂μ, kernel.singularPart κ η a = 0 by
-    filter_upwards [this] with a ha
-    rwa [singularPart_eq_zero_iff_absolutelyContinuous] at ha
-  rw [← rnDeriv_add_singularPart κ η, Measure.compProd_add_right,
-    Measure.absolutelyContinuous_add_left_iff] at h
-  have : μ ⊗ₘ singularPart κ η ⟂ₘ μ ⊗ₘ η :=
-    Measure.mutuallySingular_compProd_right μ μ (mutuallySingular_singularPart _ _)
-  have h_zero : μ ⊗ₘ singularPart κ η = 0 :=
-    eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
-  simp_rw [← Measure.measure_univ_eq_zero]
-  refine (lintegral_eq_zero_iff (kernel.measurable_coe _ MeasurableSet.univ)).mp ?_
-  rw [← set_lintegral_univ, ← Measure.compProd_apply_prod MeasurableSet.univ MeasurableSet.univ,
-    h_zero]
-  simp
-
-lemma Measure.absolutelyContinuous_of_absolutelyContinuous_compProd
-    {μ ν : Measure α} {κ η : kernel α γ}
+lemma Measure.absolutelyContinuous_of_compProd {μ ν : Measure α} {κ η : kernel α γ}
     [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η] [h_zero : ∀ a, NeZero (κ a)]
     (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
     μ ≪ ν := by
@@ -483,27 +420,46 @@ lemma Measure.absolutelyContinuous_of_absolutelyContinuous_compProd
   simp only [Measure.measure_univ_eq_zero]
   exact (h_zero a).out
 
-lemma Measure.absolutelyContinuous_compProd_iff
-    {μ ν : Measure α} {κ η : kernel α γ}
-    [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η] [h_zero : ∀ a, NeZero (κ a)] :
-    μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a := by
-  refine ⟨fun h ↦ ⟨Measure.absolutelyContinuous_of_absolutelyContinuous_compProd h, ?_⟩,
-    fun h ↦ Measure.absolutelyContinuous_compProd h.1 h.2⟩
+lemma Measure.absolutelyContinuous_kernel_of_compProd {μ ν : Measure α} {κ η : kernel α γ}
+    [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η]
+    (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) :
+    ∀ᵐ a ∂μ, κ a ≪ η a := by
   suffices ∀ᵐ a ∂μ, kernel.singularPart κ η a = 0 by
     filter_upwards [this] with a ha
     rwa [singularPart_eq_zero_iff_absolutelyContinuous] at ha
   rw [← rnDeriv_add_singularPart κ η, Measure.compProd_add_right,
-    Measure.absolutelyContinuous_add_left_iff] at h
+    Measure.AbsolutelyContinuous.add_left_iff] at h
   have : μ ⊗ₘ singularPart κ η ⟂ₘ ν ⊗ₘ η :=
     Measure.mutuallySingular_compProd_right μ ν (mutuallySingular_singularPart _ _)
   have h_zero : μ ⊗ₘ singularPart κ η = 0 :=
-    eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
+    Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this
   simp_rw [← Measure.measure_univ_eq_zero]
   refine (lintegral_eq_zero_iff (kernel.measurable_coe _ MeasurableSet.univ)).mp ?_
   rw [← set_lintegral_univ, ← Measure.compProd_apply_prod MeasurableSet.univ MeasurableSet.univ,
     h_zero]
   simp
 
+lemma Measure.absolutelyContinuous_compProd_iff
+    {μ ν : Measure α} {κ η : kernel α γ}
+    [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η] [∀ a, NeZero (κ a)] :
+    μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a :=
+  ⟨fun h ↦ ⟨Measure.absolutelyContinuous_of_compProd h,
+      absolutelyContinuous_kernel_of_compProd h⟩,
+    fun h ↦ Measure.absolutelyContinuous_compProd h.1 h.2⟩
+
+lemma Measure.absolutelyContinuous_compProd_left_iff
+    {μ ν : Measure α} {κ : kernel α γ}
+    [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [h_zero : ∀ a, NeZero (κ a)] :
+    μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν := by
+  rw [Measure.absolutelyContinuous_compProd_iff]
+  simp only [and_iff_left_iff_imp]
+  exact fun _ ↦ ae_of_all _ (fun _ ↦ Measure.AbsolutelyContinuous.rfl)
+
+lemma Measure.absolutelyContinuous_compProd_right_iff
+    {μ : Measure α} {κ η : kernel α γ} [SFinite μ] [IsFiniteKernel κ] [IsFiniteKernel η] :
+    μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a :=
+  ⟨absolutelyContinuous_kernel_of_compProd, Measure.absolutelyContinuous_compProd_right _⟩
+
 end MeasureCompProd
 
 end ProbabilityTheory.kernel