Theorem MeasureTheory.StronglyMeasurable.integral_condExpKernel

Modification history

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