Optional stopping theorem

TheoremBounded optional stopping, conditional form#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration such that \(\mu\) is σ-finite on every \(\mathcal{F}_n\), and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued submartingale with respect to \((\mathcal{F}_n)\) and \(\mu\). Let \(L\) and \(M\) be stopping times with values in \(\mathbb{N} \cup \{\infty\}\) such that \(L(\omega) \le M(\omega) \le N\) for every \(\omega\), for some \(N \in \mathbb{N}\), and suppose that \(\mu\) is σ-finite on the σ-algebra \(\mathcal{F}_L\) of events \(A\) with \(A \cap \{L \le n\} \in \mathcal{F}_n\) for every \(n\). Write \(f_L(\omega) = f_{L(\omega)}(\omega)\) and \(f_M(\omega) = f_{M(\omega)}(\omega)\) for the stopped values. Then \(f_L \le \mathbb{E}_\mu[f_M \mid \mathcal{F}_L]\) holds \(\mu\)-almost everywhere.

theorem Submartingale.stoppedValue_le_condExp_stoppedValue
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω}
    {ℱ : Filtration ℕ m0}
    [SigmaFiniteFiltration μ ℱ]
    {f : ℕ → Ω → ℝ}
    {L M : Ω → ℕ∞}
    (hsub : Submartingale f ℱ μ)
    (hL : IsStoppingTime ℱ L)
    (hM : IsStoppingTime ℱ M)
    (hLM : L ≤ M)
    {N : ℕ} (hbdd : ∀ ω, M ω ≤ N)
    [SigmaFinite (μ.trim hL.measurableSpace_le)] :
    stoppedValue f L ≤ᵐ[μ] μ[stoppedValue f M | hL.measurableSpace]
Used by 1
Used byBounded optional stopping, conditional form, supermartingale dual

TheoremBounded optional stopping, conditional form, supermartingale dual#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration such that \(\mu\) is σ-finite on every \(\mathcal{F}_n\), and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued supermartingale with respect to \((\mathcal{F}_n)\) and \(\mu\). Let \(L\) and \(M\) be stopping times with values in \(\mathbb{N} \cup \{\infty\}\) such that \(L(\omega) \le M(\omega) \le N\) for every \(\omega\), for some \(N \in \mathbb{N}\), and suppose that \(\mu\) is σ-finite on the σ-algebra \(\mathcal{F}_L\) of events \(A\) with \(A \cap \{L \le n\} \in \mathcal{F}_n\) for every \(n\). Write \(f_L(\omega) = f_{L(\omega)}(\omega)\) and \(f_M(\omega) = f_{M(\omega)}(\omega)\) for the stopped values. Then \(\mathbb{E}_\mu[f_M \mid \mathcal{F}_L] \le f_L\) holds \(\mu\)-almost everywhere.

This follows from the submartingale version applied to \(-f\).

theorem Supermartingale.condExp_stoppedValue_le_stoppedValue
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω}
    {ℱ : Filtration ℕ m0}
    [SigmaFiniteFiltration μ ℱ]
    {f : ℕ → Ω → ℝ}
    {L M : Ω → ℕ∞}
    (hsup : Supermartingale f ℱ μ)
    (hL : IsStoppingTime ℱ L)
    (hM : IsStoppingTime ℱ M)
    (hLM : L ≤ M)
    {N : ℕ} (hbdd : ∀ ω, M ω ≤ N)
    [SigmaFinite (μ.trim hL.measurableSpace_le)] :
    μ[stoppedValue f M | hL.measurableSpace] ≤ᵐ[μ] stoppedValue f L
Uses 1
Proof usesBounded optional stopping, conditional form

DefinitionValue of a process at a possibly infinite time#✓fully proved

For a real-valued process \((f_n)_{n \in \mathbb{N}}\) on \(\Omega\) and a map \(\tau : \Omega \to \mathbb{N} \cup \{\infty\}\), the value \(f_\tau\) of \(f\) at \(\tau\) is the function on \(\Omega\) given by \(f_\tau(\omega) = f_{\tau(\omega)}(\omega)\) when \(\tau(\omega) < \infty\) and \(f_\tau(\omega) = \lim_{n \to \infty} f_n(\omega)\) when \(\tau(\omega) = \infty\), where the limit is an unspecified real number if \((f_n(\omega))_n\) does not converge.

Unlike the usual stopped value, which uses an arbitrary finite index where \(\tau = \infty\), this uses the limit there, as the general optional stopping theorem requires.

noncomputable def stoppedValueAtTop (f : ℕ → Ω → ℝ) (τ : Ω → WithTop ℕ) : Ω → ℝ :=
  fun ω => if τ ω = ⊤ then Filter.limUnder atTop (fun n => f n ω) else f (τ ω).untopA ω
Used by 7
Used byGeneral optional stopping for uniformly integrable martingales · Expectation form of conditional optional stopping for uniformly integrable submartingales · General optional stopping, expectation inequality · Stopped value as conditional expectation of the limit · Conditional optional stopping with UI of the stopped process · Conditional optional stopping for uniformly integrable submartingales · Stopping at a later time does not change the stopped value

TheoremOptional stopping preserves uniform integrability of martingales#✓fully proved

Let \(\mu\) be a probability measure and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to a filtration \((\mathcal{F}_n)_{n \in \mathbb{N}}\) that is uniformly integrable. Then for every stopping time \(\tau\) with values in \(\mathbb{N} \cup \{\infty\}\), the stopped process \((f_{\tau \wedge n})_{n \in \mathbb{N}}\) is uniformly integrable.

The stopped process is a family of conditional expectations of the single integrable limit process, hence uniformly integrable.

theorem Martingale.uniformIntegrable_stoppedProcess_of_uniformIntegrable
    (hmart : Martingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    (τ : Ω → WithTop ℕ) (hτ : IsStoppingTime ℱ τ) :
    UniformIntegrable (stoppedProcess f τ) 1 μ
Used by 3
Used byGeneral optional stopping for uniformly integrable martingales · Conditional optional stopping for uniformly integrable submartingales · General optional stopping, uniform integrability preservation

TheoremGeneral optional stopping for uniformly integrable martingales#✓fully proved

Let \(\mu\) be a probability measure, let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to \((\mathcal{F}_n)\) that is uniformly integrable. Let \(f_\infty\) be the limit process of \(f\) (its almost-everywhere limit, by the martingale convergence theorem). Then for every stopping time \(\tau\) with values in \(\mathbb{N} \cup \{\infty\}\), the value \(f_\tau\) of \(f\) at \(\tau\) (at points where \(\tau = \infty\) it is \(\lim_n f_n\)) satisfies \(\int f_0 \, d\mu = \int f_\tau \, d\mu = \int f_\infty \, d\mu\).

theorem Martingale.integral_stoppedValueAtTop_eq_of_uniformIntegrable
    (hmart : Martingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    (τ : Ω → WithTop ℕ) (hτ : IsStoppingTime ℱ τ) :
    (∫ ω, f 0 ω ∂μ = ∫ ω, stoppedValueAtTop f τ ω ∂μ) ∧
    (∫ ω, stoppedValueAtTop f τ ω ∂μ = ∫ ω, ℱ.limitProcess f μ ω ∂μ)
Uses 2
Statement usesValue of a process at a possibly infinite time
Proof usesOptional stopping preserves uniform integrability of martingales

DefinitionStopped filtration#✓fully proved

Let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on a measurable space \(\Omega\) and let \(\tau\) be a stopping time for it with values in \(\mathbb{N} \cup \{\infty\}\). The stopped filtration is the filtration \(n \mapsto \mathcal{F}_{\tau \wedge n}\), where \(\mathcal{F}_{\tau \wedge n}\) is the σ-algebra of the stopping time \(\tau \wedge n\).

noncomputable def IsStoppingTime.stoppedFiltration (ℱ : Filtration ℕ m0)
    {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) : Filtration ℕ m0 where
  seq n := (hτ.min_const n).measurableSpace
  mono' := by
    intro i j hij
    exact IsStoppingTime.measurableSpace_mono (hτ.min_const i) (hτ.min_const j)
      (fun ω => min_le_min le_rfl (WithTop.coe_le_coe.mpr hij))
  le' n := (hτ.min_const n).measurableSpace_le
Used by 5
Used byThe stopped filtration generates the stopping-time σ-algebra · The event that the stopping time is infinite is measurable for the stopped filtration · Infinite-time parts of limit-σ-algebra sets are measurable for the stopped filtration · Levels of the stopped filtration · Stopped value as conditional expectation of the limit

TheoremLevels of the stopped filtration#✓fully proved

Let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on a measurable space \(\Omega\) and let \(\tau\) be a stopping time for it with values in \(\mathbb{N} \cup \{\infty\}\). For every \(n \in \mathbb{N}\), the \(n\)-th σ-algebra of the stopped filtration is \(\mathcal{F}_{\tau \wedge n}\), the σ-algebra of the stopping time \(\tau \wedge n\).

theorem IsStoppingTime.stoppedFiltration_apply (ℱ : Filtration ℕ m0)
    {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) (n : ℕ) :
    (hτ.stoppedFiltration ℱ) n = (hτ.min_const n).measurableSpace
Uses 1
Statement usesStopped filtration

TheoremThe event that the stopping time is infinite is measurable for the stopped filtration#✓fully proved

Let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on a measurable space \(\Omega\) and let \(\tau\) be a stopping time for it with values in \(\mathbb{N} \cup \{\infty\}\). For each \(n\), let \(\mathcal{F}_{\tau \wedge n}\) be the σ-algebra of the stopping time \(\tau \wedge n\). Then the set \(\{\omega : \tau(\omega) = \infty\}\) is measurable with respect to \(\bigvee_n \mathcal{F}_{\tau \wedge n}\).

theorem IsStoppingTime.measurableSet_eq_top_iSup_stoppedFiltration
    (ℱ : Filtration ℕ m0) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) :
    MeasurableSet[⨆ n, (hτ.stoppedFiltration ℱ) n] {ω | τ ω = ⊤}
Uses 1 · Used by 1
Statement usesStopped filtration
Used byInfinite-time parts of limit-σ-algebra sets are measurable for the stopped filtration

TheoremInfinite-time parts of limit-σ-algebra sets are measurable for the stopped filtration#✓fully proved

Let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on a measurable space \(\Omega\) and let \(\tau\) be a stopping time for it with values in \(\mathbb{N} \cup \{\infty\}\). For each \(n\), let \(\mathcal{F}_{\tau \wedge n}\) be the σ-algebra of the stopping time \(\tau \wedge n\). If a set \(s \subseteq \Omega\) is measurable with respect to \(\bigvee_n \mathcal{F}_n\), then \(s \cap \{\tau = \infty\}\) is measurable with respect to \(\bigvee_n \mathcal{F}_{\tau \wedge n}\).

The proof is induction on the σ-algebra generated by the π-system of sets measurable at some finite time. For \(s \in \mathcal{F}_k\) and \(m \ge k\), the sets \((s \cap \{\tau > m\}) \cup \{\tau \le m\}\) lie in \(\mathcal{F}_{\tau \wedge m}\), and their intersection over \(m \ge k\), intersected with \(\{\tau = \infty\}\), is \(s \cap \{\tau = \infty\}\).

theorem IsStoppingTime.measurableSet_inter_eq_top_iSup_stoppedFiltration
    (ℱ : Filtration ℕ m0) {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ)
    {s : Set Ω} (hs : MeasurableSet[⨆ n, ℱ n] s) :
    MeasurableSet[⨆ n, (hτ.stoppedFiltration ℱ) n] (s ∩ {ω | τ ω = ⊤})
Uses 2 · Used by 1
Statement usesStopped filtration
Proof usesThe event that the stopping time is infinite is measurable for the stopped filtration
Used byThe stopped filtration generates the stopping-time σ-algebra

TheoremThe stopped filtration generates the stopping-time σ-algebra#✓fully proved

Let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on a measurable space \(\Omega\) and let \(\tau\) be a stopping time for it with values in \(\mathbb{N} \cup \{\infty\}\). For each \(n\), let \(\mathcal{F}_{\tau \wedge n}\) be the σ-algebra of the stopping time \(\tau \wedge n\), the \(n\)-th σ-algebra of the stopped filtration, and let \(\mathcal{F}_\tau\) be the σ-algebra of \(\tau\). Then \(\bigvee_n \mathcal{F}_{\tau \wedge n} = \mathcal{F}_\tau\).

The inclusion \(\le\) is monotonicity. For \(\ge\), a set \(s \in \mathcal{F}_\tau\) splits into its finite-time part \(s \cap \{\tau < \infty\} = \bigcup_n (s \cap \{\tau \le n\})\) and its infinite-time part \(s \cap \{\tau = \infty\}\), and both are measurable for the supremum.

theorem IsStoppingTime.iSup_stoppedFiltration (ℱ : Filtration ℕ m0)
    {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) :
    ⨆ n, (hτ.stoppedFiltration ℱ) n = hτ.measurableSpace
Uses 2 · Used by 1
Statement usesStopped filtration
Proof usesInfinite-time parts of limit-σ-algebra sets are measurable for the stopped filtration
Used byStopped value as conditional expectation of the limit

TheoremStopped value as conditional expectation of the limit#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration, and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to \((\mathcal{F}_n)\) and \(\mu\) that is uniformly integrable in \(L^1(\mu)\). Let \(f_\infty\) be its limit process, a function measurable with respect to \(\bigvee_n \mathcal{F}_n\) to which \(f_n\) converges \(\mu\)-almost everywhere. Then for every stopping time \(\tau\) with values in \(\mathbb{N} \cup \{\infty\}\), the value \(f_\tau\) of \(f\) at \(\tau\) (with \(f_\tau(\omega) = \lim_n f_n(\omega)\) where \(\tau(\omega) = \infty\)) satisfies \(f_\tau = \mu[f_\infty \mid \mathcal{F}_\tau]\) \(\mu\)-almost everywhere, where \(\mu[\,\cdot \mid \mathcal{F}_\tau]\) is conditional expectation given the σ-algebra \(\mathcal{F}_\tau\) of \(\tau\).

For each \(n\), bounded optional sampling gives \(f_{\tau \wedge n} = \mu[f_\infty \mid \mathcal{F}_{\tau \wedge n}]\) almost everywhere, and Lévy's upward theorem for the filtration \(n \mapsto \mathcal{F}_{\tau \wedge n}\) identifies the almost-everywhere limit of these conditional expectations with \(\mu[f_\infty \mid \bigvee_n \mathcal{F}_{\tau \wedge n}] = \mu[f_\infty \mid \mathcal{F}_\tau]\).

theorem Martingale.stoppedValueAtTop_ae_eq_condExp_limitProcess
    (hf : Martingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    {τ : Ω → WithTop ℕ} (hτ : IsStoppingTime ℱ τ) :
    stoppedValueAtTop f τ =ᵐ[μ] μ[ℱ.limitProcess f μ | hτ.measurableSpace]
Uses 3 · Used by 3
Statement usesValue of a process at a possibly infinite time
Proof usesThe stopped filtration generates the stopping-time σ-algebra · Stopped filtration
Used byExpectation form of conditional optional stopping for uniformly integrable submartingales · Conditional optional stopping with UI of the stopped process · Conditional optional stopping for uniformly integrable submartingales

TheoremStopping at a later time does not change the stopped value#✓fully proved

Let \((f_n)_{n \in \mathbb{N}}\) be a sequence of real-valued functions on \(\Omega\) and let \(L, M : \Omega \to \mathbb{N} \cup \{\infty\}\) satisfy \(L(\omega) \le M(\omega)\) for every \(\omega\). Then the value at \(L\) of the stopped process \(n \mapsto f_{M \wedge n}\) equals the value \(f_L\) of \(f\) at \(L\) at every point of \(\Omega\). Here the value of a sequence \((g_n)\) at a point \(\omega\) where the time is infinite is \(\lim_n g_n(\omega)\) when this limit exists, and otherwise a fixed default value that depends only on the sequence \((g_n(\omega))_{n \in \mathbb{N}}\).

On \(\{L = \infty\}\) the inequality forces \(M = \infty\), so there the stopped process is \(f\) itself.

theorem stoppedValueAtTop_stoppedProcess_of_le
    {L M : Ω → WithTop ℕ} (hLM : L ≤ M) :
    stoppedValueAtTop (stoppedProcess f M) L = stoppedValueAtTop f L
Uses 1 · Used by 1
Statement usesValue of a process at a possibly infinite time
Used byConditional optional stopping with UI of the stopped process

TheoremConditional optional stopping with UI of the stopped process#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration, and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to \((\mathcal{F}_n)\) and \(\mu\). Let \(L \le M\) be stopping times with values in \(\mathbb{N} \cup \{\infty\}\), and suppose the stopped process \((f_{M \wedge n})_{n \in \mathbb{N}}\) is uniformly integrable in \(L^1(\mu)\). Then \(f_L = \mu[f_M \mid \mathcal{F}_L]\) \(\mu\)-almost everywhere. Here \(f_L\) and \(f_M\) are the values of \(f\) at the possibly infinite times \(L\) and \(M\), with \(f_L(\omega) = \lim_n f_n(\omega)\) where \(L(\omega) = \infty\) and likewise for \(M\), and \(\mu[\,\cdot \mid \mathcal{F}_L]\) is conditional expectation given the σ-algebra \(\mathcal{F}_L\) of \(L\).

If \(f\) itself is uniformly integrable, then so is the stopped process \((f_{M \wedge n})\), so the conclusion holds in that case as well.

theorem Martingale.stoppedValueAtTop_ae_eq_condExp_stoppedValueAtTop
    (hf : Martingale f ℱ μ) {L M : Ω → WithTop ℕ}
    (hui : UniformIntegrable (stoppedProcess f M) 1 μ)
    (hL : IsStoppingTime ℱ L) (hM : IsStoppingTime ℱ M) (hLM : L ≤ M) :
    stoppedValueAtTop f L
      =ᵐ[μ] μ[stoppedValueAtTop f M | hL.measurableSpace]
Uses 3 · Used by 1
Statement usesValue of a process at a possibly infinite time
Proof usesStopped value as conditional expectation of the limit · Stopping at a later time does not change the stopped value
Used byConditional optional stopping for uniformly integrable submartingales

TheoremConditional optional stopping for uniformly integrable submartingales#✓fully proved

Conditional optional stopping for uniformly integrable submartingales. For stopping times L ≤ M (possibly infinite), f_L ≤ᵐ μ[f_M | ℱ_L].

theorem Submartingale.stoppedValueAtTop_le_condExp_stoppedValueAtTop
    (hsub : Submartingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    {L M : Ω → WithTop ℕ} (hL : IsStoppingTime ℱ L) (hM : IsStoppingTime ℱ M)
    (hLM : L ≤ M) :
    stoppedValueAtTop f L ≤ᵐ[μ] μ[stoppedValueAtTop f M | hL.measurableSpace]
Uses 4 · Used by 1
Statement usesValue of a process at a possibly infinite time
Proof usesStopped value as conditional expectation of the limit · Conditional optional stopping with UI of the stopped process · Optional stopping preserves uniform integrability of martingales
Used byExpectation form of conditional optional stopping for uniformly integrable submartingales

TheoremExpectation form of conditional optional stopping for uniformly integrable submartingales#✓fully proved

Expectation form of conditional optional stopping for uniformly integrable submartingales. For stopping times L ≤ M (possibly infinite), ∫ f_L ≤ ∫ f_M.

theorem Submartingale.integral_stoppedValueAtTop_mono_of_uniformIntegrable
    (hsub : Submartingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    {L M : Ω → WithTop ℕ} (hL : IsStoppingTime ℱ L) (hM : IsStoppingTime ℱ M)
    (hLM : L ≤ M) :
    ∫ ω, stoppedValueAtTop f L ω ∂μ ≤ ∫ ω, stoppedValueAtTop f M ω ∂μ
Uses 3
Statement usesValue of a process at a possibly infinite time
Proof usesStopped value as conditional expectation of the limit · Conditional optional stopping for uniformly integrable submartingales

TheoremGeneral optional stopping, uniform integrability preservation#✓fully proved

Let \(\mu\) be a probability measure and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued submartingale with respect to a filtration \((\mathcal{F}_n)_{n \in \mathbb{N}}\) that is uniformly integrable. Then for every stopping time \(\tau\) with values in \(\mathbb{N} \cup \{\infty\}\), the stopped process \((f_{\tau \wedge n})_{n \in \mathbb{N}}\) is uniformly integrable.

theorem Submartingale.uniformIntegrable_stoppedProcess_of_uniformIntegrable
    (hsub : Submartingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    (τ : Ω → WithTop ℕ) (hτ : IsStoppingTime ℱ τ) :
    UniformIntegrable (stoppedProcess f τ) 1 μ
Uses 1 · Used by 1
Proof usesOptional stopping preserves uniform integrability of martingales
Used byGeneral optional stopping, expectation inequality

TheoremGeneral optional stopping, expectation inequality#✓fully proved

Let \(\mu\) be a probability measure, let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued submartingale with respect to \((\mathcal{F}_n)\) that is uniformly integrable. Let \(f_\infty\) be the limit process of \(f\) (its almost-everywhere limit, by the martingale convergence theorem). Then for every stopping time \(\tau\) with values in \(\mathbb{N} \cup \{\infty\}\), the value \(f_\tau\) of \(f\) at \(\tau\) (at points where \(\tau = \infty\) it is \(\lim_n f_n\)) satisfies \(\int f_0 \, d\mu \le \int f_\tau \, d\mu \le \int f_\infty \, d\mu\).

theorem Submartingale.integral_stoppedValueAtTop_of_uniformIntegrable
    (hsub : Submartingale f ℱ μ) (hui : UniformIntegrable f 1 μ)
    (τ : Ω → WithTop ℕ) (hτ : IsStoppingTime ℱ τ) :
    (∫ ω, f 0 ω ∂μ ≤ ∫ ω, stoppedValueAtTop f τ ω ∂μ) ∧
    (∫ ω, stoppedValueAtTop f τ ω ∂μ ≤ ∫ ω, ℱ.limitProcess f μ ω ∂μ)
Uses 2
Statement usesValue of a process at a possibly infinite time
Proof usesGeneral optional stopping, uniform integrability preservation

TheoremOptional stopping for supermartingales at two bounded stopping times#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and \((\mathcal G_n)_{n \ge 0}\) a filtration such that the restriction of \(\mu\) to each \(\mathcal G_n\) is σ-finite, and let \((f_n)_{n \ge 0}\) be a real-valued supermartingale with respect to \((\mathcal G_n)\) and \(\mu\). Let \(\tau\) and \(\pi\) be stopping times for \((\mathcal G_n)\) with values in \(\mathbb N \cup \{\infty\}\), and let \(N\) be a natural number such that \(\tau(\omega) \le \pi(\omega) \le N\) for every \(\omega \in \Omega\). Then \(\int f_\pi \, d\mu \le \int f_\tau \, d\mu\), where \(f_\tau(\omega) = f_{\tau(\omega)}(\omega)\).

This is the dual of the submartingale form of bounded optional stopping, obtained by applying it to \(-f\).

theorem Supermartingale.expected_stoppedValue_anti_mono
    [SigmaFiniteFiltration μ 𝒢]
    (hf : Supermartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) (hπ : IsStoppingTime 𝒢 π)
    (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) :
    μ[stoppedValue f π] ≤ μ[stoppedValue f τ]
Used by 2
Used byOptional stopping for martingales at two bounded stopping times · Optional stopping for supermartingales at a bounded stopping time

TheoremOptional stopping for supermartingales at a bounded stopping time#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and \((\mathcal G_n)_{n \ge 0}\) a filtration such that the restriction of \(\mu\) to each \(\mathcal G_n\) is σ-finite, and let \((f_n)_{n \ge 0}\) be a real-valued supermartingale with respect to \((\mathcal G_n)\) and \(\mu\). Let \(\tau\) be a stopping time for \((\mathcal G_n)\) with values in \(\mathbb N \cup \{\infty\}\), and let \(N\) be a natural number such that \(\tau(\omega) \le N\) for every \(\omega \in \Omega\). Then \(\int f_\tau \, d\mu \le \int f_0 \, d\mu\), where \(f_\tau(\omega) = f_{\tau(\omega)}(\omega)\).

theorem Supermartingale.expected_stoppedValue_le
    [SigmaFiniteFiltration μ 𝒢]
    (hf : Supermartingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ)
    {N : ℕ} (hbdd : ∀ ω, τ ω ≤ N) :
    μ[stoppedValue f τ] ≤ μ[f 0]
Uses 1
Proof usesOptional stopping for supermartingales at two bounded stopping times

TheoremOptional stopping for martingales at two bounded stopping times#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and \((\mathcal G_n)_{n \ge 0}\) a filtration such that the restriction of \(\mu\) to each \(\mathcal G_n\) is σ-finite, and let \((f_n)_{n \ge 0}\) be a real-valued martingale with respect to \((\mathcal G_n)\) and \(\mu\). Let \(\tau\) and \(\pi\) be stopping times for \((\mathcal G_n)\) with values in \(\mathbb N \cup \{\infty\}\), and let \(N\) be a natural number such that \(\tau(\omega) \le \pi(\omega) \le N\) for every \(\omega \in \Omega\). Then \(\int f_\tau \, d\mu = \int f_\pi \, d\mu\), where \(f_\tau(\omega) = f_{\tau(\omega)}(\omega)\).

theorem Martingale.expected_stoppedValue_eq
    [SigmaFiniteFiltration μ 𝒢]
    (hf : Martingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ) (hπ : IsStoppingTime 𝒢 π)
    (hle : τ ≤ π) {N : ℕ} (hbdd : ∀ ω, π ω ≤ N) :
    μ[stoppedValue f τ] = μ[stoppedValue f π]
Uses 1 · Used by 1
Proof usesOptional stopping for supermartingales at two bounded stopping times
Used byOptional stopping for martingales at a bounded stopping time

TheoremOptional stopping for martingales at a bounded stopping time#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and \((\mathcal G_n)_{n \ge 0}\) a filtration such that the restriction of \(\mu\) to each \(\mathcal G_n\) is σ-finite, and let \((f_n)_{n \ge 0}\) be a real-valued martingale with respect to \((\mathcal G_n)\) and \(\mu\). Let \(\tau\) be a stopping time for \((\mathcal G_n)\) with values in \(\mathbb N \cup \{\infty\}\), and let \(N\) be a natural number such that \(\tau(\omega) \le N\) for every \(\omega \in \Omega\). Then \(\int f_\tau \, d\mu = \int f_0 \, d\mu\), where \(f_\tau(\omega) = f_{\tau(\omega)}(\omega)\).

theorem Martingale.expected_stoppedValue_eq_zero
    [SigmaFiniteFiltration μ 𝒢]
    (hf : Martingale f 𝒢 μ) (hτ : IsStoppingTime 𝒢 τ)
    {N : ℕ} (hbdd : ∀ ω, τ ω ≤ N) :
    μ[stoppedValue f τ] = μ[f 0]
Uses 1
Proof usesOptional stopping for martingales at two bounded stopping times
21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.