From 852453f98ac01fc6b8fc76fe4bdcfdadcec875f7 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Sat, 3 Aug 2024 17:04:11 +0200 Subject: [PATCH 01/10] apply changes --- Mathlib/Probability/Kernel/Composition.lean | 90 +++++++++++++++++++++ 1 file changed, 90 insertions(+) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index a8650f58e53c3..df43becb06ae4 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -973,6 +973,96 @@ lemma snd_swapRight (κ : Kernel α (β × γ)) : snd (swapRight κ) = fst κ := end FstSnd +section Fst'Snd' + +variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} + +/-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for +a given `b : β`. -/ +noncomputable def fst' (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := + comap κ (fun a ↦ (a, b)) (measurable_id.prod_mk measurable_const) + +@[simp] theorem fst'_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : fst' κ b a = κ (a, b) := rfl + +@[simp] lemma fst'_zero (b : β) : fst' (0 : Kernel (α × β) γ) b = 0 := by simp [fst'] + +instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (fst' κ b) := by + rw [fst']; infer_instance + +instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (fst' κ b) := by + rw [fst']; infer_instance + +instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (fst' κ b) := by + rw [fst']; infer_instance + +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((fst' κ b) a) := by + rw [fst'_apply]; infer_instance + +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (fst' κ b)] : + IsMarkovKernel κ := by + refine ⟨fun _ ↦ ⟨?_⟩⟩ + rw [← fst'_apply, measure_univ] + +--I'm not sure this lemma is actually useful +lemma comap_fst' (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : + comap (fst' κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by + ext d s + rw [comap_apply, fst'_apply, comap_apply] + +@[simp] +lemma fst'_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : + fst' (prodMkLeft α κ) b a = κ b := rfl + +@[simp] +lemma fst'_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : + fst' (prodMkRight β κ) b = κ := rfl + +/-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for +a given `a : α`. -/ +noncomputable def snd' (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := + comap κ (fun b ↦ (a, b)) (measurable_const.prod_mk measurable_id) + +@[simp] theorem snd'_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : snd' κ a b = κ (a, b) := rfl + +@[simp] lemma snd'_zero (a : α) : snd' (0 : Kernel (α × β) γ) a = 0 := by simp [snd'] + +instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (snd' κ a) := by + rw [snd']; infer_instance + +instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (snd' κ a) := by + rw [snd']; infer_instance + +instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (snd' κ a) := by + rw [snd']; infer_instance + +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((snd' κ a) b) := by + rw [snd'_apply]; infer_instance + +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (snd' κ b)] : + IsMarkovKernel κ := by + refine ⟨fun _ ↦ ⟨?_⟩⟩ + rw [← snd'_apply, measure_univ] + +--I'm not sure this lemma is actually useful +lemma comap_snd' (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : + comap (snd' κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by + ext d s + rw [comap_apply, snd'_apply, comap_apply] + +@[simp] +lemma snd'_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : + snd' (prodMkLeft α κ) a = κ := rfl + +@[simp] +lemma snd'_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : + snd' (prodMkRight β κ) a b = κ a := rfl + +@[simp] lemma fst'_swapRight (κ : Kernel (α × β) γ) : fst' (swapLeft κ) = snd' κ := rfl + +@[simp] lemma snd'_swapRight (κ : Kernel (α × β) γ) : snd' (swapLeft κ) = fst' κ := rfl + +end Fst'Snd' + section Comp /-! ### Composition of two kernels -/ From 573979ce20691ebe6aa44e9e5572a0352b33feef Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Sat, 3 Aug 2024 17:25:00 +0200 Subject: [PATCH 02/10] Add `compProd_apply_eq_compProd_snd'` --- Mathlib/Probability/Kernel/MeasureCompProd.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Probability/Kernel/MeasureCompProd.lean b/Mathlib/Probability/Kernel/MeasureCompProd.lean index 99269703362e9..577b5fa21ab16 100644 --- a/Mathlib/Probability/Kernel/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/MeasureCompProd.lean @@ -67,6 +67,14 @@ lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ] rw [Set.indicator_apply] split_ifs with ha <;> simp [ha] +lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_snd' {γ : Type*} + {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) + [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) : + (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.snd' η a) := by + ext s hs + simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.snd'_apply] + rfl + lemma compProd_congr [SFinite μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] (h : κ =ᵐ[μ] η) : μ ⊗ₘ κ = μ ⊗ₘ η := by ext s hs From 8a3e826473bbeb81aacabddc17eebdbca40b93f8 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Fri, 8 Nov 2024 01:06:48 +0100 Subject: [PATCH 03/10] rename `Fst'` and `Snd'` to `domFst` and `domSnd` --- Mathlib/Probability/Kernel/Composition.lean | 88 ++++++++++----------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index dc9246345f09c..dd679610fdcb4 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -1026,95 +1026,95 @@ lemma snd_swapRight (κ : Kernel α (β × γ)) : snd (swapRight κ) = fst κ := end FstSnd -section Fst'Snd' +section domFstSnd variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} /-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for a given `b : β`. -/ -noncomputable def fst' (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := +noncomputable def domFst (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := comap κ (fun a ↦ (a, b)) (measurable_id.prod_mk measurable_const) -@[simp] theorem fst'_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : fst' κ b a = κ (a, b) := rfl +@[simp] theorem domFst_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : domFst κ b a = κ (a, b) := rfl -@[simp] lemma fst'_zero (b : β) : fst' (0 : Kernel (α × β) γ) b = 0 := by simp [fst'] +@[simp] lemma domFst_zero (b : β) : domFst (0 : Kernel (α × β) γ) b = 0 := by simp [domFst] -instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (fst' κ b) := by - rw [fst']; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (domFst κ b) := by + rw [domFst]; infer_instance -instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (fst' κ b) := by - rw [fst']; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (domFst κ b) := by + rw [domFst]; infer_instance -instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (fst' κ b) := by - rw [fst']; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (domFst κ b) := by + rw [domFst]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((fst' κ b) a) := by - rw [fst'_apply]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((domFst κ b) a) := by + rw [domFst_apply]; infer_instance -instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (fst' κ b)] : +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (domFst κ b)] : IsMarkovKernel κ := by refine ⟨fun _ ↦ ⟨?_⟩⟩ - rw [← fst'_apply, measure_univ] + rw [← domFst_apply, measure_univ] --I'm not sure this lemma is actually useful -lemma comap_fst' (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : - comap (fst' κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by +lemma comap_domFst (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : + comap (domFst κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by ext d s - rw [comap_apply, fst'_apply, comap_apply] + rw [comap_apply, domFst_apply, comap_apply] @[simp] -lemma fst'_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : - fst' (prodMkLeft α κ) b a = κ b := rfl +lemma domFst_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : + domFst (prodMkLeft α κ) b a = κ b := rfl @[simp] -lemma fst'_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : - fst' (prodMkRight β κ) b = κ := rfl +lemma domFst_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : + domFst (prodMkRight β κ) b = κ := rfl /-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for a given `a : α`. -/ -noncomputable def snd' (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := +noncomputable def domSnd (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := comap κ (fun b ↦ (a, b)) (measurable_const.prod_mk measurable_id) -@[simp] theorem snd'_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : snd' κ a b = κ (a, b) := rfl +@[simp] theorem domSnd_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : domSnd κ a b = κ (a, b) := rfl -@[simp] lemma snd'_zero (a : α) : snd' (0 : Kernel (α × β) γ) a = 0 := by simp [snd'] +@[simp] lemma domSnd_zero (a : α) : domSnd (0 : Kernel (α × β) γ) a = 0 := by simp [domSnd] -instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (snd' κ a) := by - rw [snd']; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (domSnd κ a) := by + rw [domSnd]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (snd' κ a) := by - rw [snd']; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (domSnd κ a) := by + rw [domSnd]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (snd' κ a) := by - rw [snd']; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (domSnd κ a) := by + rw [domSnd]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((snd' κ a) b) := by - rw [snd'_apply]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((domSnd κ a) b) := by + rw [domSnd_apply]; infer_instance -instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (snd' κ b)] : +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (domSnd κ b)] : IsMarkovKernel κ := by refine ⟨fun _ ↦ ⟨?_⟩⟩ - rw [← snd'_apply, measure_univ] + rw [← domSnd_apply, measure_univ] --I'm not sure this lemma is actually useful -lemma comap_snd' (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : - comap (snd' κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by +lemma comap_domSnd (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : + comap (domSnd κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by ext d s - rw [comap_apply, snd'_apply, comap_apply] + rw [comap_apply, domSnd_apply, comap_apply] @[simp] -lemma snd'_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : - snd' (prodMkLeft α κ) a = κ := rfl +lemma domSnd_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : + domSnd (prodMkLeft α κ) a = κ := rfl @[simp] -lemma snd'_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : - snd' (prodMkRight β κ) a b = κ a := rfl +lemma domSnd_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : + domSnd (prodMkRight β κ) a b = κ a := rfl -@[simp] lemma fst'_swapRight (κ : Kernel (α × β) γ) : fst' (swapLeft κ) = snd' κ := rfl +@[simp] lemma domFst_swapRight (κ : Kernel (α × β) γ) : domFst (swapLeft κ) = domSnd κ := rfl -@[simp] lemma snd'_swapRight (κ : Kernel (α × β) γ) : snd' (swapLeft κ) = fst' κ := rfl +@[simp] lemma domSnd_swapRight (κ : Kernel (α × β) γ) : domSnd (swapLeft κ) = domFst κ := rfl -end Fst'Snd' +end domFstSnd section Comp From f0770e51c078fce2b3b2740ac85b0cb583504673 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Fri, 8 Nov 2024 01:15:56 +0100 Subject: [PATCH 04/10] fix bug --- Mathlib/Probability/Kernel/MeasureCompProd.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Probability/Kernel/MeasureCompProd.lean b/Mathlib/Probability/Kernel/MeasureCompProd.lean index e3e4cb3a71c31..ef45d1e973686 100644 --- a/Mathlib/Probability/Kernel/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/MeasureCompProd.lean @@ -67,12 +67,12 @@ lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ] rw [Set.indicator_apply] split_ifs with ha <;> simp [ha] -lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_snd' {γ : Type*} +lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_domSnd {γ : Type*} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) : - (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.snd' η a) := by + (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.domSnd η a) := by ext s hs - simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.snd'_apply] + simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.domSnd_apply] rfl lemma compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η] From 30ec8f8516d0f248e2b7fe54bed3c7d38a49f9fb Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Fri, 8 Nov 2024 01:16:10 +0100 Subject: [PATCH 05/10] fix lint warning --- Mathlib/Probability/Kernel/Composition.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index dd679610fdcb4..e3fbc332658ac 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -1201,6 +1201,7 @@ variable {γ : Type*} {mγ : MeasurableSpace γ} noncomputable def prod (κ : Kernel α β) (η : Kernel α γ) : Kernel α (β × γ) := κ ⊗ₖ swapLeft (prodMkLeft β η) +@[inherit_doc] scoped[ProbabilityTheory] infixl:100 " ×ₖ " => ProbabilityTheory.Kernel.prod theorem prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] From 3d13c57e79297292853c7120279a6678027bcf7f Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Mon, 11 Nov 2024 22:33:36 +0100 Subject: [PATCH 06/10] rename `Fst` to `sectl` and `Snd` to `sectr` --- Mathlib/Probability/Kernel/Composition.lean | 88 +++++++++---------- .../Probability/Kernel/MeasureCompProd.lean | 6 +- 2 files changed, 47 insertions(+), 47 deletions(-) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index e3fbc332658ac..470b4500dc35e 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -1026,95 +1026,95 @@ lemma snd_swapRight (κ : Kernel α (β × γ)) : snd (swapRight κ) = fst κ := end FstSnd -section domFstSnd +section SectlSectr variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} /-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for a given `b : β`. -/ -noncomputable def domFst (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := +noncomputable def sectl (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := comap κ (fun a ↦ (a, b)) (measurable_id.prod_mk measurable_const) -@[simp] theorem domFst_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : domFst κ b a = κ (a, b) := rfl +@[simp] theorem sectl_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectl κ b a = κ (a, b) := rfl -@[simp] lemma domFst_zero (b : β) : domFst (0 : Kernel (α × β) γ) b = 0 := by simp [domFst] +@[simp] lemma sectl_zero (b : β) : sectl (0 : Kernel (α × β) γ) b = 0 := by simp [sectl] -instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (domFst κ b) := by - rw [domFst]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectl κ b) := by + rw [sectl]; infer_instance -instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (domFst κ b) := by - rw [domFst]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectl κ b) := by + rw [sectl]; infer_instance -instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (domFst κ b) := by - rw [domFst]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectl κ b) := by + rw [sectl]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((domFst κ b) a) := by - rw [domFst_apply]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectl κ b) a) := by + rw [sectl_apply]; infer_instance -instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (domFst κ b)] : +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectl κ b)] : IsMarkovKernel κ := by refine ⟨fun _ ↦ ⟨?_⟩⟩ - rw [← domFst_apply, measure_univ] + rw [← sectl_apply, measure_univ] --I'm not sure this lemma is actually useful -lemma comap_domFst (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : - comap (domFst κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by +lemma comap_sectl (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : + comap (sectl κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by ext d s - rw [comap_apply, domFst_apply, comap_apply] + rw [comap_apply, sectl_apply, comap_apply] @[simp] -lemma domFst_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : - domFst (prodMkLeft α κ) b a = κ b := rfl +lemma sectl_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : + sectl (prodMkLeft α κ) b a = κ b := rfl @[simp] -lemma domFst_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : - domFst (prodMkRight β κ) b = κ := rfl +lemma sectl_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : + sectl (prodMkRight β κ) b = κ := rfl /-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for a given `a : α`. -/ -noncomputable def domSnd (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := +noncomputable def sectr (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := comap κ (fun b ↦ (a, b)) (measurable_const.prod_mk measurable_id) -@[simp] theorem domSnd_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : domSnd κ a b = κ (a, b) := rfl +@[simp] theorem sectr_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectr κ a b = κ (a, b) := rfl -@[simp] lemma domSnd_zero (a : α) : domSnd (0 : Kernel (α × β) γ) a = 0 := by simp [domSnd] +@[simp] lemma sectr_zero (a : α) : sectr (0 : Kernel (α × β) γ) a = 0 := by simp [sectr] -instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (domSnd κ a) := by - rw [domSnd]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectr κ a) := by + rw [sectr]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (domSnd κ a) := by - rw [domSnd]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectr κ a) := by + rw [sectr]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (domSnd κ a) := by - rw [domSnd]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectr κ a) := by + rw [sectr]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((domSnd κ a) b) := by - rw [domSnd_apply]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectr κ a) b) := by + rw [sectr_apply]; infer_instance -instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (domSnd κ b)] : +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectr κ b)] : IsMarkovKernel κ := by refine ⟨fun _ ↦ ⟨?_⟩⟩ - rw [← domSnd_apply, measure_univ] + rw [← sectr_apply, measure_univ] --I'm not sure this lemma is actually useful -lemma comap_domSnd (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : - comap (domSnd κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by +lemma comap_sectr (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : + comap (sectr κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by ext d s - rw [comap_apply, domSnd_apply, comap_apply] + rw [comap_apply, sectr_apply, comap_apply] @[simp] -lemma domSnd_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : - domSnd (prodMkLeft α κ) a = κ := rfl +lemma sectr_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : + sectr (prodMkLeft α κ) a = κ := rfl @[simp] -lemma domSnd_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : - domSnd (prodMkRight β κ) a b = κ a := rfl +lemma sectr_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : + sectr (prodMkRight β κ) a b = κ a := rfl -@[simp] lemma domFst_swapRight (κ : Kernel (α × β) γ) : domFst (swapLeft κ) = domSnd κ := rfl +@[simp] lemma sectl_swapRight (κ : Kernel (α × β) γ) : sectl (swapLeft κ) = sectr κ := rfl -@[simp] lemma domSnd_swapRight (κ : Kernel (α × β) γ) : domSnd (swapLeft κ) = domFst κ := rfl +@[simp] lemma sectr_swapRight (κ : Kernel (α × β) γ) : sectr (swapLeft κ) = sectl κ := rfl -end domFstSnd +end SectlSectr section Comp diff --git a/Mathlib/Probability/Kernel/MeasureCompProd.lean b/Mathlib/Probability/Kernel/MeasureCompProd.lean index ef45d1e973686..ee87b56d012d8 100644 --- a/Mathlib/Probability/Kernel/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/MeasureCompProd.lean @@ -67,12 +67,12 @@ lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ] rw [Set.indicator_apply] split_ifs with ha <;> simp [ha] -lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_domSnd {γ : Type*} +lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectr {γ : Type*} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) : - (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.domSnd η a) := by + (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectr η a) := by ext s hs - simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.domSnd_apply] + simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.sectr_apply] rfl lemma compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η] From 904d9e3ce2c619974a4751c699add2d93f55f0d3 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Sun, 17 Nov 2024 10:20:15 +0100 Subject: [PATCH 07/10] change `sectl` and `sectr` to `sectL` and `sectR` --- Mathlib/Probability/Kernel/Composition.lean | 88 +++++++++---------- .../Probability/Kernel/MeasureCompProd.lean | 6 +- 2 files changed, 47 insertions(+), 47 deletions(-) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index 470b4500dc35e..dbb7023d5eb57 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -1026,95 +1026,95 @@ lemma snd_swapRight (κ : Kernel α (β × γ)) : snd (swapRight κ) = fst κ := end FstSnd -section SectlSectr +section sectLsectR variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} /-- Define a `Kernel α γ` from a `Kernel (α × β) γ` by taking the comap of `fun a ↦ (a, b)` for a given `b : β`. -/ -noncomputable def sectl (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := +noncomputable def sectL (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := comap κ (fun a ↦ (a, b)) (measurable_id.prod_mk measurable_const) -@[simp] theorem sectl_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectl κ b a = κ (a, b) := rfl +@[simp] theorem sectL_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectL κ b a = κ (a, b) := rfl -@[simp] lemma sectl_zero (b : β) : sectl (0 : Kernel (α × β) γ) b = 0 := by simp [sectl] +@[simp] lemma sectL_zero (b : β) : sectL (0 : Kernel (α × β) γ) b = 0 := by simp [sectL] -instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectl κ b) := by - rw [sectl]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectL κ b) := by + rw [sectL]; infer_instance -instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectl κ b) := by - rw [sectl]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectL κ b) := by + rw [sectL]; infer_instance -instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectl κ b) := by - rw [sectl]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectL κ b) := by + rw [sectL]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectl κ b) a) := by - rw [sectl_apply]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectL κ b) a) := by + rw [sectL_apply]; infer_instance -instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectl κ b)] : +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectL κ b)] : IsMarkovKernel κ := by refine ⟨fun _ ↦ ⟨?_⟩⟩ - rw [← sectl_apply, measure_univ] + rw [← sectL_apply, measure_univ] --I'm not sure this lemma is actually useful -lemma comap_sectl (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : - comap (sectl κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by +lemma comap_sectL (κ : Kernel (α × β) γ) (b : β) {f : δ → α} (hf : Measurable f) : + comap (sectL κ b) f hf = comap κ (fun d ↦ (f d, b)) (hf.prod_mk measurable_const) := by ext d s - rw [comap_apply, sectl_apply, comap_apply] + rw [comap_apply, sectL_apply, comap_apply] @[simp] -lemma sectl_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : - sectl (prodMkLeft α κ) b a = κ b := rfl +lemma sectL_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) {b : β} : + sectL (prodMkLeft α κ) b a = κ b := rfl @[simp] -lemma sectl_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : - sectl (prodMkRight β κ) b = κ := rfl +lemma sectL_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) : + sectL (prodMkRight β κ) b = κ := rfl /-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for a given `a : α`. -/ -noncomputable def sectr (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := +noncomputable def sectR (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := comap κ (fun b ↦ (a, b)) (measurable_const.prod_mk measurable_id) -@[simp] theorem sectr_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectr κ a b = κ (a, b) := rfl +@[simp] theorem sectR_apply (κ : Kernel (α × β) γ) (b : β) (a : α) : sectR κ a b = κ (a, b) := rfl -@[simp] lemma sectr_zero (a : α) : sectr (0 : Kernel (α × β) γ) a = 0 := by simp [sectr] +@[simp] lemma sectR_zero (a : α) : sectR (0 : Kernel (α × β) γ) a = 0 := by simp [sectR] -instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectr κ a) := by - rw [sectr]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectR κ a) := by + rw [sectR]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectr κ a) := by - rw [sectr]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectR κ a) := by + rw [sectR]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectr κ a) := by - rw [sectr]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectR κ a) := by + rw [sectR]; infer_instance -instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectr κ a) b) := by - rw [sectr_apply]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) (b : β) [NeZero (κ (a, b))] : NeZero ((sectR κ a) b) := by + rw [sectR_apply]; infer_instance -instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectr κ b)] : +instance (priority := 100) {κ : Kernel (α × β) γ} [∀ b, IsMarkovKernel (sectR κ b)] : IsMarkovKernel κ := by refine ⟨fun _ ↦ ⟨?_⟩⟩ - rw [← sectr_apply, measure_univ] + rw [← sectR_apply, measure_univ] --I'm not sure this lemma is actually useful -lemma comap_sectr (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : - comap (sectr κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by +lemma comap_sectR (κ : Kernel (α × β) γ) (a : α) {f : δ → β} (hf : Measurable f) : + comap (sectR κ a) f hf = comap κ (fun d ↦ (a, f d)) (measurable_const.prod_mk hf) := by ext d s - rw [comap_apply, sectr_apply, comap_apply] + rw [comap_apply, sectR_apply, comap_apply] @[simp] -lemma sectr_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : - sectr (prodMkLeft α κ) a = κ := rfl +lemma sectR_prodMkLeft (α : Type*) [MeasurableSpace α] (κ : Kernel β γ) (a : α) : + sectR (prodMkLeft α κ) a = κ := rfl @[simp] -lemma sectr_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : - sectr (prodMkRight β κ) a b = κ a := rfl +lemma sectR_prodMkRight (β : Type*) [MeasurableSpace β] (κ : Kernel α γ) (b : β) {a : α} : + sectR (prodMkRight β κ) a b = κ a := rfl -@[simp] lemma sectl_swapRight (κ : Kernel (α × β) γ) : sectl (swapLeft κ) = sectr κ := rfl +@[simp] lemma sectL_swapRight (κ : Kernel (α × β) γ) : sectL (swapLeft κ) = sectR κ := rfl -@[simp] lemma sectr_swapRight (κ : Kernel (α × β) γ) : sectr (swapLeft κ) = sectl κ := rfl +@[simp] lemma sectR_swapRight (κ : Kernel (α × β) γ) : sectR (swapLeft κ) = sectL κ := rfl -end SectlSectr +end sectLsectR section Comp diff --git a/Mathlib/Probability/Kernel/MeasureCompProd.lean b/Mathlib/Probability/Kernel/MeasureCompProd.lean index ee87b56d012d8..5566d9fda5429 100644 --- a/Mathlib/Probability/Kernel/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/MeasureCompProd.lean @@ -67,12 +67,12 @@ lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ] rw [Set.indicator_apply] split_ifs with ha <;> simp [ha] -lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectr {γ : Type*} +lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Type*} {mγ : MeasurableSpace γ} (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) : - (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectr η a) := by + (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectR η a) := by ext s hs - simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.sectr_apply] + simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.sectR_apply] rfl lemma compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η] From 1ca07649d2d26f0570ee9067bbaa293aefc1bfa7 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Thu, 21 Nov 2024 16:25:12 +0100 Subject: [PATCH 08/10] add `IsZeroOrMarkovKernel.comap` --- Mathlib/Probability/Kernel/Composition.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index dbb7023d5eb57..7980ce9ef724a 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -697,6 +697,12 @@ instance IsMarkovKernel.comap (κ : Kernel α β) [IsMarkovKernel κ] (hg : Meas IsMarkovKernel (comap κ g hg) := ⟨fun a => ⟨by rw [comap_apply' κ hg a Set.univ, measure_univ]⟩⟩ +instance IsZeroOrMarkovKernel.comap (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (hg : Measurable g) : + IsZeroOrMarkovKernel (comap κ g hg) := by + rcases eq_zero_or_isMarkovKernel κ with rfl | h + · simp only [comap_zero]; infer_instance + · have := IsMarkovKernel.comap κ hg; infer_instance + instance IsFiniteKernel.comap (κ : Kernel α β) [IsFiniteKernel κ] (hg : Measurable g) : IsFiniteKernel (comap κ g hg) := by refine ⟨⟨IsFiniteKernel.bound κ, IsFiniteKernel.bound_lt_top κ, fun a => ?_⟩⟩ From 856d1fbb210a6b885f6b367545013d7d3f463f2e Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Thu, 21 Nov 2024 16:26:00 +0100 Subject: [PATCH 09/10] apply suggestion: add instances of `IsZeroOrMarkovKernel` for `sectL` and `sectR` --- Mathlib/Probability/Kernel/Composition.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index 7980ce9ef724a..0d7530c3d6fd4 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -1048,6 +1048,10 @@ noncomputable def sectL (κ : Kernel (α × β) γ) (b : β) : Kernel α γ := instance (κ : Kernel (α × β) γ) (b : β) [IsMarkovKernel κ] : IsMarkovKernel (sectL κ b) := by rw [sectL]; infer_instance +instance (κ : Kernel (α × β) γ) (b : β) [IsZeroOrMarkovKernel κ] : + IsZeroOrMarkovKernel (sectL κ b) := by + rw [sectL]; infer_instance + instance (κ : Kernel (α × β) γ) (b : β) [IsFiniteKernel κ] : IsFiniteKernel (sectL κ b) := by rw [sectL]; infer_instance @@ -1088,6 +1092,10 @@ noncomputable def sectR (κ : Kernel (α × β) γ) (a : α) : Kernel β γ := instance (κ : Kernel (α × β) γ) (a : α) [IsMarkovKernel κ] : IsMarkovKernel (sectR κ a) := by rw [sectR]; infer_instance +instance (κ : Kernel (α × β) γ) (a : α) [IsZeroOrMarkovKernel κ] : + IsZeroOrMarkovKernel (sectR κ a) := by + rw [sectR]; infer_instance + instance (κ : Kernel (α × β) γ) (a : α) [IsFiniteKernel κ] : IsFiniteKernel (sectR κ a) := by rw [sectR]; infer_instance From 3c46787a4dfbff19eaf1e024b0a8b150e44b17a9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 3 Jan 2025 09:23:45 +0100 Subject: [PATCH 10/10] fix --- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean index 3703586ef8cb7..64933b8111dc2 100644 --- a/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean +++ b/Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean @@ -78,7 +78,7 @@ lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Typ [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) : (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectR η a) := by ext s hs - simp_rw [Kernel.compProd_apply _ _ _ hs, compProd_apply hs, Kernel.sectR_apply] + simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply] rfl lemma compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η]