Theorem ProbabilityTheory.ae_toKernel_eq_one

Modification history

2024-04-16 12:43

Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean

feat(Probability/Kernel): disintegration of finite kernels (#10603) …

Deleted ProbabilityTheory.ae_toKernel_eq_one View on Github →

2024-03-17 17:51

Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean

feat(Probability/Kernel): build a kernel from a kernel CDF (#11209) …

Added ProbabilityTheory.ae_toKernel_eq_one View on Github →