Theorems · Theorem · probability

MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_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 ι] [inst_4 : TopologicalSpace ι]
  [OrderTopology ι] {ℱ : MeasureTheory.Filtration ι m} [MeasureTheory.SigmaFiniteFiltration μ ℱ] {τ σ : Ω → WithTop ι}
  {f : ι → Ω → E} {n : ι} [inst_7 : Nonempty ι] [Countable ι],
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.IsStoppingTime ℱ τ →
      ∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ),
        σ ≤ τ →
          (∀ (x : Ω), τ x ≤ ↑n) →
            ∀ [MeasureTheory.SigmaFinite (μ.trim ⋯)],
              MeasureTheory.stoppedValue f σ =ᵐ[μ] μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace]

If τ and σ are two stopping times with σ ≤ τ and τ is bounded, then the value of a martingale f at σ is the conditional expectation of its value at τ with respect to the σ-algebra generated by σ.

Defined in

Mathlib.Probability.Martingale.OptionalSampling

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceLinearOrderTopologicalSpaceOrderTopologyMeasureTheory.SigmaFiniteFiltrationNonemptyCountableMeasureTheory.SigmaFinite