English
If f = o_l g on atTop, then the running sum of f over range n is little-o of the running sum of g; under suitable boundedness assumptions.
Русский
Если f = o_l g на atTop, то сумма f по диапазону до n мала по отношению к сумме g до n; при надлежащих ограничениях.
LaTeX
$$$ (\text{fun } n => \sum_{i=0}^{n-1} f(i)) = o_{atTop} (\sum_{i=0}^{n-1} g(i)) $$$
Lean4
theorem sum_range {α : Type*} [NormedAddCommGroup α] {f : ℕ → α} {g : ℕ → ℝ} (h : f =o[atTop] g) (hg : 0 ≤ g)
(h'g : Tendsto (fun n => ∑ i ∈ range n, g i) atTop atTop) :
(fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i :=
by
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
have B : ∀ n, ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i := fun n => by rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
apply isLittleO_iff.2 fun ε εpos => _
intro ε εpos
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
have : (fun _ : ℕ => ∑ i ∈ range N, f i) =o[atTop] fun n : ℕ => ∑ i ∈ range n, g i :=
by
apply isLittleO_const_left.2
exact Or.inr (h'g.congr fun n => (B n).symm)
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn
calc
‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by rw [sum_range_add_sum_Ico _ Nn]
_ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := (norm_add_le _ _)
_ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
(add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
_ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i :=
by
gcongr
· exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
· rw [range_eq_Ico]
exact Ico_subset_Ico (zero_le _) le_rfl
_ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
_ = ε * ‖∑ i ∈ range n, g i‖ := by
simp only [B]
ring
