Commit 2026-04-04 13:13 4ecd8b17

View on Github →

feat(Probability): Local and stable properties (#33375) Defines local and stable properties which is useful for local martingales.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.measure_iInter_of_ae_antitone

added theorem MeasureTheory.measure_iInter_of_ae_monotone

Created Mathlib/Probability/Process/LocalProperty.lean

added theorem ProbabilityTheory.IsLocalizingSequence.isPrelocalizingSequence_inf_extraction

added structure ProbabilityTheory.IsLocalizingSequence

added theorem ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf

added structure ProbabilityTheory.IsPreLocalizingSequence

added theorem ProbabilityTheory.IsStable.locally

added theorem ProbabilityTheory.IsStable.locally_and_iff

added theorem ProbabilityTheory.IsStable.locally_induction

added theorem ProbabilityTheory.IsStable.locally_induction₂

added theorem ProbabilityTheory.IsStable.locally_locally_iff

added theorem ProbabilityTheory.IsStable.locally_of_isPreLocalizingSequence

added def ProbabilityTheory.IsStable

added theorem ProbabilityTheory.Locally.isLocalizingSequence_localSeq

added theorem ProbabilityTheory.Locally.left

added def ProbabilityTheory.Locally.localSeq

added theorem ProbabilityTheory.Locally.mono

added theorem ProbabilityTheory.Locally.of_and

added theorem ProbabilityTheory.Locally.of_prop

added theorem ProbabilityTheory.Locally.right

added theorem ProbabilityTheory.Locally.stoppedProcess_localSeq

added def ProbabilityTheory.Locally

added theorem ProbabilityTheory.isLocalizingSequence_const_top