Theorems · Theorem · probability

MeasureTheory.IsStronglyPredictable.of_measurable_add_one

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E},
  MeasureTheory.StronglyMeasurable (u 0) →
    (∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))) → MeasureTheory.IsStronglyPredictable 𝓕 u

Defined in: Mathlib.Probability.Process.Predictable
Cited by: 4 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites37

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setproof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
SetLike.coeproof · cited by 8,199
nhdsproof · cited by 5,554
Set.preimageproof · cited by 4,946
Set.rangeproof · cited by 4,705
Filter.Tendstoproof · cited by 3,814
MeasurableSetproof · cited by 3,075
Set.iUnionproof · cited by 2,483
Filter.atTopproof · cited by 2,405

Cited by4

Results whose statement or proof uses this declaration.

MeasureTheory.martingalePart_add_ae_eqproof · cited by 1
MeasureTheory.IsStronglyPredictable.iff_measurable_add_oneproof · cited by 1
MeasureTheory.IsPredictable.of_measurable_add_oneproof · cited by 0
MeasureTheory.isPredictable_predictablePartproof · cited by 0