Root test

TheoremCauchy's root test, absolute convergence case#✓fully proved

Let \(f : \mathbb{N} \to \alpha\) be a sequence in a normed additive commutative group \(\alpha\). If \(\|f(n)\|^{1/n}\) tends to a real limit \(l\) with \(l < 1\) as \(n \to \infty\), then the series \(\sum_n \|f(n)\|\) converges.

theorem summable_norm_of_root_test_tendsto_lt_one [NormedAddCommGroup α]
    {l : ℝ} (hl : l < 1)
    (h : Filter.Tendsto (fun n => ‖f n‖ ^ ((1 : ℝ) / n)) Filter.atTop (𝓝 l)) :
    Summable (fun n => ‖f n‖)

Used by 1

Used byCauchy's root test, convergence case

TheoremCauchy's root test, convergence case#✓fully proved

Let \(f : \mathbb{N} \to \alpha\) be a sequence in a complete normed additive commutative group \(\alpha\). If \(\|f(n)\|^{1/n}\) tends to a real limit \(l\) with \(l < 1\) as \(n \to \infty\), then \(f\) is summable, that is, the series \(\sum_n f(n)\) converges unconditionally.

theorem summable_of_root_test_tendsto_lt_one [NormedAddCommGroup α] [CompleteSpace α]
    {l : ℝ} (hl : l < 1)
    (h : Filter.Tendsto (fun n => ‖f n‖ ^ ((1 : ℝ) / n)) Filter.atTop (𝓝 l)) :
    Summable f

Uses 1

Proof usesCauchy's root test, absolute convergence case

TheoremCauchy's root test, divergence case#✓fully proved

Let \(f : \mathbb{N} \to \alpha\) be a sequence in a seminormed additive commutative group \(\alpha\). If \(\|f(n)\|^{1/n}\) tends to a real limit \(l\) with \(l > 1\) as \(n \to \infty\), then \(f\) is not summable, that is, the series \(\sum_n f(n)\) does not converge unconditionally.

theorem not_summable_of_root_test_tendsto_gt_one [SeminormedAddCommGroup α]
    {l : ℝ} (hl : 1 < l)
    (h : Filter.Tendsto (fun n => ‖f n‖ ^ ((1 : ℝ) / n)) Filter.atTop (𝓝 l)) :
    ¬Summable f

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.