Riemann rearrangement theorem

DefinitionConvergence of a series in order#✓fully proved

For a sequence \(f : \mathbb{N} \to \mathbb{R}\) and \(a \in \mathbb{R}\), the series \(\sum_n f(n)\) converges in order to \(a\) when its partial sums \(\sum_{n=0}^{N-1} f(n)\) tend to \(a\) as \(N \to \infty\).

def OrderedHasSum (f : ℕ → ℝ) (a : ℝ) : Prop :=
  Filter.Tendsto (fun N => ∑ n ∈ Finset.range N, f n) Filter.atTop (nhds a)

Used by 3

Used byConvergence in order via partial sums · Terms of a convergent series tend to zero · Riemann rearrangement theorem

TheoremConvergence in order via partial sums#✓fully proved

For a sequence \(f : \mathbb{N} \to \mathbb{R}\) and \(a \in \mathbb{R}\), the series \(\sum_n f(n)\) converges in order to \(a\) if and only if its partial sums \(\sum_{n=0}^{N-1} f(n)\) tend to \(a\) as \(N \to \infty\).

theorem orderedHasSum_iff (f : ℕ → ℝ) (a : ℝ) :
    OrderedHasSum f a ↔
      Filter.Tendsto (fun N => ∑ n ∈ Finset.range N, f n) Filter.atTop (nhds a)

Uses 1

Statement usesConvergence of a series in order

TheoremTerms of a convergent series tend to zero#✓fully proved

If \(f : \mathbb{N} \to \mathbb{R}\) and the series \(\sum_n f(n)\) converges in order to some \(s \in \mathbb{R}\), then \(f(n) \to 0\) as \(n \to \infty\).

theorem orderedHasSum_tendsto_zero (f : ℕ → ℝ) (s : ℝ) (h : OrderedHasSum f s) :
    Filter.Tendsto f Filter.atTop (nhds 0)

Uses 1 · Used by 1

Statement usesConvergence of a series in order

Used byRiemann rearrangement theorem

TheoremRiemann rearrangement theorem#✓fully proved

Let \(f : \mathbb{N} \to \mathbb{R}\) be such that the series \(\sum_n f(n)\) converges in order to some real number, while the series \(\sum_n |f(n)|\) is not summable. Then for every \(a \in \mathbb{R}\) there is a permutation \(\sigma\) of \(\mathbb{N}\) such that the rearranged series \(\sum_n f(\sigma(n))\) converges in order to \(a\).

theorem riemann_rearrangement
    (f : ℕ → ℝ) (hf : ∃ s, OrderedHasSum f s)
    (hfa : ¬ Summable (fun n => |f n|)) (a : ℝ) :
    ∃ e : Equiv.Perm ℕ, OrderedHasSum (fun n => f (e n)) a

Sources

B. Riemann, Über die Darstellbarkeit einer Function durch eine trigonometrische Reihe, Habilitationsschrift (1854; published 1867).

Uses 2

Statement usesConvergence of a series in order

Proof usesTerms of a convergent series tend to zero

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.