Commit 2025-09-26 12:24 cffe679e

View on Github →

feat(Probability): lemmas about composition of kernels and measures (#29552) From the LeanBandits project.

Estimated changes

Modified Mathlib/Probability/ConditionalProbability.lean

added theorem ProbabilityTheory.ae_cond_of_forall_mem

Modified Mathlib/Probability/Kernel/Composition/Lemmas.lean

added theorem MeasureTheory.Measure.compProd_map

modified theorem MeasureTheory.Measure.parallelComp_comp_compProd

Modified Mathlib/Probability/Kernel/Composition/MeasureComp.lean

added theorem MeasureTheory.Measure.compProd_deterministic

added theorem MeasureTheory.Measure.comp_congr

added theorem MeasureTheory.Measure.copy_comp_map

Modified Mathlib/Probability/Kernel/Composition/ParallelComp.lean

added theorem ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic

added theorem ProbabilityTheory.Kernel.parallelComp_apply_prod

Modified Mathlib/Probability/Kernel/Composition/Prod.lean

added theorem ProbabilityTheory.Kernel.prod_apply_prod