Theorem ProbabilityTheory.compProd_map_condDistrib

Modification history

2026-08-26 08:21
Mathlib/Probability/Kernel/CondDistrib.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified ProbabilityTheory.compProd_map_condDistribView on Github →
2025-02-15 20:15
Mathlib/Probability/Kernel/CondDistrib.lean
feat: properties of condExpKernel and condDistrib (#21906)
Added ProbabilityTheory.compProd_map_condDistribView on Github →