Theorems · Theorem · probability

MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le

∀ {Ω : 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 ι] [LocallyFiniteOrder ι]
  [inst_5 : OrderBot ι] [inst_6 : TopologicalSpace ι] [DiscreteTopology ι] [inst_8 : MeasurableSpace ι] [BorelSpace ι]
  [inst_10 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ℱ : MeasureTheory.Filtration ι m}
  {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {i : ι},
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.IsStoppingTime ℱ τ →
      ∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
        (∀ (x : Ω), τ x ≤ ↑i) →
          μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
            MeasureTheory.stoppedValue f τ

Defined in

Mathlib.Probability.Martingale.OptionalSampling

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceLinearOrderLocallyFiniteOrderOrderBotTopologicalSpaceDiscreteTopologyMeasurableSpaceBorelSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyMeasureTheory.SigmaFinite