Theorems · Theorem · probability

MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const

∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] [FirstCountableTopology ι] {ℱ : MeasureTheory.Filtration ι m}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {i n : ι},
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
      i ≤ n → μ[f n | hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = ↑i}] f i

Defined in

Mathlib.Probability.Martingale.OptionalSampling

Cited by

0 results in Mathlib

Foundations

Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceLinearOrderTopologicalSpaceOrderTopologyFirstCountableTopologyMeasureTheory.SigmaFiniteFiltrationMeasureTheory.SigmaFinite