Commit 2024-10-20 07:37 2f60fa67

View on Github →

feat(Kernel): map (κ ×ₖ η) Prod.swap = η ×ₖ κ (#17920) and similar lemmas. From PFR

Estimated changes

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.Kernel.comap_prod_swap

modified theorem ProbabilityTheory.Kernel.compProd_apply

added theorem ProbabilityTheory.Kernel.compProd_deterministic_apply

added theorem ProbabilityTheory.Kernel.compProd_preimage_fst

added theorem ProbabilityTheory.Kernel.map_prod_swap

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Integral.lean

Modified Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

Modified Mathlib/Probability/Kernel/Disintegration/Unique.lean

Modified Mathlib/Probability/Kernel/IntegralCompProd.lean

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean