Theorem ProbabilityTheory.condExp_ae_eq_integral_condDistrib'

Modification history

2025-11-26 15:01
Mathlib/Probability/Kernel/CondDistrib.lean
feat(MeasureTheory): typeclass for measurability of equality (#31512) …
Modified ProbabilityTheory.condExp_ae_eq_integral_condDistrib'View on Github →
2025-01-22 13:49
Mathlib/Probability/Kernel/CondDistrib.lean
chore: rename `condexp` to `condExp` (#20930) …
Added ProbabilityTheory.condExp_ae_eq_integral_condDistrib'View on Github →