From 0571c82877b7c2b508cbc9a39e041eb117d050b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Fri, 3 Jan 2025 14:55:08 +0000 Subject: [PATCH] feat: add fst_compProd_apply (#20429) Extract from the proof of `fst_compProd` a new lemma that applies more generally than Markov kernels. --- .../Probability/Kernel/Composition/Basic.lean | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/Mathlib/Probability/Kernel/Composition/Basic.lean b/Mathlib/Probability/Kernel/Composition/Basic.lean index 8fd4daf2faf96..fd06f343aa595 100644 --- a/Mathlib/Probability/Kernel/Composition/Basic.lean +++ b/Mathlib/Probability/Kernel/Composition/Basic.lean @@ -963,19 +963,20 @@ lemma fst_map_id_prod (κ : Kernel α β) {γ : Type*} {mγ : MeasurableSpace γ fst (map κ (fun a ↦ (a, f a))) = κ := by rw [fst_map_prod _ hf, Kernel.map_id'] +/-- If `η` is a Markov kernel, use instead `fst_compProd` to get `(κ ⊗ₖ η).fst = κ`. -/ +lemma fst_compProd_apply (κ : Kernel α β) (η : Kernel (α × β) γ) + [IsSFiniteKernel κ] [IsSFiniteKernel η] (x : α) {s : Set β} (hs : MeasurableSet s) : + (κ ⊗ₖ η).fst x s = ∫⁻ b, s.indicator (fun b ↦ η (x, b) Set.univ) b ∂(κ x) := by + rw [Kernel.fst_apply' _ _ hs, Kernel.compProd_apply] + swap; · exact measurable_fst hs + have h_eq b : η (x, b) {c | b ∈ s} = s.indicator (fun b ↦ η (x, b) Set.univ) b := by + by_cases hb : b ∈ s <;> simp [hb] + simp_rw [Set.mem_setOf_eq, h_eq] + @[simp] lemma fst_compProd (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] : fst (κ ⊗ₖ η) = κ := by - ext x s hs - rw [fst_apply' _ _ hs, compProd_apply] - swap; · exact measurable_fst hs - simp only [Set.mem_setOf_eq] - classical - have : ∀ b : β, η (x, b) {_c | b ∈ s} = s.indicator (fun _ ↦ 1) b := by - intro b - by_cases hb : b ∈ s <;> simp [hb] - simp_rw [this] - rw [lintegral_indicator_const hs, one_mul] + ext x s hs; simp [fst_compProd_apply, hs] lemma fst_prodMkLeft (δ : Type*) [MeasurableSpace δ] (κ : Kernel α (β × γ)) : fst (prodMkLeft δ κ) = prodMkLeft δ (fst κ) := rfl