Theorem MeasureTheory.StronglyMeasurable.integral_condDistrib

Modification history

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