Theorems · Theorem · probability
MeasureTheory.Filtration.le
∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m) (i : ι),
↑f i ≤ m- Defined in
- Mathlib.Probability.Process.Filtration
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- Preorderstatement and proof · cited by 7,952
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.Filtration.seqstatement · cited by 184
- MeasureTheory.Filtration.le'proof · cited by 1
Cited by67
Results whose statement or proof uses this declaration.
- MeasureTheory.IsStoppingTime.measurableSpace_leproof · cited by 10
- MeasureTheory.IsStoppingTime.measurableSpace_le_of_leproof · cited by 5
- MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bddproof · cited by 4
- MeasureTheory.Submartingale.ae_tendsto_limitProcessproof · cited by 4
- MeasureTheory.Filtration.condExp_condExpstatement and proof · cited by 3
- MeasureTheory.Submartingale.condExp_sub_nonnegproof · cited by 3
- MeasureTheory.Submartingale.expected_stoppedValue_monoproof · cited by 3
- MeasureTheory.StronglyAdapted.measurable_upcrossingsBeforeproof · cited by 3
- MeasureTheory.IsStronglyProgressive.stronglyMeasurable_stoppedProcessproof · cited by 2
- MeasureTheory.Integrable.tendsto_ae_condExpproof · cited by 2
- MeasureTheory.Integrable.uniformIntegrable_condExp_filtrationproof · cited by 2
- MeasureTheory.memLp_stoppedProcess_of_mem_finsetproof · cited by 2