Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.Kernel.compProd_assoc'

PFR.ForMathlib.Entropy.Kernel.MutualInfo · PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean:68 to 80

Mathematical statement

Exact Lean statement

lemma compProd_assoc' (ξ : Kernel T S) [IsSFiniteKernel ξ]
    (κ : Kernel (T × S) U) [IsSFiniteKernel κ] (η : Kernel (T × S × U) V) [IsSFiniteKernel η] :
    map ((ξ ⊗ₖ κ) ⊗ₖ η) MeasurableEquiv.prodAssoc
      = ξ ⊗ₖ (κ ⊗ₖ (comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma compProd_assoc' (ξ : Kernel T S) [IsSFiniteKernel ξ]    (κ : Kernel (T × S) U) [IsSFiniteKernel κ] (η : Kernel (T × S × U) V) [IsSFiniteKernel η] :    map ((ξ ⊗ₖ κ) ⊗ₖ η) MeasurableEquiv.prodAssoc      = ξ ⊗ₖ (κ ⊗ₖ (comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable)) := by  ext x s hs  rw [map_apply' _ (by fun_prop) _ hs,    compProd_apply (MeasurableEquiv.prodAssoc.measurable hs),    compProd_apply hs, lintegral_compProd]  swap; · exact measurable_kernel_prodMk_left' (MeasurableEquiv.prodAssoc.measurable hs) _  congr with a  rw [compProd_apply]  swap; · exact measurable_prodMk_left hs  congr