prove Kernel.measurableSet_eq

Author: RemyDegenne

LeanBandits/ForMathlib/CondDistrib.lean

@@ -816,40 +816,14 @@ instance : OrderedSub (FiniteMeasure α) where
     simp only [FiniteMeasure.le_iff_coe, FiniteMeasure.toMeasure_sub, FiniteMeasure.toMeasure_add]
     exact Measure.sub_le_iff_add
 
-instance : MeasurableSub₂ (FiniteMeasure α) where
-  measurable_sub := by
-    simp only [FiniteMeasure.sub_def]
-    refine Measurable.subtype_mk ?_
-    refine Measure.measurable_of_measurable_coe _ fun s hs ↦ ?_
-    sorry
-
-instance : MeasurableSingletonClass (Measure α) where
-  measurableSet_singleton μ := sorry
-
-instance : MeasurableSingletonClass (FiniteMeasure α) := Subtype.instMeasurableSingletonClass
-
-lemma Kernel.measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
-    MeasurableSet {a | κ a = η a} := by
-  let κ' : α → FiniteMeasure β := fun a ↦ ⟨κ a, inferInstance⟩
-  have hκ' : Measurable κ' := Measurable.subtype_mk (by fun_prop)
-  let η' : α → FiniteMeasure β := fun a ↦ ⟨η a, inferInstance⟩
-  have hη' : Measurable η' := Measurable.subtype_mk (by fun_prop)
-  have h2 : {a | κ a = η a}
-      = (fun a ↦ (κ' a, η' a)) ⁻¹'
-        {p : FiniteMeasure β × FiniteMeasure β | p.fst = p.snd} := by
-    ext
-    simp [κ', η', FiniteMeasure.ext_iff_coe]
-    sorry
-  rw [h2]
-  refine MeasurableSet.preimage ?_ (by fun_prop)
-  refine measurableSet_eq_fun' (by fun_prop) (by fun_prop)
-
-lemma Kernel.prodMkLeft_ae_eq_iff {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η]
+lemma Kernel.prodMkLeft_ae_eq_iff [MeasurableSpace.CountableOrCountablyGenerated α β]
+    {κ η : Kernel α β} [IsFiniteKernel κ] [IsFiniteKernel η]
     {μ : Measure (γ × α)} :
     κ.prodMkLeft γ =ᵐ[μ] η.prodMkLeft γ ↔ κ =ᵐ[μ.snd] η := by
   rw [Measure.snd, Filter.EventuallyEq, Filter.EventuallyEq, ae_map_iff (by fun_prop)]
   · simp
-  · exact Kernel.measurableSet_eq κ η
+  · classical
+    exact Kernel.measurableSet_eq κ η
 
 omit [Nonempty Ω'] in
 lemma condIndepFun_of_exists_condDistrib_prod_ae_eq_prodMkLeft

LeanBandits/ForMathlib/KernelSub.lean

@@ -202,4 +202,64 @@ lemma sub_apply [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFinit
   filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb
   simp [← hb]
 
+omit [CountableOrCountablyGenerated α β] in
+lemma le_iff (κ η : Kernel α β) : κ ≤ η ↔ ∀ a, κ a ≤ η a := Iff.rfl
+
+lemma sub_le_self [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)] [IsFiniteKernel κ]
+    [IsFiniteKernel η] :
+    κ - η ≤ κ := by
+  rw [le_iff]
+  intro a
+  rw [sub_apply]
+  exact Measure.sub_le
+
+instance [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ - η) :=
+  isFiniteKernel_of_le sub_le_self
+
+lemma sub_apply_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) : (κ - η) a = 0 ↔ κ a ≤ η a := by
+  simp_rw [sub_apply_eq_rnDeriv_add_singularPart,
+    add_eq_zero_iff_of_nonneg (Measure.zero_le _) (Measure.zero_le _)]
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)] at h
+    rw [singularPart_eq_zero_iff_absolutelyContinuous κ η a] at h
+    rw [← Measure.rnDeriv_le_one_iff_le h.2]
+    filter_upwards [h.1, rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2
+    rw [← hb2]
+    simp only [Pi.sub_apply, Pi.one_apply, Pi.zero_apply] at hb1
+    rwa [tsub_eq_zero_iff_le] at hb1
+  · rw [(singularPart_eq_zero_iff_absolutelyContinuous κ η a).mpr
+        (Measure.absolutelyContinuous_of_le h)]
+    rw [Kernel.withDensity_apply _ (by fun_prop), withDensity_eq_zero_iff (by fun_prop)]
+    simp only [and_true]
+    suffices κ.rnDeriv η a ≤ᵐ[η a] 1 by
+      filter_upwards [this] with b hb
+      simpa [tsub_eq_zero_iff_le] using hb
+    filter_upwards [Measure.rnDeriv_le_one_of_le h,
+      rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb1 hb2
+    rwa [hb2]
+
+lemma sub_eq_zero_iff_le [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    [IsFiniteKernel κ] [IsFiniteKernel η] : κ - η = 0 ↔ κ ≤ η := by
+  simp [Kernel.ext_iff, le_iff, sub_apply_eq_zero_iff_le]
+
+lemma measurableSet_eq_zero (κ : Kernel α β) [IsFiniteKernel κ] :
+    MeasurableSet {a | κ a = 0} := by
+  have h_sing : {a | κ a = 0} = {a | κ a ⟂ₘ κ a} := by ext; simp
+  rw [h_sing]
+  exact measurableSet_mutuallySingular κ κ
+
+lemma measurableSet_eq [∀ η : Kernel α β, Decidable (IsSFiniteKernel η)]
+    (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
+    MeasurableSet {a | κ a = η a} := by
+  have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by
+    ext1 a
+    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
+    exact ⟨fun h ↦ by simp [h], fun h ↦ le_antisymm h.1 h.2⟩
+  rw [h_sub]
+  refine MeasurableSet.inter ?_ ?_
+  · exact measurableSet_eq_zero _
+  · exact measurableSet_eq_zero _
+
 end ProbabilityTheory.Kernel