Structures · Analysis
MeasureTheory.SigmaFiniteFiltration
A measure is σ-finite with respect to filtration if it is σ-finite with respect to all the sub-σ-algebra of the filtration.
- Defined in
- Mathlib.Probability.Process.Filtration
- Shape
- 2 explicit arguments · adds SigmaFinite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- MeasureTheory.Submartingale.expected_stoppedValue_mono
- MeasureTheory.Submartingale.setIntegral_le
- MeasureTheory.Martingale.eq_zero_of_predictable
- MeasureTheory.martingale_martingalePart
- MeasureTheory.submartingale_of_setIntegral_le
- MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range
- MeasureTheory.Submartingale.zero_le_of_predictable
- MeasureTheory.martingalePart_add_ae_eq
- MeasureTheory.Submartingale.stoppedProcess
- MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq
- MeasureTheory.martingale_condExp
- MeasureTheory.martingale_const_fun
- MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const
- MeasureTheory.Supermartingale.le_zero_of_predictable
- MeasureTheory.Supermartingale.setIntegral_le
- MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range
- MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range
- MeasureTheory.submartingale_of_expected_stoppedValue_mono
- MeasureTheory.submartingale_of_condExp_sub_nonneg
- MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le
- MeasureTheory.submartingale_iff_expected_stoppedValue_mono
- MeasureTheory.IsStronglyPredictable.predictablePart_eq
- MeasureTheory.Supermartingale.le_zero_of_predictable'
- MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const
- MeasureTheory.Submartingale.zero_le_of_predictable'
- MeasureTheory.Martingale.setIntegral_eq
- MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration
- MeasureTheory.Martingale.eq_zero_of_predictable'
- MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp
- MeasureTheory.SigmaFiniteFiltration.SigmaFinite
- MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable
- MeasureTheory.submartingale_iff_condExp_sub_nonneg
- MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time
- MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq
- MeasureTheory.IsPredictable.martingalePart_eq
- MeasureTheory.predictablePart_add_ae_eq
- MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time_of_le
- MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const
Ancestors0
No ancestors.