Theorems · Theorem · probability
MeasureTheory.IsStronglyProgressive.stronglyAdapted
∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
{β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι],
MeasureTheory.IsStronglyProgressive f u → MeasureTheory.StronglyAdapted f u- Defined in
- Mathlib.Probability.Process.Adapted
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- Preorderstatement and proof · cited by 7,952
- Set.Elemproof · cited by 7,166
- le_rflproof · cited by 1,558
- Set.Iicproof · cited by 1,111
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.StronglyMeasurableproof · cited by 363
- MeasureTheory.StronglyAdaptedstatement · cited by 81
- measurable_prodMk_leftproof · cited by 69
- MeasureTheory.IsStronglyProgressivestatement and proof · cited by 54
- MeasureTheory.StronglyMeasurable.comp_measurableproof · cited by 52
Cited by7
Results whose statement or proof uses this declaration.
- MeasureTheory.IsStronglyPredictable.stronglyAdaptedproof · cited by 3
- MeasureTheory.IsStronglyProgressive.stronglyAdapted_stoppedProcessproof · cited by 2
- MeasureTheory.measurable_stoppedValueproof · cited by 2
- MeasureTheory.StronglyAdapted.stoppedProcess_of_discreteproof · cited by 1
- MeasureTheory.IsStronglyPredictable.iff_measurable_add_oneproof · cited by 1
- MeasureTheory.ProgMeasurable.stronglyAdaptedproof · cited by 0
- MeasureTheory.StronglyAdapted.stoppedProcessproof · cited by 0