From 3b92d54a05ee592aa2c6181a4e76b1bb7cc45d0b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <Remydegenne@gmail.com>
Date: Wed, 7 Jun 2023 11:35:18 +0000
Subject: [PATCH] chore(probability/kernel/composition): redefine kernel.comp
 using measure.bind, remove kernel.map_measure (#19160)

We replace the definition of `kernel.comp` with a new one using `measure.bind`: it removes the need for `is_s_finite_kernel` hypotheses in the definition and most lemmas. When the kernels are s-finite, the new definition coincides with the old one.

We remove `kernel.map_measure` because it is exactly the same as `measure.bind` applied to a kernel.



Co-authored-by: RemyDegenne <remydegenne@gmail.com>
---
 src/probability/kernel/composition.lean |  51 ++++++-----
 src/probability/kernel/invariance.lean  | 115 ++++++------------------
 2 files changed, 56 insertions(+), 110 deletions(-)

diff --git a/src/probability/kernel/composition.lean b/src/probability/kernel/composition.lean
index ced5d02480471..17cc45818f356 100644
--- a/src/probability/kernel/composition.lean
+++ b/src/probability/kernel/composition.lean
@@ -13,8 +13,8 @@ We define
 * the composition-product `κ ⊗ₖ η` of two s-finite kernels `κ : kernel α β` and
   `η : kernel (α × β) γ`, a kernel from `α` to `β × γ`.
 * the map and comap of a kernel along a measurable function.
-* the composition `η ∘ₖ κ` of s-finite kernels `κ : kernel α β` and `η : kernel β γ`,
-  a kernel from `α` to `γ`.
+* the composition `η ∘ₖ κ` of kernels `κ : kernel α β` and `η : kernel β γ`,  kernel from `α` to
+  `γ`.
 * the product `κ ×ₖ η` of s-finite kernels `κ : kernel α β` and `η : kernel α γ`,
   a kernel from `α` to `β × γ`.
 
@@ -34,7 +34,7 @@ Kernels built from other kernels:
   `∫⁻ c, g c ∂(map κ f hf a) = ∫⁻ b, g (f b) ∂(κ a)`
 * `comap (κ : kernel α β) (f : γ → α) (hf : measurable f) : kernel γ β`
   `∫⁻ b, g b ∂(comap κ f hf c) = ∫⁻ b, g b ∂(κ (f c))`
-* `comp (η : kernel β γ) (κ : kernel α β) : kernel α γ`: composition of 2 s-finite kernels.
+* `comp (η : kernel β γ) (κ : kernel α β) : kernel α γ`: composition of 2 kernels.
   We define a notation `η ∘ₖ κ = comp η κ`.
   `∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a)`
 * `prod (κ : kernel α β) (η : kernel α γ) : kernel α (β × γ)`: product of 2 s-finite kernels.
@@ -741,69 +741,72 @@ include mγ
 
 /-- Composition of two s-finite kernels. -/
 noncomputable
-def comp (η : kernel β γ) [is_s_finite_kernel η] (κ : kernel α β) [is_s_finite_kernel κ] :
-  kernel α γ :=
-snd (κ ⊗ₖ prod_mk_left α η)
+def comp (η : kernel β γ) (κ : kernel α β) : kernel α γ :=
+{ val := λ a, (κ a).bind η,
+  property := (measure.measurable_bind' (kernel.measurable _)).comp (kernel.measurable _) }
 
 localized "infix (name := kernel.comp) ` ∘ₖ `:100 := probability_theory.kernel.comp" in
   probability_theory
 
-lemma comp_apply (η : kernel β γ) [is_s_finite_kernel η] (κ : kernel α β) [is_s_finite_kernel κ]
-  (a : α) {s : set γ} (hs : measurable_set s) :
+lemma comp_apply (η : kernel β γ) (κ : kernel α β) (a : α) :
+  (η ∘ₖ κ) a = (κ a).bind η := rfl
+
+lemma comp_apply' (η : kernel β γ) (κ : kernel α β) (a : α) {s : set γ} (hs : measurable_set s) :
   (η ∘ₖ κ) a s = ∫⁻ b, η b s ∂(κ a) :=
+by rw [comp_apply, measure.bind_apply hs (kernel.measurable _)]
+
+lemma comp_eq_snd_comp_prod (η : kernel β γ) [is_s_finite_kernel η]
+  (κ : kernel α β) [is_s_finite_kernel κ] :
+  η ∘ₖ κ = snd (κ ⊗ₖ prod_mk_left α η) :=
 begin
-  rw [comp, snd_apply' _ _ hs, comp_prod_apply],
+  ext a s hs : 2,
+  rw [comp_apply' _ _ _ hs, snd_apply' _ _ hs, comp_prod_apply],
   swap, { exact measurable_snd hs, },
   simp only [set.mem_set_of_eq, set.set_of_mem_eq, prod_mk_left_apply' _ _ s],
 end
 
-lemma lintegral_comp (η : kernel β γ) [is_s_finite_kernel η] (κ : kernel α β) [is_s_finite_kernel κ]
+lemma lintegral_comp (η : kernel β γ) (κ : kernel α β)
   (a : α) {g : γ → ℝ≥0∞} (hg : measurable g) :
   ∫⁻ c, g c ∂((η ∘ₖ κ) a) = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a) :=
-begin
-  rw [comp, lintegral_snd _ _ hg],
-  change ∫⁻ bc, (λ a b, g b) bc.fst bc.snd ∂((κ ⊗ₖ prod_mk_left α η) a)
-    = ∫⁻ b, ∫⁻ c, g c ∂(η b) ∂(κ a),
-  exact lintegral_comp_prod _ _ _ (hg.comp measurable_snd),
-end
+by rw [comp_apply, measure.lintegral_bind (kernel.measurable _) hg]
 
 instance is_markov_kernel.comp (η : kernel β γ) [is_markov_kernel η]
   (κ : kernel α β) [is_markov_kernel κ] :
   is_markov_kernel (η ∘ₖ κ) :=
-by { rw comp, apply_instance, }
+by { rw comp_eq_snd_comp_prod, apply_instance, }
 
 instance is_finite_kernel.comp (η : kernel β γ) [is_finite_kernel η]
   (κ : kernel α β) [is_finite_kernel κ] :
   is_finite_kernel (η ∘ₖ κ) :=
-by { rw comp, apply_instance, }
+by { rw comp_eq_snd_comp_prod, apply_instance, }
 
 instance is_s_finite_kernel.comp (η : kernel β γ) [is_s_finite_kernel η]
   (κ : kernel α β) [is_s_finite_kernel κ] :
   is_s_finite_kernel (η ∘ₖ κ) :=
-by { rw comp, apply_instance, }
+by { rw comp_eq_snd_comp_prod, apply_instance, }
 
 /-- Composition of kernels is associative. -/
 lemma comp_assoc {δ : Type*} {mδ : measurable_space δ} (ξ : kernel γ δ) [is_s_finite_kernel ξ]
-  (η : kernel β γ) [is_s_finite_kernel η] (κ : kernel α β) [is_s_finite_kernel κ] :
+  (η : kernel β γ) (κ : kernel α β) :
   (ξ ∘ₖ η ∘ₖ κ) = ξ ∘ₖ (η ∘ₖ κ) :=
 begin
   refine ext_fun (λ a f hf, _),
   simp_rw [lintegral_comp _ _ _ hf, lintegral_comp _ _ _ hf.lintegral_kernel],
 end
 
-lemma deterministic_comp_eq_map (hf : measurable f) (κ : kernel α β) [is_s_finite_kernel κ] :
+lemma deterministic_comp_eq_map (hf : measurable f) (κ : kernel α β) :
   (deterministic f hf ∘ₖ κ) = map κ f hf :=
 begin
   ext a s hs : 2,
-  simp_rw [map_apply' _ _ _ hs, comp_apply _ _ _ hs, deterministic_apply' hf _ hs,
+  simp_rw [map_apply' _ _ _ hs, comp_apply' _ _ _ hs, deterministic_apply' hf _ hs,
     lintegral_indicator_const_comp hf hs, one_mul],
 end
 
-lemma comp_deterministic_eq_comap (κ : kernel α β) [is_s_finite_kernel κ] (hg : measurable g) :
+lemma comp_deterministic_eq_comap (κ : kernel α β) (hg : measurable g) :
   (κ ∘ₖ deterministic g hg) = comap κ g hg :=
 begin
   ext a s hs : 2,
-  simp_rw [comap_apply' _ _ _ s, comp_apply _ _ _ hs, deterministic_apply hg a,
+  simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
     lintegral_dirac' _ (kernel.measurable_coe κ hs)],
 end
 
diff --git a/src/probability/kernel/invariance.lean b/src/probability/kernel/invariance.lean
index 75ccfd8c63442..a33a340bb8e74 100644
--- a/src/probability/kernel/invariance.lean
+++ b/src/probability/kernel/invariance.lean
@@ -8,20 +8,17 @@ import probability.kernel.composition
 /-!
 # Invariance of measures along a kernel
 
-We define the push-forward of a measure along a kernel which results in another measure. In the
-case that the push-forward measure is the same as the original measure, we say that the measure is
-invariant with respect to the kernel.
+We say that a measure `μ` is invariant with respect to a kernel `κ` if its push-forward along the
+kernel `μ.bind κ` is the same measure.
 
 ## Main definitions
 
-* `probability_theory.kernel.map_measure`: the push-forward of a measure along a kernel.
 * `probability_theory.kernel.invariant`: invariance of a given measure with respect to a kernel.
 
 ## Useful lemmas
 
-* `probability_theory.kernel.comp_apply_eq_map_measure`,
-  `probability_theory.kernel.const_map_measure_eq_comp_const`, and
-  `probability_theory.kernel.comp_const_apply_eq_map_measure` established the relationship between
+* `probability_theory.kernel.const_bind_eq_comp_const`, and
+  `probability_theory.kernel.comp_const_apply_eq_bind` established the relationship between
   the push-forward measure and the composition of kernels.
 
 -/
@@ -41,87 +38,35 @@ namespace kernel
 
 /-! ### Push-forward of measures along a kernel -/
 
-/-- The push-forward of a measure along a kernel. -/
-noncomputable
-def map_measure (κ : kernel α β) (μ : measure α) :
-  measure β :=
-measure.of_measurable (λ s hs, ∫⁻ x, κ x s ∂μ)
-  (by simp only [measure_empty, measure_theory.lintegral_const, zero_mul])
-  begin
-    intros f hf₁ hf₂,
-    simp_rw [measure_Union hf₂ hf₁,
-      lintegral_tsum (λ i, (kernel.measurable_coe κ (hf₁ i)).ae_measurable)],
-  end
-
-@[simp]
-lemma map_measure_apply (κ : kernel α β) (μ : measure α) {s : set β} (hs : measurable_set s) :
-  map_measure κ μ s = ∫⁻ x, κ x s ∂μ :=
-by rw [map_measure, measure.of_measurable_apply s hs]
-
 @[simp]
-lemma map_measure_zero (κ : kernel α β) : map_measure κ 0 = 0 :=
+lemma bind_add (μ ν : measure α) (κ : kernel α β) :
+  (μ + ν).bind κ = μ.bind κ + ν.bind κ :=
 begin
   ext1 s hs,
-  rw [map_measure_apply κ 0 hs, lintegral_zero_measure, measure.coe_zero, pi.zero_apply],
+  rw [measure.bind_apply hs (kernel.measurable _), lintegral_add_measure, measure.coe_add,
+    pi.add_apply, measure.bind_apply hs (kernel.measurable _),
+    measure.bind_apply hs (kernel.measurable _)],
 end
 
 @[simp]
-lemma map_measure_add  (κ : kernel α β) (μ ν : measure α) :
-  map_measure κ (μ + ν) = map_measure κ μ + map_measure κ ν :=
+lemma bind_smul (κ : kernel α β) (μ : measure α) (r : ℝ≥0∞) :
+  (r • μ).bind κ = r • μ.bind κ :=
 begin
   ext1 s hs,
-  rw [map_measure_apply κ (μ + ν) hs, lintegral_add_measure, measure.coe_add, pi.add_apply,
-    map_measure_apply κ μ hs, map_measure_apply κ ν hs],
+  rw [measure.bind_apply hs (kernel.measurable _), lintegral_smul_measure, measure.coe_smul,
+    pi.smul_apply, measure.bind_apply hs (kernel.measurable _), smul_eq_mul],
 end
 
-@[simp]
-lemma map_measure_smul (κ : kernel α β) (μ : measure α) (r : ℝ≥0∞) :
-  map_measure κ (r • μ) = r • map_measure κ μ :=
+lemma const_bind_eq_comp_const (κ : kernel α β) (μ : measure α) :
+  const α (μ.bind κ) = κ ∘ₖ const α μ :=
 begin
-  ext1 s hs,
-  rw [map_measure_apply κ (r • μ) hs, lintegral_smul_measure, measure.coe_smul, pi.smul_apply,
-    map_measure_apply κ μ hs, smul_eq_mul],
+  ext a s hs : 2,
+  simp_rw [comp_apply' _ _ _ hs, const_apply, measure.bind_apply hs (kernel.measurable _)],
 end
 
-include mγ
-
-lemma comp_apply_eq_map_measure
-  (η : kernel β γ) [is_s_finite_kernel η] (κ : kernel α β) [is_s_finite_kernel κ] (a : α) :
-  (η ∘ₖ κ) a = map_measure η (κ a) :=
-begin
-  ext1 s hs,
-  rw [comp_apply η κ a hs, map_measure_apply η _ hs],
-end
-
-omit mγ
-
-lemma const_map_measure_eq_comp_const (κ : kernel α β) [is_s_finite_kernel κ]
-  (μ : measure α) [is_finite_measure μ] :
-  const α (map_measure κ μ) = κ ∘ₖ const α μ :=
-begin
-  ext1 a, ext1 s hs,
-  rw [const_apply, map_measure_apply _ _ hs, comp_apply _ _ _ hs, const_apply],
-end
-
-lemma comp_const_apply_eq_map_measure (κ : kernel α β) [is_s_finite_kernel κ]
-  (μ : measure α) [is_finite_measure μ] (a : α) :
-  (κ ∘ₖ const α μ) a = map_measure κ μ :=
-by rw [← const_apply (map_measure κ μ) a, const_map_measure_eq_comp_const κ μ]
-
-lemma lintegral_map_measure
-  (κ : kernel α β) [is_s_finite_kernel κ] (μ : measure α) [is_finite_measure μ]
-  {f : β → ℝ≥0∞} (hf : measurable f) :
-  ∫⁻ b, f b ∂(map_measure κ μ) = ∫⁻ a, ∫⁻ b, f b ∂(κ a) ∂μ :=
-begin
-  by_cases hα : nonempty α,
-  { have := const_apply μ hα.some,
-    swap, apply_instance,
-    conv_rhs { rw [← this]  },
-    rw [← lintegral_comp _ _ _ hf, ← comp_const_apply_eq_map_measure κ μ hα.some] },
-  { haveI := not_nonempty_iff.1 hα,
-    rw [μ.eq_zero_of_is_empty, map_measure_zero, lintegral_zero_measure,
-      lintegral_zero_measure] }
-end
+lemma comp_const_apply_eq_bind (κ : kernel α β) (μ : measure α) (a : α) :
+  (κ ∘ₖ const α μ) a = μ.bind κ :=
+by rw [← const_apply (μ.bind κ) a, const_bind_eq_comp_const κ μ]
 
 omit mβ
 
@@ -130,24 +75,22 @@ omit mβ
 /-- A measure `μ` is invariant with respect to the kernel `κ` if the push-forward measure of `μ`
 along `κ` equals `μ`. -/
 def invariant (κ : kernel α α) (μ : measure α) : Prop :=
-map_measure κ μ = μ
+μ.bind κ = μ
 
 variables {κ η : kernel α α} {μ : measure α}
 
-lemma invariant.def (hκ : invariant κ μ) : map_measure κ μ = μ := hκ
+lemma invariant.def (hκ : invariant κ μ) : μ.bind κ = μ := hκ
 
-lemma invariant.comp_const [is_s_finite_kernel κ] [is_finite_measure μ]
-  (hκ : invariant κ μ) : (κ ∘ₖ const α μ) = const α μ :=
-by rw [← const_map_measure_eq_comp_const κ μ, hκ.def]
+lemma invariant.comp_const (hκ : invariant κ μ) : κ ∘ₖ const α μ = const α μ :=
+by rw [← const_bind_eq_comp_const κ μ, hκ.def]
 
-lemma invariant.comp [is_s_finite_kernel κ] [is_s_finite_kernel η] [is_finite_measure μ]
-  (hκ : invariant κ μ) (hη : invariant η μ) : invariant (κ ∘ₖ η) μ :=
+lemma invariant.comp [is_s_finite_kernel κ] (hκ : invariant κ μ) (hη : invariant η μ) :
+  invariant (κ ∘ₖ η) μ :=
 begin
-  by_cases hα : nonempty α,
-  { simp_rw [invariant, ← comp_const_apply_eq_map_measure (κ ∘ₖ η) μ hα.some, comp_assoc,
+  casesI is_empty_or_nonempty α with _ hα,
+  { exact subsingleton.elim _ _ },
+  { simp_rw [invariant, ← comp_const_apply_eq_bind (κ ∘ₖ η) μ hα.some, comp_assoc,
       hη.comp_const, hκ.comp_const, const_apply] },
-  { haveI := not_nonempty_iff.1 hα,
-    exact subsingleton.elim _ _ },
 end
 
 end kernel