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

ProbabilityTheory.Kernel.Measure.compProd_compProd

PFR.ForMathlib.Entropy.Kernel.MutualInfo · PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean:82 to 94

Mathematical statement

Exact Lean statement

lemma Measure.compProd_compProd (μ : Measure T)
    (ξ : Kernel T S) [IsSFiniteKernel ξ] (κ : Kernel (T × S) U) [IsSFiniteKernel κ] :
    μ ⊗ₘ (ξ ⊗ₖ κ) = (μ ⊗ₘ ξ ⊗ₘ κ).map MeasurableEquiv.prodAssoc

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Measure.compProd_compProd (μ : Measure T)    (ξ : Kernel T S) [IsSFiniteKernel ξ] (κ : Kernel (T × S) U) [IsSFiniteKernel κ] :    μ ⊗ₘ (ξ ⊗ₖ κ) = (μ ⊗ₘ ξ ⊗ₘ κ).map MeasurableEquiv.prodAssoc := by  by_cases hμ : SFinite μ; swap  · simp [Measure.compProd_of_not_sfinite _ _ hμ]  ext s hs  rw [Measure.compProd_apply hs, Measure.map_apply MeasurableEquiv.prodAssoc.measurable hs,    Measure.compProd_apply (MeasurableEquiv.prodAssoc.measurable hs),    Measure.lintegral_compProd]  swap; · exact measurable_kernel_prodMk_left (MeasurableEquiv.prodAssoc.measurable hs)  congr with a  rw [compProd_apply (measurable_prodMk_left hs)]  congr