Theorems · Theorem · probability

MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp

∀ {Ω : 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} [MeasureTheory.SigmaFiniteFiltration μ ℱ],
  MeasureTheory.Martingale f ℱ μ →
    ∀ (hτ : MeasureTheory.IsStoppingTime ℱ τ) (hσ : MeasureTheory.IsStoppingTime ℱ σ) {n : ι},
      (∀ (x : Ω), τ x ≤ ↑n) →
        ∀ [h_sf_min : MeasureTheory.SigmaFinite (μ.trim ⋯)],
          (MeasureTheory.stoppedValue f fun x => min (σ x) (τ x)) =ᵐ[μ]
            μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace]

Optional Sampling theorem. If τ is a bounded stopping time and σ is another stopping time, then the value of a martingale f at the stopping time min τ σ is almost everywhere equal to the conditional expectation of f stopped at τ with respect to the σ-algebra generated by σ.

Defined in

Mathlib.Probability.Martingale.OptionalSampling

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceLinearOrderLocallyFiniteOrderOrderBotTopologicalSpaceDiscreteTopologyMeasurableSpaceBorelSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyMeasureTheory.SigmaFiniteFiltrationMeasureTheory.SigmaFinite