English
If f is monotone and tends to 0, and the sequence of z has bounded partial sums, then the series ∑ f(n) z(n) converges in a Cauchy sense.
Русский
Если f монотонна и стремится к 0, а частичные суммы z ограничены, то ∑ f(n) z(n) сходится (Коши).
LaTeX
$$$\forall {E} [\text{NormedAddCommGroup } E] (f : \mathbb{N} \to \mathbb{R}) (z : \mathbb{N} \to E) (hfa:\text{Monotone } f) (hf0: \text{Tendsto } f \text{ atTop } (\mathcal{N}0)) (hgb: \forall n, \|\sum_{i< n} z(i)\| ≤ b) : CauchySeq (\lambda n, \sum_{i< n} f(i) • z(i))$$$
Lean4
/-- **Dirichlet's test** for monotone sequences. -/
theorem cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0))
(hgb : ∀ n, ‖∑ i ∈ range n, z i‖ ≤ b) : CauchySeq fun n ↦ ∑ i ∈ range n, f i • z i :=
by
rw [← cauchySeq_shift 1]
simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub, tsub_zero]
apply
(NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
⟨b, eventually_map.mpr <| Eventually.of_forall fun n ↦ hgb <| n + 1⟩).cauchySeq.add
refine CauchySeq.neg ?_
refine
cauchySeq_range_of_norm_bounded ?_
(fun n ↦ ?_ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)
· simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (Nat.le_succ _))), ← mul_sum]
apply Real.uniformContinuous_const_mul.comp_cauchySeq
simp_rw [sum_range_sub, sub_eq_add_neg]
exact (Tendsto.cauchySeq hf0).add_const
· rw [norm_smul, mul_comm]
exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)
