English
A refined variant of the integral formula where the Big-O bound is strengthened and the equality is kept intact.
Русский
Уточнённый вариант интегрального формула: сила границы Big-O усилена, равенство сохраняется.
LaTeX
$$$LSeries'(f,s) = s \\int_{1}^{\\infty} (\\sum_{k ≤ ⌊t⌋} f(k)) t^{-(s+1)} dt$ under strengthened Big-O$$
Lean4
theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div
(hlim : Tendsto (fun n : ℕ ↦ (∑ k ∈ Icc 1 n, f k) / n) atTop (𝓝 l)) (hfS : ∀ s : ℝ, 1 < s → LSeriesSummable f s) :
Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s) (𝓝[>] 1) (𝓝 l) :=
by
have h₁ {C ε : ℝ} : Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε) :=
by
rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
have h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s : ℝ ↦ ‖(s - 1) * LSeries f s - s * l‖ :=
by
obtain ⟨C, _, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
exact h₁.isBoundedUnder_le.mono_le hC₂
suffices Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s - s * l) (𝓝[>] 1) (𝓝 0)
by
rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
exact (this.add h₃).congr fun _ ↦ by ring
refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_
· exact le_liminf_of_le h₂.isCoboundedUnder_ge (univ_mem' (fun _ ↦ norm_nonneg _))
· refine le_of_forall_pos_le_add fun ε hε ↦ ?_
rw [zero_add]
obtain ⟨C, hC₁, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS hε
refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq
exact isCoboundedUnder_le_of_eventually_le _ (univ_mem' fun _ ↦ norm_nonneg _)
· exact isBoundedUnder_of_eventually_ge (univ_mem' fun _ ↦ norm_nonneg _)
