English
For finite measure μ, and predictable measurable sets s(n), the sum of indicators converges in distribution to its conditional-expectation version if and only if the original sum converges similarly.
Русский
Для конечной меры \(μ\) и предсказуемых множеств \(s(n)\) сумма индикаторов сходится к той же предельной величине как и соответствующая сумма условных ожиданий.
LaTeX
$$$$\\forall^*\\omega\\partial\\mu:\\ Tendsto(\\sum_{k=0}^{n-1} (s(k+1)) indicator 1\\omega)_{n\\to\\infty} = Tendsto(\\sum_{k=0}^{n-1} \\mathbb{E}[ (s(k+1)).indicator 1 \\mid \\mathcal{F}_k](\\omega))_{n\\to\\infty}.$$$$
Lean4
/-- An a.e. monotone adapted process `f` with uniformly bounded differences converges to `+∞` if
and only if its predictable part also converges to `+∞`. -/
theorem tendsto_sum_indicator_atTop_iff [IsFiniteMeasure μ] (hfmono : ∀ᵐ ω ∂μ, ∀ n, f n ω ≤ f (n + 1) ω)
(hf : Adapted ℱ f) (hint : ∀ n, Integrable (f n) μ) (hbdd : ∀ᵐ ω ∂μ, ∀ n, |f (n + 1) ω - f n ω| ≤ R) :
∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop atTop ↔ Tendsto (fun n => predictablePart f ℱ μ n ω) atTop atTop :=
by
have h₁ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atTop (martingalePart_bdd_difference ℱ hbdd)
have h₂ := (martingale_martingalePart hf hint).ae_not_tendsto_atTop_atBot (martingalePart_bdd_difference ℱ hbdd)
have h₃ : ∀ᵐ ω ∂μ, ∀ n, 0 ≤ (μ[f (n + 1) - f n|ℱ n]) ω :=
by
refine ae_all_iff.2 fun n => condExp_nonneg ?_
filter_upwards [ae_all_iff.1 hfmono n] with ω hω using sub_nonneg.2 hω
filter_upwards [h₁, h₂, h₃, hfmono] with ω hω₁ hω₂ hω₃ hω₄
constructor <;> intro ht
· refine tendsto_atTop_atTop_of_monotone' ?_ ?_
· intro n m hnm
simp only [predictablePart, Finset.sum_apply]
exact Finset.sum_mono_set_of_nonneg hω₃ (Finset.range_mono hnm)
rintro ⟨b, hbdd⟩
rw [← tendsto_neg_atBot_iff] at ht
simp only [martingalePart, sub_eq_add_neg] at hω₁
exact hω₁ (tendsto_atTop_add_right_of_le _ (-b) (tendsto_neg_atBot_iff.1 ht) fun n => neg_le_neg (hbdd ⟨n, rfl⟩))
· refine tendsto_atTop_atTop_of_monotone' (monotone_nat_of_le_succ hω₄) ?_
rintro ⟨b, hbdd⟩
exact hω₂ ((tendsto_atBot_add_left_of_ge _ b fun n => hbdd ⟨n, rfl⟩) <| tendsto_neg_atBot_iff.2 ht)
