cauchySeq_series_mul_of_tendsto_zero_of_bounded

English

If f is monotone and tends to 0, then the alternating sum ∑ (-1)^i f(i) is Cauchy.

Русский

Если f монотонна и стремится к 0, то чередующийся ряд ∑ (-1)^i f(i) является Коши.

LaTeX

$$$\forall {f : \mathbb{N} \to \mathbb{R}} (hfa: \text{Monotone } f) (hf0: \text{Tendsto } f \text{ atTop } (\mathcal{N}0)) : CauchySeq (\lambda n, \sum_{i< n} (-1)^i f(i))$$$

Lean4

/-- **Dirichlet's test** for antitone sequences. -/
theorem cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Antitone f) (hf0 : Tendsto f atTop (𝓝 0))
    (hzb : ∀ n, ‖∑ i ∈ range n, z i‖ ≤ b) : CauchySeq fun n ↦ ∑ i ∈ range n, f i • z i :=
  by
  have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
  have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
    convert hf0.neg
    simp
  convert (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg
  simp

Похожие утверждения