Optional sampling for submartingales

Stream: Brownian motion

[Etienne Marion]

In the blueprint there is only the optional sampling theorem for martingales, but wouldn't we need it for submartingales too? It is used to prove this lemma on almostsuremath. I am wondering if we could not adapt the proof for martingales (which is in mathlib in discrete time) to submartingales, then deduce it for supermartingales and then deduce it for martingales. Then we can do the same in continuous time.

[Rémy Degenne]

About "deduce for martingales": in MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp there is no order on E, so you can't say that a martingale is a submartingale.

[Etienne Marion]

Ah right.

[Rémy Degenne]

But I think we can use the Doob decomposition (https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Martingale/Centering.html) to prove the submartingale discrete time result from the martingale one?

[Rémy Degenne]

And I asked GPT5 for a sketch of proof (sorry if it ends up being AI slop):

Yes. In discrete time, the Doob decomposition gives a very quick proof.

Setup:
- Let (X_n) be an integrable submartingale adapted to (F_n).
- Let S ≤ T be bounded stopping times (or assume uniform integrability and pass to the limit via truncations).

Doob decomposition:
- Write X_n = M_n + A_n where:
  - (M_n) is a martingale,
  - (A_n) is predictable (A_n is F_{n-1}-measurable for n ≥ 1), increasing, and A_0 = 0.

Proof:
- By your OST for martingales, E[M_T | F_S] = M_S.
- Since A is increasing and S ≤ T, we have A_T ≥ A_S almost surely, hence E[A_T | F_S] ≥ A_S.
- Therefore,
  E[X_T | F_S] = E[M_T | F_S] + E[A_T | F_S] ≥ M_S + A_S = X_S.
- Taking expectations gives E[X_T] ≥ E[X_S].

Remarks:
- The key point is that for the predictable increasing part A, you don’t need any stopping-time trick: A_T ≥ A_S a.s. follows immediately from pathwise monotonicity and S ≤ T.
- For unbounded stopping times, first prove the result for T∧n, S∧n and then let n → ∞ using uniform integrability (or other standard integrability conditions). The martingale part uses your martingale OST; the A-part uses monotone convergence since A is increasing.

[Kexing Ying]

The proof looks correct to me. I will add it to the blueprint and rewrite the continuous version to use it

[Rémy Degenne]

Etienne is working on class D/DL and probably also on this since it's a prerequisite, so perhaps it's best to leave it to him.

[Kexing Ying]

Okay