English
The supremum (pointwise) of two submartingales is a submartingale.
Русский
Пока что супремум по точкам двух субмартингалов — субмартингал.
LaTeX
$$$\mathrm{Submartingale}(f,\mathcal{F},\mu) \land \mathrm{Submartingale}(g,\mathcal{F},\mu) \Rightarrow \mathrm{Submartingale}(f \vee g,\mathcal{F},\mu)$$$
Lean4
protected theorem sup {f g : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) (hg : Submartingale g ℱ μ) :
Submartingale (f ⊔ g) ℱ μ :=
by
refine
⟨fun i => @StronglyMeasurable.sup _ _ _ _ (ℱ i) _ _ _ (hf.adapted i) (hg.adapted i), fun i j hij => ?_, fun i =>
Integrable.sup (hf.integrable _) (hg.integrable _)⟩
refine EventuallyLE.sup_le ?_ ?_
·
exact
EventuallyLE.trans (hf.2.1 i j hij)
(condExp_mono (hf.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
(Eventually.of_forall fun x => le_max_left _ _))
·
exact
EventuallyLE.trans (hg.2.1 i j hij)
(condExp_mono (hg.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
(Eventually.of_forall fun x => le_max_right _ _))
