feat(Kernel): map (κ ×ₖ η) Prod.swap = η ×ₖ κ

and similar lemmas.

From PFR

Co-authored-by: Rémy Degenne

Mathlib/Probability/Kernel/Composition.lean

@@ -208,8 +208,8 @@ theorem compProd_of_not_isSFiniteKernel_right (κ : Kernel α β) (η : Kernel (
   rw [compProd, dif_neg]
   simp [h]
 
-theorem compProd_apply (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
-    [IsSFiniteKernel η] (a : α) (hs : MeasurableSet s) :
+theorem compProd_apply (hs : MeasurableSet s) (κ : Kernel α β) [IsSFiniteKernel κ]
+    (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α) :
     (κ ⊗ₖ η) a s = ∫⁻ b, η (a, b) {c | (b, c) ∈ s} ∂κ a :=
   compProd_apply_eq_compProdFun κ η a hs
 
@@ -229,7 +229,7 @@ lemma compProd_zero_left (κ : Kernel (α × β) γ) :
     (0 : Kernel α β) ⊗ₖ κ = 0 := by
   by_cases h : IsSFiniteKernel κ
   · ext a s hs
-    rw [Kernel.compProd_apply _ _ _ hs]
+    rw [Kernel.compProd_apply hs]
     simp
   · rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h]
 
@@ -238,10 +238,44 @@ lemma compProd_zero_right (κ : Kernel α β) (γ : Type*) {mγ : MeasurableSpac
     κ ⊗ₖ (0 : Kernel (α × β) γ) = 0 := by
   by_cases h : IsSFiniteKernel κ
   · ext a s hs
-    rw [Kernel.compProd_apply _ _ _ hs]
+    rw [Kernel.compProd_apply hs]
     simp
   · rw [Kernel.compProd_of_not_isSFiniteKernel_left _ _ h]
 
+lemma compProd_preimage_fst {s : Set β} (hs : MeasurableSet s) (κ : Kernel α β)
+    (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsMarkovKernel η] (x : α) :
+    (κ ⊗ₖ η) x (Prod.fst ⁻¹' s) = κ x s := by
+  rw [compProd_apply (measurable_fst hs)]
+  simp only [Set.mem_preimage]
+  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]
+
+lemma compProd_deterministic_apply [MeasurableSingletonClass γ] {f : α × β → γ} (hf : Measurable f)
+    {s : Set (β × γ)} (hs : MeasurableSet s) (κ : Kernel α β) [IsSFiniteKernel κ] (x : α) :
+    (κ ⊗ₖ deterministic f hf) x s = κ x {b | (b, f (x, b)) ∈ s} := by
+  rw [compProd_apply hs]
+  simp only [deterministic_apply, measurableSet_setOf, Set.mem_setOf_eq, Measure.dirac_apply]
+  classical
+  simp only [Set.mem_setOf_eq, Set.indicator_apply, Pi.one_apply]
+  let t := {b | (b, f (x, b)) ∈ s}
+  have ht : MeasurableSet t := (measurable_id.prod_mk (hf.comp measurable_prod_mk_left)) hs
+  rw [← lintegral_add_compl _ ht]
+  convert add_zero _
+  · suffices ∀ b ∈ tᶜ, (if (b, f (x, b)) ∈ s then (1 : ℝ≥0∞) else 0) = 0 by
+      rw [setLIntegral_congr_fun ht.compl (ae_of_all _ this), lintegral_zero]
+    intro b hb
+    simp only [t, Set.mem_compl_iff, Set.mem_setOf_eq] at hb
+    simp [hb]
+  · suffices ∀ b ∈ t, (if (b, f (x, b)) ∈ s then (1 : ℝ≥0∞) else 0) = 1 by
+      rw [setLIntegral_congr_fun ht (ae_of_all _ this), setLIntegral_one]
+    intro b hb
+    simp only [t, Set.mem_setOf_eq] at hb
+    simp [hb]
+
 section Ae
 
 /-! ### `ae` filter of the composition-product -/
@@ -257,14 +291,14 @@ theorem ae_kernel_lt_top (a : α) (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
   have ht : MeasurableSet t := measurableSet_toMeasurable _ _
   have h2t : (κ ⊗ₖ η) a t ≠ ∞ := by rwa [measure_toMeasurable]
   have ht_lt_top : ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' t) < ∞ := by
-    rw [Kernel.compProd_apply _ _ _ ht] at h2t
+    rw [Kernel.compProd_apply ht] at h2t
     exact ae_lt_top (Kernel.measurable_kernel_prod_mk_left' ht a) h2t
   filter_upwards [ht_lt_top] with b hb
   exact (this b).trans_lt hb
 
 theorem compProd_null (a : α) (hs : MeasurableSet s) :
     (κ ⊗ₖ η) a s = 0 ↔ (fun b => η (a, b) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0 := by
-  rw [Kernel.compProd_apply _ _ _ hs, lintegral_eq_zero_iff]
+  rw [Kernel.compProd_apply hs, lintegral_eq_zero_iff]
   · rfl
   · exact Kernel.measurable_kernel_prod_mk_left' hs a
 
@@ -308,8 +342,8 @@ variable {κ : Kernel α β} [IsSFiniteKernel κ] {η : Kernel (α × β) γ} [I
 theorem compProd_restrict {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
     Kernel.restrict κ hs ⊗ₖ Kernel.restrict η ht = Kernel.restrict (κ ⊗ₖ η) (hs.prod ht) := by
   ext a u hu
-  rw [compProd_apply _ _ _ hu, restrict_apply' _ _ _ hu,
-    compProd_apply _ _ _ (hu.inter (hs.prod ht))]
+  rw [compProd_apply hu, restrict_apply' _ _ _ hu,
+    compProd_apply (hu.inter (hs.prod ht))]
   simp only [Kernel.restrict_apply, Measure.restrict_apply' ht, Set.mem_inter_iff,
     Set.prod_mk_mem_set_prod_eq]
   have :
@@ -383,7 +417,7 @@ theorem lintegral_compProd' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kerne
     simp (config := { unfoldPartialApp := true }) only [SimpleFunc.const_zero,
       SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
       Set.piecewise_eq_indicator, Function.const, lintegral_indicator_const hs]
-    rw [compProd_apply κ η _ hs, ← lintegral_const_mul c _]
+    rw [compProd_apply hs, ← lintegral_const_mul c _]
     swap
     · exact (measurable_kernel_prod_mk_left ((measurable_fst.snd.prod_mk measurable_snd) hs)).comp
         measurable_prod_mk_left
@@ -485,19 +519,16 @@ theorem compProd_eq_sum_compProd_right (κ : Kernel α β) (η : Kernel (α × 
   rw [Kernel.sum_comm]
 
 instance IsMarkovKernel.compProd (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel (α × β) γ)
-    [IsMarkovKernel η] : IsMarkovKernel (κ ⊗ₖ η) :=
-  ⟨fun a =>
-    ⟨by
-      rw [compProd_apply κ η a MeasurableSet.univ]
-      simp only [Set.mem_univ, Set.setOf_true, measure_univ, lintegral_one]⟩⟩
+    [IsMarkovKernel η] : IsMarkovKernel (κ ⊗ₖ η) where
+  isProbabilityMeasure a := ⟨by simp [compProd_apply MeasurableSet.univ]⟩
 
 theorem compProd_apply_univ_le (κ : Kernel α β) (η : Kernel (α × β) γ) [IsFiniteKernel η] (a : α) :
     (κ ⊗ₖ η) a Set.univ ≤ κ a Set.univ * IsFiniteKernel.bound η := by
   by_cases hκ : IsSFiniteKernel κ
   swap
   · rw [compProd_of_not_isSFiniteKernel_left _ _ hκ]
     simp
-  rw [compProd_apply κ η a MeasurableSet.univ]
+  rw [compProd_apply MeasurableSet.univ]
   simp only [Set.mem_univ, Set.setOf_true]
   let Cη := IsFiniteKernel.bound η
   calc
@@ -530,13 +561,13 @@ instance IsSFiniteKernel.compProd (κ : Kernel α β) (η : Kernel (α × β) γ
 
 lemma compProd_add_left (μ κ : Kernel α β) (η : Kernel (α × β) γ)
     [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
-    (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η := by ext _ _ hs; simp [compProd_apply _ _ _ hs]
+    (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η := by ext _ _ hs; simp [compProd_apply hs]
 
 lemma compProd_add_right (μ : Kernel α β) (κ η : Kernel (α × β) γ)
     [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] :
     μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η := by
   ext a s hs
-  simp only [compProd_apply _ _ _ hs, coe_add, Pi.add_apply, Measure.coe_add]
+  simp only [compProd_apply hs, coe_add, Pi.add_apply, Measure.coe_add]
   rw [lintegral_add_left]
   exact measurable_kernel_prod_mk_left' hs a
 
@@ -545,7 +576,7 @@ lemma comapRight_compProd_id_prod {δ : Type*} {mδ : MeasurableSpace δ}
     {f : δ → γ} (hf : MeasurableEmbedding f) :
     comapRight (κ ⊗ₖ η) (MeasurableEmbedding.id.prod_mk hf) = κ ⊗ₖ (comapRight η hf) := by
   ext a t ht
-  rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply _ _ _ ht]
+  rw [comapRight_apply' _ _ _ ht, compProd_apply, compProd_apply ht]
   swap; · exact (MeasurableEmbedding.id.prod_mk hf).measurableSet_image.mpr ht
   refine lintegral_congr (fun b ↦ ?_)
   simp only [id_eq, Set.mem_image, Prod.mk.injEq, Prod.exists]
@@ -1136,8 +1167,7 @@ section Prod
 
 /-! ### Product of two kernels -/
 
-
-variable {γ : Type*} {mγ : MeasurableSpace γ}
+variable {γ δ : Type*} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
 
 /-- Product of two kernels. This is meaningful only when the kernels are s-finite. -/
 noncomputable def prod (κ : Kernel α β) (η : Kernel α γ) : Kernel α (β × γ) :=
@@ -1148,7 +1178,7 @@ scoped[ProbabilityTheory] infixl:100 " ×ₖ " => ProbabilityTheory.Kernel.prod
 theorem prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
     (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) :
     (κ ×ₖ η) a s = ∫⁻ b : β, (η a) {c : γ | (b, c) ∈ s} ∂κ a := by
-  simp_rw [prod, compProd_apply _ _ _ hs, swapLeft_apply _ _, prodMkLeft_apply, Prod.swap_prod_mk]
+  simp_rw [prod, compProd_apply hs, swapLeft_apply _ _, prodMkLeft_apply, Prod.swap_prod_mk]
 
 lemma prod_apply (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
     (a : α) :
@@ -1192,6 +1222,28 @@ instance IsSFiniteKernel.prod (κ : Kernel α β) (η : Kernel α γ) :
     snd (κ ×ₖ η) = η := by
   ext x; simp [snd_apply, prod_apply]
 
+lemma comap_prod_swap (κ : Kernel α β) (η : Kernel γ δ) [IsFiniteKernel κ] [IsFiniteKernel η] :
+    comap (prodMkRight α η ×ₖ prodMkLeft γ κ) Prod.swap measurable_swap
+      = map (prodMkRight γ κ ×ₖ prodMkLeft α η) Prod.swap := by
+  rw [ext_fun_iff]
+  intro x f hf
+  rw [lintegral_comap, lintegral_map _ measurable_swap _ hf, lintegral_prod _ _ _ hf,
+    lintegral_prod]
+  swap; · exact hf.comp measurable_swap
+  simp only [prodMkRight_apply, Prod.fst_swap, Prod.swap_prod_mk, lintegral_prodMkLeft,
+    Prod.snd_swap]
+  refine (lintegral_lintegral_swap ?_).symm
+  exact (hf.comp measurable_swap).aemeasurable
+
+lemma map_prod_swap (κ : Kernel α β) (η : Kernel α γ) [IsMarkovKernel κ] [IsMarkovKernel η] :
+    map (κ ×ₖ η) Prod.swap = η ×ₖ κ := by
+  rw [ext_fun_iff]
+  intro x f hf
+  rw [lintegral_map _ measurable_swap _ hf, lintegral_prod, lintegral_prod _ _ _ hf]
+  swap; · exact hf.comp measurable_swap
+  refine (lintegral_lintegral_swap ?_).symm
+  exact hf.aemeasurable
+
 lemma deterministic_prod_deterministic {f : α → β} {g : α → γ}
     (hf : Measurable f) (hg : Measurable g) :
     deterministic f hf ×ₖ deterministic g hg

Mathlib/Probability/Kernel/Disintegration/Basic.lean

@@ -163,7 +163,7 @@ instance condKernelCountable.instIsCondKernel [∀ a, IsMarkovKernel (κCond a)]
   constructor
   ext a s hs
   conv_rhs => rw [← (κ a).disintegrate (κCond a)]
-  simp_rw [compProd_apply _ _ _ hs, condKernelCountable_apply, Measure.compProd_apply hs]
+  simp_rw [compProd_apply hs, condKernelCountable_apply, Measure.compProd_apply hs]
   congr
 
 end Countable

Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

@@ -684,7 +684,7 @@ lemma lintegral_toKernel_mem [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν)
 lemma compProd_toKernel [IsFiniteKernel κ] [IsSFiniteKernel ν] (hf : IsCondKernelCDF f κ ν) :
     ν ⊗ₖ hf.toKernel f = κ := by
   ext a s hs
-  rw [Kernel.compProd_apply _ _ _ hs, lintegral_toKernel_mem hf a hs]
+  rw [Kernel.compProd_apply hs, lintegral_toKernel_mem hf a hs]
 
 end
 

Mathlib/Probability/Kernel/Disintegration/Integral.lean

@@ -39,14 +39,14 @@ variable [CountableOrCountablyGenerated α β] {κ : Kernel α (β × Ω)} [IsFi
 lemma lintegral_condKernel_mem (a : α) {s : Set (β × Ω)} (hs : MeasurableSet s) :
     ∫⁻ x, Kernel.condKernel κ (a, x) {y | (x, y) ∈ s} ∂(Kernel.fst κ a) = κ a s := by
   conv_rhs => rw [← κ.disintegrate κ.condKernel]
-  simp_rw [Kernel.compProd_apply _ _ _ hs]
+  simp_rw [Kernel.compProd_apply hs]
 
 lemma setLIntegral_condKernel_eq_measure_prod (a : α) {s : Set β} (hs : MeasurableSet s)
     {t : Set Ω} (ht : MeasurableSet t) :
     ∫⁻ b in s, Kernel.condKernel κ (a, b) t ∂(Kernel.fst κ a) = κ a (s ×ˢ t) := by
   have : κ a (s ×ˢ t) = (Kernel.fst κ ⊗ₖ Kernel.condKernel κ) a (s ×ˢ t) := by
     congr; exact (κ.disintegrate _).symm
-  rw [this, Kernel.compProd_apply _ _ _ (hs.prod ht)]
+  rw [this, Kernel.compProd_apply (hs.prod ht)]
   classical
   have : ∀ b, Kernel.condKernel κ (a, b) {c | (b, c) ∈ s ×ˢ t}
       = s.indicator (fun b ↦ Kernel.condKernel κ (a, b) t) b := by

Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

@@ -259,7 +259,7 @@ lemma compProd_fst_borelMarkovFromReal_eq_comapRight_compProd
     congr
   rw [h_fst]
   ext a t ht : 2
-  simp_rw [compProd_apply _ _ _ ht]
+  simp_rw [compProd_apply ht]
   refine lintegral_congr_ae ?_
   have h_ae : ∀ᵐ t ∂(fst κ a), (a, t) ∈ {p : α × β | η p (range e)ᶜ = 0} := by
     rw [← h_fst]

Mathlib/Probability/Kernel/Disintegration/Unique.lean

@@ -134,7 +134,7 @@ lemma Kernel.apply_eq_measure_condKernel_of_compProd_eq
   have : ρ a = (ρ a).fst ⊗ₘ Kernel.comap κ (fun b ↦ (a, b)) measurable_prod_mk_left := by
     ext s hs
     conv_lhs => rw [← hκ]
-    rw [Measure.compProd_apply hs, Kernel.compProd_apply _ _ _ hs]
+    rw [Measure.compProd_apply hs, Kernel.compProd_apply hs]
     rfl
   have h := eq_condKernel_of_measure_eq_compProd _ this
   rw [Kernel.fst_apply]

Mathlib/Probability/Kernel/IntegralCompProd.lean

@@ -53,7 +53,7 @@ theorem hasFiniteIntegral_prod_mk_left (a : α) {s : Set (β × γ)} (h2s : (κ
       filter_upwards [ae_kernel_lt_top a h2s] with b hb
       rw [ofReal_toReal hb.ne]
       exact measure_mono (preimage_mono (subset_toMeasurable _ _))
-    _ ≤ (κ ⊗ₖ η) a t := le_compProd_apply _ _ _ _
+    _ ≤ (κ ⊗ₖ η) a t := le_compProd_apply _
     _ = (κ ⊗ₖ η) a s := measure_toMeasurable s
     _ < ⊤ := h2s.lt_top
 
@@ -234,7 +234,7 @@ theorem integral_compProd :
     rotate_left
     · exact (Kernel.measurable_kernel_prod_mk_left' hs _).aemeasurable
     · exact ae_kernel_lt_top a h2s.ne
-    rw [Kernel.compProd_apply _ _ _ hs]
+    rw [Kernel.compProd_apply hs]
     rfl
   · intro f g _ i_f i_g hf hg
     simp_rw [integral_add' i_f i_g, Kernel.integral_integral_add' i_f i_g, hf, hg]

Mathlib/Probability/Kernel/MeasureCompProd.lean

@@ -55,7 +55,7 @@ lemma compProd_of_not_isSFiniteKernel (μ : Measure α) (κ : Kernel α β) (h :
 
 lemma compProd_apply [SFinite μ] [IsSFiniteKernel κ] {s : Set (α × β)} (hs : MeasurableSet s) :
     (μ ⊗ₘ κ) s = ∫⁻ a, κ a (Prod.mk a ⁻¹' s) ∂μ := by
-  simp_rw [compProd, Kernel.compProd_apply _ _ _ hs, Kernel.const_apply, Kernel.prodMkLeft_apply']
+  simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']
   rfl
 
 lemma compProd_apply_prod [SFinite μ] [IsSFiniteKernel κ]