Commit 2023-06-18 07:17 d6bf8714

View on Github →

feat: port Probability.Process.Adapted (#5205)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Process/Adapted.lean

added theorem MeasureTheory.Adapted.progMeasurable_of_continuous

added theorem MeasureTheory.Adapted.progMeasurable_of_discrete

added theorem MeasureTheory.Adapted.stronglyMeasurable_le

added def MeasureTheory.Adapted

added theorem MeasureTheory.Filtration.adapted_natural

added theorem MeasureTheory.Predictable.adapted

added def MeasureTheory.ProgMeasurable

added theorem MeasureTheory.adapted_const

added theorem MeasureTheory.adapted_zero

added theorem MeasureTheory.progMeasurable_const

added theorem MeasureTheory.progMeasurable_of_tendsto'

added theorem MeasureTheory.progMeasurable_of_tendsto