Commit 2024-08-25 12:38 1e574d7d

View on Github →

feat: remove Nonempty assumption in condexpKernel (#16138)

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

added theorem MeasureTheory.AEStronglyMeasurable'.of_subsingleton'

added theorem MeasureTheory.AEStronglyMeasurable'.of_subsingleton

Modified Mathlib/Probability/Independence/Conditional.lean

Modified Mathlib/Probability/Independence/ZeroOne.lean

modified theorem ProbabilityTheory.condIndep_biSup_compl

modified theorem ProbabilityTheory.condIndep_biSup_limsup

modified theorem ProbabilityTheory.condIndep_iSup_limsup

modified theorem ProbabilityTheory.condIndep_limsup_atBot_self

modified theorem ProbabilityTheory.condIndep_limsup_atTop_self

modified theorem ProbabilityTheory.condIndep_limsup_self

modified theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup

modified theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atBot

modified theorem ProbabilityTheory.condexp_zero_or_one_of_measurableSet_limsup_atTop

Modified Mathlib/Probability/Kernel/Condexp.lean

modified theorem ProbabilityTheory.condexpKernel_apply_eq_condDistrib

added theorem ProbabilityTheory.condexpKernel_eq