Theorem ProbabilityTheory.stronglyMeasurable_integral_condDistrib

Modification history

2025-02-15 20:15
Mathlib/Probability/Kernel/CondDistrib.lean
feat: properties of condExpKernel and condDistrib (#21906)
Added ProbabilityTheory.stronglyMeasurable_integral_condDistribView on Github →