English
For a finite measure martingale f, with bounded increments, the set range being bounded above is equivalent to the set range being bounded below, and thus the limit behavior ties to both directions.
Русский
Для конечной меры и мартинга́ла с ограниченными приращениями, верхняя ограниченность диапазона эквивалентна нижней ограниченности диапазона, следовательно, предел связан с обеими направлениями.
LaTeX
$$$$\forall^* \omega,\; BddAbove(\{f n(\omega)\}) \iff BddBelow(\{f n(\omega)\}).$$$$
Lean4
theorem bddAbove_range_iff_bddBelow_range [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
(hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
∀ᵐ ω ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω) :=
by
have hbdd' : ∀ᵐ ω ∂μ, ∀ i, |(-f) (i + 1) ω - (-f) i ω| ≤ R :=
by
filter_upwards [hbdd] with ω hω i
erw [← abs_neg, neg_sub, sub_neg_eq_add, neg_add_eq_sub]
exact hω i
have hup := hf.submartingale.bddAbove_iff_exists_tendsto hbdd
have hdown := hf.neg.submartingale.bddAbove_iff_exists_tendsto hbdd'
filter_upwards [hup, hdown] with ω hω₁ hω₂
have : (∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c) :=
by
constructor <;> rintro ⟨c, hc⟩
· exact ⟨-c, hc.neg⟩
· refine ⟨-c, ?_⟩
convert hc.neg
simp only [neg_neg, Pi.neg_apply]
rw [hω₁, this, ← hω₂]
constructor <;> rintro ⟨c, hc⟩ <;> refine ⟨-c, fun ω hω => ?_⟩
· rw [mem_upperBounds] at hc
refine neg_le.2 (hc _ ?_)
simpa only [Pi.neg_apply, Set.mem_range, neg_inj]
· rw [mem_lowerBounds] at hc
simp_rw [Set.mem_range, Pi.neg_apply, neg_eq_iff_eq_neg] at hω
refine le_neg.1 (hc _ ?_)
simpa only [Set.mem_range]
