Commit 2026-01-16 21:07 a0ec512e

View on Github →

feat(Probability): add Adapted (#32882) Add Adapted which is a version of StronglyAdapted for Measurable rather than StronglyMeasurable. Also add theorems which state when one property implies the other and when they are equivalent.

depends on: #33063

Estimated changes

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/Centering.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/Probability/Process/Adapted.lean

added theorem MeasureTheory.Adapted.measurable_le

added theorem MeasureTheory.Adapted.stronglyAdapted

added def MeasureTheory.Adapted

added theorem MeasureTheory.StronglyAdapted.adapted

added theorem MeasureTheory.adapted_const'

added theorem MeasureTheory.adapted_const

added theorem MeasureTheory.stronglyAdapted_iff_adapted

Modified Mathlib/Probability/Process/Stopping.lean