Limits of specific sequences and partial sums

DefinitionPartial sums of \(a_k + 1/a_k\)#✓fully proved

For a real sequence \((a_k)_{k \in \mathbb{N}}\), the sequence \((x_n)_{n \in \mathbb{N}}\) is given by \(x_n = \sum_{k=0}^{n} (a_k + 1/a_k)\) for \(n \in \mathbb{N}\), with the convention \(1/0 = 0\).

noncomputable def xSeq (a : ℕ → ℝ) : ℕ → ℝ :=
  fun n ↦ ∑ k ∈ Finset.range (n + 1), (a k + (1 / a k))

Used by 1

Used byThe reciprocals of \(\sum_{k=0}^{n} (a_k + 1/a_k)\) tend to zero

TheoremThe reciprocals of \(\sum_{k=0}^{n} (a_k + 1/a_k)\) tend to zero#●ready to prove

Let \((a_n)_{n \in \mathbb{N}}\) be a sequence of positive real numbers, and for \(n \in \mathbb{N}\) let \(x_n = \sum_{k=0}^{n} (a_k + 1/a_k)\). Then \(1/x_n \to 0\) as \(n \to \infty\).

public theorem_wanted tendsto_one_div_sum_add_inv_zero (a : ℕ → ℝ) (ha : ∀ n : ℕ, 0 < a n) :
    Tendsto (fun n ↦ 1 / xSeq a n) atTop (𝓝 0)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Sequences, series, summability; Convergence and divergence of infinite limiting processes), problem ma_proofbench_l1_18.

Uses 1

Statement usesPartial sums of \(a_k + 1/a_k\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.