Commit 2026-01-13 15:36 88a6f557

View on Github →

chore(Probability): Rename Adapted to StronglyAdapted (#33063) See discussion at: https://leanprover.zulipchat.com/#narrow/channel/509433-Brownian-motion/topic/Adapted.20Filtrations.20for.20Markov.20Chains.20and.20Markov.20Processes

Estimated changes

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

deleted theorem ProbabilityTheory.Kernel.adapted_densityProcess

added theorem ProbabilityTheory.Kernel.stronglyAdapted_densityProcess

Modified Mathlib/Probability/Martingale/Basic.lean

modified theorem MeasureTheory.martingale_nat

modified theorem MeasureTheory.martingale_of_setIntegral_eq_succ

modified theorem MeasureTheory.submartingale_nat

modified theorem MeasureTheory.supermartingale_nat

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

deleted theorem MeasureTheory.Adapted.isStoppingTime_leastGE

deleted theorem MeasureTheory.BorelCantelli.adapted_process

added theorem MeasureTheory.BorelCantelli.stronglyAdapted_process

added theorem MeasureTheory.StronglyAdapted.isStoppingTime_leastGE

Modified Mathlib/Probability/Martingale/Centering.lean

deleted theorem MeasureTheory.adapted_martingalePart

deleted theorem MeasureTheory.adapted_predictablePart'

deleted theorem MeasureTheory.adapted_predictablePart

modified theorem MeasureTheory.martingale_martingalePart

added theorem MeasureTheory.stronglyAdapted_martingalePart

added theorem MeasureTheory.stronglyAdapted_predictablePart'

added theorem MeasureTheory.stronglyAdapted_predictablePart

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Probability/Martingale/OptionalSampling.lean

Modified Mathlib/Probability/Martingale/OptionalStopping.lean

modified theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono

modified theorem MeasureTheory.submartingale_of_expected_stoppedValue_mono

Modified Mathlib/Probability/Martingale/Upcrossing.lean

deleted theorem MeasureTheory.Adapted.integrable_upcrossingsBefore

deleted theorem MeasureTheory.Adapted.isStoppingTime_crossing

deleted theorem MeasureTheory.Adapted.isStoppingTime_lowerCrossingTime

deleted theorem MeasureTheory.Adapted.isStoppingTime_upperCrossingTime

deleted theorem MeasureTheory.Adapted.measurable_upcrossings

deleted theorem MeasureTheory.Adapted.measurable_upcrossingsBefore

deleted theorem MeasureTheory.Adapted.upcrossingStrat_adapted

added theorem MeasureTheory.StronglyAdapted.integrable_upcrossingsBefore

added theorem MeasureTheory.StronglyAdapted.isStoppingTime_crossing

added theorem MeasureTheory.StronglyAdapted.isStoppingTime_lowerCrossingTime

added theorem MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime

added theorem MeasureTheory.StronglyAdapted.measurable_upcrossings

added theorem MeasureTheory.StronglyAdapted.measurable_upcrossingsBefore

added theorem MeasureTheory.StronglyAdapted.upcrossingStrat

Modified Mathlib/Probability/Moments/SubGaussian.lean

Modified Mathlib/Probability/Process/Adapted.lean

deleted theorem MeasureTheory.Adapted.progMeasurable_of_continuous

deleted theorem MeasureTheory.Adapted.progMeasurable_of_discrete

deleted theorem MeasureTheory.Adapted.stronglyMeasurable_le

deleted def MeasureTheory.Adapted

deleted theorem MeasureTheory.Filtration.adapted_natural

added theorem MeasureTheory.Filtration.stronglyAdapted_natural

deleted theorem MeasureTheory.Predictable.adapted

added theorem MeasureTheory.Predictable.stronglyAdapted

added theorem MeasureTheory.StronglyAdapted.progMeasurable_of_continuous

added theorem MeasureTheory.StronglyAdapted.progMeasurable_of_discrete

added theorem MeasureTheory.StronglyAdapted.stronglyMeasurable_le

added def MeasureTheory.StronglyAdapted

deleted theorem MeasureTheory.adapted_const'

deleted theorem MeasureTheory.adapted_const

deleted theorem MeasureTheory.adapted_zero'

deleted theorem MeasureTheory.adapted_zero

added theorem MeasureTheory.stronglyAdapted_const'

added theorem MeasureTheory.stronglyAdapted_const

added theorem MeasureTheory.stronglyAdapted_zero'

added theorem MeasureTheory.stronglyAdapted_zero

Modified Mathlib/Probability/Process/HittingTime.lean

Modified Mathlib/Probability/Process/Predictable.lean

Modified Mathlib/Probability/Process/Stopping.lean

deleted theorem MeasureTheory.Adapted.stoppedProcess

deleted theorem MeasureTheory.Adapted.stoppedProcess_of_discrete

deleted theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess

deleted theorem MeasureTheory.Adapted.stronglyMeasurable_stoppedProcess_of_discrete

deleted theorem MeasureTheory.ProgMeasurable.adapted_stoppedProcess

added theorem MeasureTheory.ProgMeasurable.stronglyAdapted_stoppedProcess

added theorem MeasureTheory.StronglyAdapted.stoppedProcess

added theorem MeasureTheory.StronglyAdapted.stoppedProcess_of_discrete

added theorem MeasureTheory.StronglyAdapted.stronglyMeasurable_stoppedProcess

added theorem MeasureTheory.StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete