Theorems · Theorem · probability
MeasureTheory.IsPredictable.measurable_add_one
Deprecated since 2026-04-24Use MeasureTheory.IsStronglyPredictable.measurable_add_one instead.
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
{u : ℕ → Ω → E}, MeasureTheory.IsStronglyPredictable 𝓕 u → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))Alias of MeasureTheory.IsStronglyPredictable.measurable_add_one.
If u is a discrete predictable process, then u (n + 1) is 𝓕 n-measurable.
- Defined in
- Mathlib.Probability.Process.Predictable
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Filtrationstatement · cited by 425
- MeasureTheory.StronglyMeasurablestatement · cited by 363
- MeasureTheory.Filtration.seqstatement · cited by 184
- MeasureTheory.IsStronglyPredictablestatement · cited by 17
- MeasureTheory.IsStronglyPredictable.measurable_add_oneproof · cited by 6
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.