Commit 2023-06-17 19:48 07e79d97

View on Github →

feat: port Probability.Process.Filtration (#5195)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Process/Filtration.lean

added theorem MeasureTheory.Filtration.coeFn_inf

added theorem MeasureTheory.Filtration.coeFn_sup

added def MeasureTheory.Filtration.const

added theorem MeasureTheory.Filtration.const_apply

added theorem MeasureTheory.Filtration.filtrationOfSet_eq_natural

added theorem MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd

added def MeasureTheory.Filtration.natural

added theorem MeasureTheory.Filtration.sInf_def

added theorem MeasureTheory.Filtration.sSup_def

added theorem MeasureTheory.Filtration.stronglyMeasurable_limitProcess

added theorem MeasureTheory.Filtration.stronglyMeasurable_limit_process'

added structure MeasureTheory.Filtration

added theorem MeasureTheory.Integrable.uniformIntegrable_condexp_filtration

added def MeasureTheory.filtrationOfSet

added theorem MeasureTheory.measurableSet_filtrationOfSet

added theorem MeasureTheory.measurableSet_filtration_of_set'

added theorem MeasureTheory.measurableSet_of_filtration