English
A technical lemma on equivalence of inequalities under subtraction.
Русский
Техническая лемма об эквивалентности неравенств при вычитании.
LaTeX
$$∀ {a b c : α}, Eq (And a b → c) (a → b → c)$$
Lean4
/-- `Xᵢ` satisfies the strong law of large numbers along the sequence
`c^n`, for any `c > 1`. This follows from the version for the truncated `Xᵢ`, and the fact that
`Xᵢ` and its truncated version have the same asymptotic behavior. -/
theorem strong_law_aux6 {c : ℝ} (c_one : 1 < c) :
∀ᵐ ω, Tendsto (fun n : ℕ => (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ⌊c ^ n⌋₊) atTop (𝓝 𝔼[X 0]) :=
by
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c ^ n⌋₊ := by
intro n
refine zero_lt_one.trans_le ?_
simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ c_one.le]
filter_upwards [strong_law_aux4 X hint hindep hident hnonneg c_one, strong_law_aux5 X hint hident hnonneg] with ω hω
h'ω
rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ]
have L : (fun n : ℕ => ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ⌊c ^ n⌋₊ * 𝔼[X 0]) =o[atTop] fun n => (⌊c ^ n⌋₊ : ℝ) :=
by
have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
convert hω.sub (h'ω.comp_tendsto A) using 1
ext1 n
simp only [Function.comp_apply, sub_sub_sub_cancel_left]
convert L.mul_isBigO (isBigO_refl (fun n : ℕ => (⌊c ^ n⌋₊ : ℝ)⁻¹) atTop) using 1 <;> (ext1 n; field_simp [(H n).ne'])
