English
For IsFiniteMeasure μ and Submartingale f, boundedness of the range in ω is equivalent to boundedness of -f range; equivalently bounds above correspond to bounds below after sign flip.
Русский
Для конечной меры и субмартингала ограниченность диапазона приращений сохраняется под заменой f на −f: верхняя ограниченность эквивалентна нижней после знака.
LaTeX
$$$$\forall^* \omega, BddAbove(\{f n(\omega)\}) \iff BddBelow(\{f n(\omega)\}).$$$$
Lean4
/-- One sided martingale bound: If `f` is a submartingale which has uniformly bounded differences,
then for almost every `ω`, `f n ω` is bounded above (in `n`) if and only if it converges. -/
theorem bddAbove_iff_exists_tendsto [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
(hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
∀ᵐ ω ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c) :=
by
set g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
have hg : Submartingale g ℱ μ := hf.sub_martingale (martingale_const_fun _ _ (hf.adapted 0) (hf.integrable 0))
have hg0 : g 0 = 0 := by
ext ω
simp only [g, sub_self, Pi.zero_apply]
have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by simpa only [g, sub_sub_sub_cancel_right]
filter_upwards [hg.bddAbove_iff_exists_tendsto_aux hg0 hgbdd] with ω hω
convert hω using 1
· refine ⟨fun h => ?_, fun h => ?_⟩ <;> obtain ⟨b, hb⟩ := h <;> refine ⟨b + |f 0 ω|, fun y hy => ?_⟩ <;>
obtain ⟨n, rfl⟩ := hy
· simp_rw [g, sub_eq_add_neg]
exact add_le_add (hb ⟨n, rfl⟩) (neg_le_abs _)
· exact sub_le_iff_le_add.1 (le_trans (sub_le_sub_left (le_abs_self _) _) (hb ⟨n, rfl⟩))
· refine ⟨fun h => ?_, fun h => ?_⟩ <;> obtain ⟨c, hc⟩ := h
· exact ⟨c - f 0 ω, hc.sub_const _⟩
· refine ⟨c + f 0 ω, ?_⟩
have := hc.add_const (f 0 ω)
simpa only [g, sub_add_cancel]
