English
The same strong law holds under weaker assumptions via IdentDistrib and indep Fun.
Русский
Сильный закон сохраняется под более слабых предпосылках через IdentDistrib и IndepFun.
LaTeX
$$∀ᵐ ω, Tendsto (λ n, (∑_{i< n} X_i ω)/n) atTop (𝓝 μ[X_0])$$
Lean4
/-- The truncated and non-truncated versions of `Xᵢ` have the same asymptotic behavior, as they
almost surely coincide at all but finitely many steps. This follows from a probability computation
and Borel-Cantelli. -/
theorem strong_law_aux5 :
∀ᵐ ω, (fun n : ℕ => ∑ i ∈ range n, truncation (X i) i ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n : ℕ => (n : ℝ) :=
by
have A : (∑' j : ℕ, ℙ {ω | X j ω ∈ Set.Ioi (j : ℝ)}) < ∞ :=
by
convert tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2
ext1 j
exact (hident j).measure_mem_eq measurableSet_Ioi
have B : ∀ᵐ ω, Tendsto (fun n : ℕ => truncation (X n) n ω - X n ω) atTop (𝓝 0) :=
by
filter_upwards [ae_eventually_notMem A.ne] with ω hω
apply tendsto_const_nhds.congr' _
filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos
simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]
split_ifs with h
· exact (sub_self _).symm
· have : -(n : ℝ) < X n ω := by
apply lt_of_lt_of_le _ (hnonneg n ω)
simpa only [Right.neg_neg_iff, Nat.cast_pos] using npos
simp only [this, true_and, not_le] at h
exact (hn h).elim
filter_upwards [B] with ω hω
convert isLittleO_sum_range_of_tendsto_zero hω using 1
ext n
rw [sum_sub_distrib]
