English
Auxiliary statements about floor powers and nonzero elements in N.
Русский
Вспомогательные утверждения о целых частях степеней и не равных нулю элементами.
LaTeX
$$∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R] (x : R), Eq (instLENat.le 1 (Nat.floor x)) (instDistribLatticeOfLinearOrder.toSemilatticeInf.le 1 x)$$
Lean4
/-- `Xᵢ` satisfies the strong law of large numbers along all integers. This follows from the
corresponding fact along the sequences `c^n`, and the fact that any integer can be sandwiched
between `c^n` and `c^(n+1)` with comparably small error if `c` is close enough to `1`
(which is formalized in `tendsto_div_of_monotone_of_tendsto_div_floor_pow`). -/
theorem strong_law_aux7 : ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range n, X i ω) / n) atTop (𝓝 𝔼[X 0]) :=
by
obtain ⟨c, -, cone, clim⟩ : ∃ c : ℕ → ℝ, StrictAnti c ∧ (∀ n : ℕ, 1 < c n) ∧ Tendsto c atTop (𝓝 1) :=
exists_seq_strictAnti_tendsto (1 : ℝ)
have : ∀ k, ∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ⌊c k ^ n⌋₊) atTop (𝓝 𝔼[X 0]) := fun k =>
strong_law_aux6 X hint hindep hident hnonneg (cone k)
filter_upwards [ae_all_iff.2 this] with ω hω
apply tendsto_div_of_monotone_of_tendsto_div_floor_pow _ _ _ c cone clim _
· intro m n hmn
exact sum_le_sum_of_subset_of_nonneg (range_mono hmn) fun i _ _ => hnonneg i ω
· exact hω
