English
Difference between truncated and full sums is little-o of n almost surely.
Русский
Разность усеченных и полных сумм равна o(n) почти наверняка.
LaTeX
$$∀ᵐ ω, (∑_{i< n} truncation(X_i) i ω - ∑_{i< n} X_i ω) = o[n]$$
Lean4
/-- The truncation of `Xᵢ` up to `i` satisfies the strong law of large numbers
(with respect to the truncated expectation) along the sequence
`c^n`, for any `c > 1`. This follows from `strong_law_aux1` by varying `ε`. -/
theorem strong_law_aux2 {c : ℝ} (c_one : 1 < c) :
∀ᵐ ω,
(fun n : ℕ => ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) i ω - 𝔼[∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) i]) =o[atTop]
fun n : ℕ => (⌊c ^ n⌋₊ : ℝ) :=
by
obtain ⟨v, -, v_pos, v_lim⟩ : ∃ v : ℕ → ℝ, StrictAnti v ∧ (∀ n : ℕ, 0 < v n) ∧ Tendsto v atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto (0 : ℝ)
have := fun i => strong_law_aux1 X hint hindep hident hnonneg c_one (v_pos i)
filter_upwards [ae_all_iff.2 this] with ω hω
apply Asymptotics.isLittleO_iff.2 fun ε εpos => ?_
obtain ⟨i, hi⟩ : ∃ i, v i < ε := ((tendsto_order.1 v_lim).2 ε εpos).exists
filter_upwards [hω i] with n hn
simp only [Real.norm_eq_abs, Nat.abs_cast]
exact hn.le.trans (mul_le_mul_of_nonneg_right hi.le (Nat.cast_nonneg _))
