Commit 2024-11-08 08:56 ca888d9e

View on Github →

feat: relation between conditional measure and conditional kernel/expectation (#18697)

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem MeasurableSpace.generateFrom_singleton_le

added theorem MeasureTheory.measurableSet_generateFrom_singleton_iff

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.ae_restrict_le

Modified Mathlib/Probability/Kernel/Condexp.lean

added theorem ProbabilityTheory.condexpKernel_singleton_ae_eq_cond

added theorem ProbabilityTheory.condexp_generateFrom_singleton

added theorem ProbabilityTheory.condexp_set_generateFrom_singleton