use dot notation for kernels

LorenzoLuccioli · Aug 29, 2024 · aa32fcb · aa32fcb
1 parent 4dd53ed
commit aa32fcb
Show file tree

Hide file tree

Showing 13 changed files with 152 additions and 174 deletions.
diff --git a/TestingLowerBounds/Divergences/Hellinger.lean b/TestingLowerBounds/Divergences/Hellinger.lean
@@ -804,7 +804,7 @@ lemma integrable_hellingerDiv_iff' (ha_pos : 0 < a) (ha_ne_one : a ≠ 1)
     <| inv_eq_zero.mp.mt <| sub_ne_zero_of_ne ha_ne_one)]
   obtain ⟨C, ⟨hC_finite, hC⟩⟩ := IsFiniteKernel.exists_univ_le (κ := η)
   refine integrable_add_iff_integrable_left <| (integrable_const C.toReal).mono' ?_ ?_
-  · exact Kernel.measurable_coe η .univ |>.ennreal_toReal.neg.aestronglyMeasurable
+  · exact η.measurable_coe .univ |>.ennreal_toReal.neg.aestronglyMeasurable
   refine eventually_of_forall (fun x ↦ ?_)
   rw [norm_eq_abs, abs_neg, abs_eq_self.mpr ENNReal.toReal_nonneg, ENNReal.toReal_le_toReal
     (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)]
@@ -819,18 +819,18 @@ lemma integrable_hellingerDiv_zero [CountableOrCountablyGenerated α β]
   obtain ⟨C, ⟨hC_finite, hC⟩⟩ := IsFiniteKernel.exists_univ_le (κ := η)
   simp only [EReal.toReal_coe_ennreal]
   have h_eq : (fun x ↦ ((η x) {y | ((κ x).rnDeriv (η x) y).toReal = 0}).toReal) =
-      fun x ↦ ((η x) {y | (Kernel.rnDeriv κ η x y).toReal = 0}).toReal := by
+      fun x ↦ ((η x) {y | (κ.rnDeriv η x y).toReal = 0}).toReal := by
     ext x
     congr 1
     apply measure_congr
-    filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure κ η x] with y hy
+    filter_upwards [κ.rnDeriv_eq_rnDeriv_measure η x] with y hy
     simp only [Set.setOf_app_iff, eq_iff_iff, hy]
   simp_rw [h_eq]
   apply (integrable_const C.toReal).mono'
   · apply Measurable.aestronglyMeasurable
     apply Measurable.ennreal_toReal
     exact Kernel.measurable_kernel_prod_mk_left
-      (measurableSet_eq_fun (Kernel.measurable_rnDeriv _ _).ennreal_toReal measurable_const)
+      (measurableSet_eq_fun (κ.measurable_rnDeriv η).ennreal_toReal measurable_const)
   · refine eventually_of_forall (fun x ↦ ?_)
     simp only [norm_eq_abs, ENNReal.abs_toReal, ENNReal.toReal_le_toReal
     (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)]

diff --git a/TestingLowerBounds/Divergences/KullbackLeibler.lean b/TestingLowerBounds/Divergences/KullbackLeibler.lean
@@ -447,22 +447,22 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
     {ξ : Kernel α β} [IsSFiniteKernel ξ] {κ η : Kernel (α × β) γ}
     [IsMarkovKernel κ] [IsMarkovKernel η] :
     condKL κ η (μ ⊗ₘ ξ) = ⊤
-      ↔ ¬ (∀ᵐ a ∂μ, condKL (Kernel.snd' κ a) (Kernel.snd' η a) (ξ a) ≠ ⊤)
-        ∨ ¬ Integrable (fun x ↦ (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal) μ := by
+      ↔ ¬ (∀ᵐ a ∂μ, condKL (κ.snd' a) (η.snd' a) (ξ a) ≠ ⊤)
+        ∨ ¬ Integrable (fun x ↦ (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ := by
   rw [condKL_eq_top_iff]
   have h_ae_eq (h_ae : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b))
       (h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (llr (κ (a, b)) (η (a, b))) (κ (a, b))) :
-      (fun x ↦ (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal)
+      (fun x ↦ (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal)
         =ᵐ[μ] fun a ↦ ∫ b, (kl (κ (a, b)) (η (a, b))).toReal ∂ξ a := by
     filter_upwards [h_ae, h_int] with a ha_ae ha_int
     rw [condKL_toReal_of_ae_ac_of_ae_integrable]
     · simp only [Kernel.snd'_apply]
-    · filter_upwards [ha_ae] with b hb using Kernel.snd'_apply _ _ _ ▸ hb
-    · filter_upwards [ha_int] with b hb using Kernel.snd'_apply _ _ _ ▸ hb
+    · filter_upwards [ha_ae] with b hb using κ.snd'_apply _ _ ▸ hb
+    · filter_upwards [ha_int] with b hb using κ.snd'_apply _ _ ▸ hb
   constructor
   · by_cases h_ae : ∀ᵐ x ∂(μ ⊗ₘ ξ), κ x ≪ η x
     swap
-    · rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
+    · rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
       simp_rw [condKL_ne_top_iff, Kernel.snd'_apply, eventually_and, not_and_or]
       intro; left; left
       exact h_ae
@@ -485,7 +485,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
       simp only [condKL_ne_top_iff, Kernel.snd'_apply] at ha_int2
       exact ha_int2.2.2
     right
-    rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
+    rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
     apply Integrable.congr.mt
     swap; exact fun a ↦ ∫ b, (kl (κ (a, b)) (η (a, b))).toReal ∂(ξ a)
     push_neg
@@ -500,7 +500,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
     contrapose! h
     obtain ⟨h_ae, ⟨h_int1, h_int2⟩⟩ := h
     rw [ae_compProd_integrable_llr_iff h_ae] at h_int1
-    rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ae
+    rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ae
     have h_meas := (Integrable.integral_compProd' h_int2).aestronglyMeasurable
     rw [Measure.integrable_compProd_iff h_int2.aestronglyMeasurable] at h_int2
     constructor
@@ -524,7 +524,7 @@ lemma condKL_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ]
 lemma condKL_compProd_meas [CountableOrCountablyGenerated (α × β) γ] [SFinite μ] {ξ : Kernel α β}
     [IsSFiniteKernel ξ] {κ η : Kernel (α × β) γ} [IsMarkovKernel κ] [IsMarkovKernel η]
     (h : condKL κ η (μ ⊗ₘ ξ) ≠ ⊤) :
-    condKL κ η (μ ⊗ₘ ξ) = ∫ x, (condKL (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal ∂μ := by
+    condKL κ η (μ ⊗ₘ ξ) = ∫ x, (condKL (κ.snd' x) (η.snd' x) (ξ x)).toReal ∂μ := by
   rw [condKL_ne_top_iff'.mp h, Measure.integral_compProd (condKL_ne_top_iff.mp h).2.2]
   replace h := condKL_compProd_meas_eq_top.mpr.mt h
   push_neg at h
@@ -571,29 +571,28 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
         condKL_ne_bot, condKL_of_not_integrable', EReal.add_top_of_ne_bot, kl_ne_bot,
         condKL_of_not_ae_integrable]
   have intμν := integrable_llr_of_integrable_llr_compProd h_prod h_int
-  have intκη : Integrable (fun a ↦ ∫ (x : β), log (Kernel.rnDeriv κ η a x).toReal ∂κ a) μ := by
+  have intκη : Integrable (fun a ↦ ∫ (x : β), log (κ.rnDeriv η a x).toReal ∂κ a) μ := by
     apply Integrable.congr (integrable_integral_llr_of_integrable_llr_compProd h_prod h_int)
     filter_upwards [hκη] with a ha
     apply integral_congr_ae
-    filter_upwards [ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)] with x hx
+    filter_upwards [ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)] with x hx
     rw [hx, llr_def]
   have intκη2 := ae_integrable_llr_of_integrable_llr_compProd h_prod h_int
   calc kl (μ ⊗ₘ κ) (ν ⊗ₘ η) = ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂(μ ⊗ₘ κ) :=
     kl_of_ac_of_integrable h_prod h_int
   _ = ∫ a, ∫ x, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) (a, x) ∂κ a ∂μ := mod_cast Measure.integral_compProd h_int
-  _ = ∫ a, ∫ x, log (μ.rnDeriv ν a).toReal
-      + log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
+  _ = ∫ a, ∫ x, log (μ.rnDeriv ν a).toReal + log (κ.rnDeriv η a x).toReal ∂κ a ∂μ := by
     norm_cast
     have h := hμν.ae_le (Measure.ae_ae_of_ae_compProd (Kernel.rnDeriv_measure_compProd μ ν κ η))
     apply Kernel.integral_congr_ae₂
     filter_upwards [h, hκη, Measure.rnDeriv_toReal_pos hμν] with a ha hκηa hμν_pos
     have hμν_zero : (μ.rnDeriv ν a).toReal ≠ 0 := by linarith
     filter_upwards [Kernel.rnDeriv_toReal_pos hκηa, hκηa.ae_le ha] with x hκη_pos hx
-    have hκη_zero : (Kernel.rnDeriv κ η a x).toReal ≠ 0 := by linarith
+    have hκη_zero : (κ.rnDeriv η a x).toReal ≠ 0 := by linarith
     rw [llr, hx, ENNReal.toReal_mul]
     exact log_mul hμν_zero hκη_zero
   _ = ∫ a, ∫ _, log (μ.rnDeriv ν a).toReal ∂κ a ∂μ
-      + ∫ a, ∫ x, log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
+      + ∫ a, ∫ x, log (κ.rnDeriv η a x).toReal ∂κ a ∂μ := by
     norm_cast
     rw [← integral_add']
     simp only [Pi.add_apply]
@@ -603,7 +602,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
     · exact intκη
     apply integral_congr_ae
     filter_upwards [hκη, intκη2] with a ha hκηa
-    have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
+    have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
     rw [← integral_add']
     rotate_left
     · simp only [integrable_const]
@@ -619,7 +618,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
     congr 2
     apply Kernel.integral_congr_ae₂
     filter_upwards [hκη] with a ha
-    have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
+    have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
     filter_upwards [h] with x hx
     congr
   _ = kl μ ν + condKL κ η μ := by
@@ -630,7 +629,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
       simp_rw [llr_def]
       apply Integrable.congr intκη
       filter_upwards [hκη] with a ha
-      have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
+      have h := ha.ae_le (κ.rnDeriv_eq_rnDeriv_measure η a)
       apply integral_congr_ae
       filter_upwards [h] with x hx
       rw [hx]
@@ -672,13 +671,13 @@ lemma kl_compProd_kernel_of_ae_ac_of_ae_integrable [CountableOrCountablyGenerate
   simp only [Kernel.absolutelyContinuous_compProd_iff, eventually_and] at h_ac
   filter_upwards [h_ac.1, h_ac.2, h_ae_int.1, h_ae_int.2.1, h_ae_int.2.2] with a ha_ac₁ ha_ac₂
     ha_int₁ ha_int_kl₂ ha_int₂
-  have h_snd_ne_top : condKL (Kernel.snd' κ₂ a) (Kernel.snd' η₂ a) (κ₁ a) ≠ ⊤ := by
+  have h_snd_ne_top : condKL (κ₂.snd' a) (η₂.snd' a) (κ₁ a) ≠ ⊤ := by
     apply condKL_ne_top_iff.mpr
     simp_rw [Kernel.snd'_apply]
     exact ⟨ha_ac₂, ⟨ha_int₂, ha_int_kl₂⟩⟩
   simp_rw [Kernel.compProd_apply_eq_compProd_snd', kl_compProd,
     EReal.toReal_add (kl_ne_top_iff.mpr ⟨ha_ac₁, ha_int₁⟩) (kl_ne_bot (κ₁ a) (η₁ a)) h_snd_ne_top
-    (condKL_ne_bot (Kernel.snd' κ₂ a) (Kernel.snd' η₂ a) (κ₁ a)),
+    (condKL_ne_bot (κ₂.snd' a) (η₂.snd' a) (κ₁ a)),
     condKL_ne_top_iff'.mp h_snd_ne_top, EReal.toReal_coe, Kernel.snd'_apply]
 
 lemma condKL_compProd_kernel_eq_top [CountableOrCountablyGenerated (α × β) γ] {κ₁ η₁ : Kernel α β}
@@ -691,14 +690,13 @@ lemma condKL_compProd_kernel_eq_top [CountableOrCountablyGenerated (α × β) γ
     simp only [condKL_isEmpty_left]
     tauto
   have := countableOrCountablyGenerated_right_of_prod_left_of_nonempty (α := α) (β := β) (γ := γ)
-  simp_rw [condKL_eq_top_iff,
-    Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)]
+  simp_rw [condKL_eq_top_iff, Measure.ae_compProd_iff (κ₂.measurableSet_absolutelyContinuous _)]
   by_cases h_ac : ∀ᵐ a ∂μ, (κ₁ ⊗ₖ κ₂) a ≪ (η₁ ⊗ₖ η₂) a
     <;> have h_ac' := h_ac
     <;> simp only [Kernel.absolutelyContinuous_compProd_iff, eventually_and, not_and_or] at h_ac'
     <;> simp only [h_ac, h_ac', not_false_eq_true, true_or, not_true, true_iff, false_or]
   swap; tauto
-  rw [← Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac'
+  rw [← Measure.ae_compProd_iff (κ₂.measurableSet_absolutelyContinuous _)] at h_ac'
   by_cases h_ae_int : ∀ᵐ a ∂μ, Integrable (llr ((κ₁ ⊗ₖ κ₂) a) ((η₁ ⊗ₖ η₂) a)) ((κ₁ ⊗ₖ κ₂) a)
     <;> have h_ae_int' := h_ae_int
     <;> simp only [eventually_congr (h_ac.mono (fun a h ↦ (Kernel.integrable_llr_compProd_iff' a h))),

diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean
@@ -885,30 +885,30 @@ section Measurability
 
 lemma measurableSet_integrable_f_kernel_rnDeriv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η ξ : Kernel α β) [IsFiniteKernel ξ] (hf : StronglyMeasurable f) :
-    MeasurableSet {a | Integrable (fun x ↦ f (Kernel.rnDeriv κ η a x).toReal) (ξ a)} :=
+    MeasurableSet {a | Integrable (fun x ↦ f (κ.rnDeriv η a x).toReal) (ξ a)} :=
   measurableSet_kernel_integrable
-    (hf.comp_measurable (Kernel.measurable_rnDeriv κ η).ennreal_toReal)
+    (hf.comp_measurable (κ.measurable_rnDeriv η).ennreal_toReal)
 
 lemma measurableSet_integrable_f_rnDeriv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) :
     MeasurableSet {a | Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)} := by
   convert measurableSet_integrable_f_kernel_rnDeriv κ η η hf using 3 with a
   refine integrable_congr ?_
-  filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure κ η a] with b hb
+  filter_upwards [κ.rnDeriv_eq_rnDeriv_measure η a] with b hb
   rw [hb]
 
 lemma measurable_integral_f_rnDeriv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) :
     Measurable fun a ↦ ∫ x, f ((∂κ a/∂η a) x).toReal ∂(η a) := by
   have : ∀ a, ∫ x, f ((∂κ a/∂η a) x).toReal ∂η a
-      = ∫ x, f (Kernel.rnDeriv κ η a x).toReal ∂η a := by
+      = ∫ x, f (κ.rnDeriv η a x).toReal ∂η a := by
     refine fun a ↦ integral_congr_ae ?_
-    filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure κ η a] with x hx
+    filter_upwards [κ.rnDeriv_eq_rnDeriv_measure η a] with x hx
     rw [hx]
   simp_rw [this]
   refine (StronglyMeasurable.integral_kernel_prod_left ?_).measurable
   refine hf.comp_measurable ?_
-  exact ((Kernel.measurable_rnDeriv κ η).comp measurable_swap).ennreal_toReal
+  exact ((κ.measurable_rnDeriv η).comp measurable_swap).ennreal_toReal
 
 lemma measurable_fDiv [MeasurableSpace.CountableOrCountablyGenerated α β]
     (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η]
@@ -930,8 +930,7 @@ lemma measurable_fDiv [MeasurableSpace.CountableOrCountablyGenerated α β]
   refine Measurable.add ?_ ?_
   · exact (measurable_integral_f_rnDeriv _ _ hf).coe_real_ereal
   · refine Measurable.const_mul ?_ _
-    exact ((Measure.measurable_coe .univ).comp
-      (Kernel.measurable_singularPart κ η)).coe_ereal_ennreal
+    exact ((Measure.measurable_coe .univ).comp (κ.measurable_singularPart η)).coe_ereal_ennreal
 
 end Measurability