English
Extends the truncated LLN from powers c^n to general multiplicative sequences.
Русский
Расширяет закон большого числа для усечённых сумм от powers к общим последовательностям.
LaTeX
$$∀ᵐ ω, Tendsto (λ n, (∑_{i<⌊c^n⌋} X_i ω) / ⌊c^n⌋) atTop (𝓝 𝔼[X_0])$$
Lean4
/-- The expectation of the truncated version of `Xᵢ` behaves asymptotically like the whole
expectation. This follows from convergence and Cesàro averaging. -/
theorem strong_law_aux3 : (fun n => 𝔼[∑ i ∈ range n, truncation (X i) i] - n * 𝔼[X 0]) =o[atTop] ((↑) : ℕ → ℝ) :=
by
have A : Tendsto (fun i => 𝔼[truncation (X i) i]) atTop (𝓝 𝔼[X 0]) :=
by
convert (tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop using 1
ext i
exact (hident i).truncation.integral_eq
convert Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 A) using 1
ext1 n
simp only [sum_sub_distrib, sum_const, card_range, nsmul_eq_mul, sum_apply, sub_left_inj]
rw [integral_finset_sum _ fun i _ => ?_]
exact ((hident i).symm.integrable_snd hint).1.integrable_truncation
