Schur's theorem on weak convergence in ℓ¹

TheoremThe \(\ell^1\) norm is the sum of the coordinate norms#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). Every \(x \in \ell^1(\mathbb{N}, \mathbb{K})\) satisfies \(\|x\| = \sum_{i=0}^{\infty} |x_i|\).

theorem l1_norm_eq_tsum (x : lp (fun _ : ℕ => 𝕜) 1) : ‖x‖ = ∑' i, ‖x i‖

Used by 4

Used byPairing \(\ell^1\) with a sequence bounded by one · Pairing with a sequence bounded by one has norm at most one · Schur's theorem · Tail of the norm series of an \(\ell^1\) sequence

TheoremThe pairing of \(\ell^1\) with sequences bounded by \(1\) is summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). If \(y : \mathbb{N} \to \mathbb{K}\) satisfies \(\|y_i\| \le 1\) for every \(i\) and \(x \in \ell^1(\mathbb{N}, \mathbb{K})\), then the series \(\sum_i y_i x_i\) is summable.

theorem summable_bounded_mul_l1 (y : ℕ → 𝕜) (hy : ∀ i, ‖y i‖ ≤ 1)
    (x : lp (fun _ : ℕ => 𝕜) 1) : Summable fun i => y i * x i

Uses 1 · Used by 3

Proof usesCoordinate norms of an \(\ell^1\) family are summable

Used byPairing \(\ell^1\) with a sequence bounded by one · Pairing with a sequence bounded by one has norm at most one · Schur's theorem

DefinitionPairing \(\ell^1\) with a sequence bounded by one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \((y_i)_{i \in \mathbb{N}}\) be a sequence in \(\mathbb{K}\) with \(|y_i| \le 1\) for every \(i\). The pairing with \(y\) is the continuous linear functional \(\ell^1(\mathbb{N}, \mathbb{K}) \to \mathbb{K}\) given by \(x \mapsto \sum_{i=0}^{\infty} y_i x_i\).

MathlibExt.Analysis.FunctionalAnalysis.SchurL1.l1DualOfBounded · 22 lines

noncomputable def l1DualOfBounded (y : ℕ → 𝕜) (hy : ∀ i, ‖y i‖ ≤ 1) :
    lp (fun _ : ℕ => 𝕜) 1 →L[𝕜] 𝕜 :=
  LinearMap.mkContinuous
    { toFun := fun x => ∑' i, y i * x i
      map_add' := fun x z => by
        rw [← Summable.tsum_add (summable_bounded_mul_l1 y hy x) (summable_bounded_mul_l1 y hy z)]
        exact tsum_congr fun i => by simp [mul_add]
      map_smul' := fun c x => by
        rw [smul_eq_mul, ← tsum_mul_left]
        exact tsum_congr fun i => by simp [smul_eq_mul, mul_left_comm] }
    1
    (fun x => by
      rw [one_mul]
      calc ‖∑' i, y i * x i‖ ≤ ∑' i, ‖y i * x i‖ :=
            norm_tsum_le_tsum_norm (summable_bounded_mul_l1 y hy x).norm
        _ ≤ ∑' i, ‖x i‖ :=
            Summable.tsum_le_tsum (fun i => by
              rw [norm_mul]
              calc ‖y i‖ * ‖x i‖ ≤ 1 * ‖x i‖ := by gcongr; exact hy i
                _ = ‖x i‖ := one_mul _)
              (summable_bounded_mul_l1 y hy x).norm (summable_norm_lp_one x)
        _ = ‖x‖ := (l1_norm_eq_tsum x).symm)

Uses 3 · Used by 2

Statement usesThe \(\ell^1\) norm is the sum of the coordinate norms · The pairing of \(\ell^1\) with sequences bounded by \(1\) is summable · Coordinate norms of an \(\ell^1\) family are summable

Used byPairing with a sequence bounded by one has norm at most one · Schur's theorem

TheoremPairing with a sequence bounded by one has norm at most one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \((y_i)_{i \in \mathbb{N}}\) be a sequence in \(\mathbb{K}\) with \(|y_i| \le 1\) for every \(i\). The continuous linear functional \(x \mapsto \sum_{i=0}^{\infty} y_i x_i\) on \(\ell^1(\mathbb{N}, \mathbb{K})\) has operator norm at most \(1\).

theorem norm_l1DualOfBounded_le (y : ℕ → 𝕜) (hy : ∀ i, ‖y i‖ ≤ 1) :
    ‖l1DualOfBounded y hy‖ ≤ 1

Uses 4

Statement usesPairing \(\ell^1\) with a sequence bounded by one

Proof usesThe \(\ell^1\) norm is the sum of the coordinate norms · The pairing of \(\ell^1\) with sequences bounded by \(1\) is summable · Coordinate norms of an \(\ell^1\) family are summable

TheoremSplitting a series into a head, a middle block and a tail#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(h : \mathbb{N} \to \mathbb{K}\) be summable and let \(a \le b\) be natural numbers. Then \(\sum_{i=0}^{\infty} h(i)\) equals \(\sum_{i < a} h(i) + \sum_{a \le i < b} h(i) + \sum_{j=0}^{\infty} h(j + b)\).

theorem tsum_split3 {h : ℕ → 𝕜} (hs : Summable h) {a b : ℕ} (hab : a ≤ b) :
    ∑' i, h i = (∑ i ∈ Finset.range a, h i) + (∑ i ∈ Finset.Ico a b, h i) +
      ∑' j, h (j + b)

Used by 1

Used bySchur's theorem

TheoremTails of an \(\ell^1\) sequence are absolutely summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^1(\mathbb{N}, \mathbb{K})\) and every \(b \in \mathbb{N}\), the series \(\sum_{j=0}^{\infty} \|x_{j+b}\|\) is summable.

theorem summable_norm_shift (x : lp (fun _ : ℕ => 𝕜) 1) (b : ℕ) :
    Summable fun j => ‖x (j + b)‖

Uses 1 · Used by 1

Proof usesCoordinate norms of an \(\ell^1\) family are summable

Used bySchur's theorem

TheoremTail of the norm series of an \(\ell^1\) sequence#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^1(\mathbb{N}, \mathbb{K})\) and every \(b \in \mathbb{N}\), \(\sum_{j=0}^{\infty} \|x_{j+b}\| = \|x\| - \sum_{i < b} \|x_i\|\), where \(\|x\|\) is the \(\ell^1\) norm of \(x\).

theorem tail_tsum_norm (x : lp (fun _ : ℕ => 𝕜) 1) (b : ℕ) :
    ∑' j, ‖x (j + b)‖ = ‖x‖ - ∑ i ∈ Finset.range b, ‖x i‖

Uses 2 · Used by 1

Proof usesThe \(\ell^1\) norm is the sum of the coordinate norms · Coordinate norms of an \(\ell^1\) family are summable

Used bySchur's theorem

DefinitionBlock index for a cutoff sequence#✓fully proved

Let \(M : \mathbb{N} \to \mathbb{N}\) be such that every \(i \in \mathbb{N}\) satisfies \(i < M(k + 1)\) for some \(k\). The block index of \(i \in \mathbb{N}\) is the least \(k\) with \(i < M(k + 1)\).

When \(M\) is monotone and \(M(0) = 0\), the block index of \(i\) is the unique \(k\) with \(M(k) \le i < M(k + 1)\).

noncomputable def schurBlockOf (M' : ℕ → ℕ) (hex : ∀ i, ∃ k, i < M' (k + 1))
    (i : ℕ) : ℕ :=
  Nat.find (hex i)

Used by 5

Used byThe conjugate-sign sequence is bounded by one · Indices in block \(k\) have block index \(k\) · An index lies in the block it is assigned to · Conjugate-sign sequence of a block decomposition · On block \(k\), the conjugate signs recover absolute values

TheoremAn index lies in the block it is assigned to#✓fully proved

Let \(M : \mathbb{N} \to \mathbb{N}\) satisfy \(M(0) = 0\), and suppose every \(i \in \mathbb{N}\) satisfies \(i < M(j + 1)\) for some \(j\). For every \(i \in \mathbb{N}\), if \(k\) is the block index of \(i\) (the least \(k\) with \(i < M(k + 1)\)), then \(M(k) \le i < M(k + 1)\).

theorem schurBlockOf_mem (M' : ℕ → ℕ) (hM'0 : M' 0 = 0)
    (hex : ∀ i, ∃ k, i < M' (k + 1)) (i : ℕ) :
    i ∈ Finset.Ico (M' (schurBlockOf M' hex i)) (M' (schurBlockOf M' hex i + 1))

Uses 1

Statement usesBlock index for a cutoff sequence

TheoremIndices in block \(k\) have block index \(k\)#✓fully proved

Let \(M : \mathbb{N} \to \mathbb{N}\) be monotone, and suppose every \(i \in \mathbb{N}\) satisfies \(i < M(j + 1)\) for some \(j\). For all \(k, i \in \mathbb{N}\) with \(M(k) \le i < M(k + 1)\), the block index of \(i\) (the least \(j\) with \(i < M(j + 1)\)) is \(k\).

theorem schurBlockOf_eq {M' : ℕ → ℕ} (hmono : Monotone M')
    (hex : ∀ i, ∃ k, i < M' (k + 1)) (k : ℕ)
    {i : ℕ} (hi : i ∈ Finset.Ico (M' k) (M' (k + 1))) :
    schurBlockOf M' hex i = k

Uses 1 · Used by 1

Statement usesBlock index for a cutoff sequence

Used byOn block \(k\), the conjugate signs recover absolute values

DefinitionConjugate-sign sequence of a block decomposition#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \((x_n)\) be a sequence in \(\ell^1(\mathbb{N}, \mathbb{K})\), let \(n' : \mathbb{N} \to \mathbb{N}\), and let \(M : \mathbb{N} \to \mathbb{N}\) be such that every \(i \in \mathbb{N}\) satisfies \(i < M(j + 1)\) for some \(j\). For \(i \in \mathbb{N}\), let \(k\) be the block index of \(i\) (the least \(k\) with \(i < M(k + 1)\)) and let \(v = x_{n'(k)}(i)\). The \(i\)-th term \(\sigma_i\) of the conjugate-sign sequence is \(0\) if \(v = 0\), and \(\overline{v} / |v|\) otherwise.

noncomputable def schurSignSeq (x : ℕ → lp (fun _ : ℕ => 𝕜) 1) (n' : ℕ → ℕ)
    (M' : ℕ → ℕ) (hex : ∀ i, ∃ k, i < M' (k + 1)) (i : ℕ) : 𝕜 :=
  if x (n' (schurBlockOf M' hex i)) i = 0 then 0
  else starRingEnd 𝕜 (x (n' (schurBlockOf M' hex i)) i) /
    (‖x (n' (schurBlockOf M' hex i)) i‖ : 𝕜)

Uses 1 · Used by 3

Statement usesBlock index for a cutoff sequence

Used byThe conjugate-sign sequence is bounded by one · On block \(k\), the conjugate signs recover absolute values · Schur's theorem

TheoremThe conjugate-sign sequence is bounded by one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \((x_n)\) be a sequence in \(\ell^1(\mathbb{N}, \mathbb{K})\), let \(n' : \mathbb{N} \to \mathbb{N}\), and let \(M : \mathbb{N} \to \mathbb{N}\) be such that every \(i \in \mathbb{N}\) satisfies \(i < M(j + 1)\) for some \(j\). Every term \(\sigma_i\) of the conjugate-sign sequence of \((x_n)\), \(n'\) and \(M\) satisfies \(|\sigma_i| \le 1\).

theorem norm_schurSignSeq_le (x : ℕ → lp (fun _ : ℕ => 𝕜) 1) (n' : ℕ → ℕ)
    (M' : ℕ → ℕ) (hex : ∀ i, ∃ k, i < M' (k + 1)) (i : ℕ) :
    ‖schurSignSeq x n' M' hex i‖ ≤ 1

Uses 2 · Used by 1

Statement usesConjugate-sign sequence of a block decomposition

Proof usesBlock index for a cutoff sequence

Used bySchur's theorem

TheoremOn block \(k\), the conjugate signs recover absolute values#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \((x_n)\) be a sequence in \(\ell^1(\mathbb{N}, \mathbb{K})\), let \(n' : \mathbb{N} \to \mathbb{N}\), and let \(M : \mathbb{N} \to \mathbb{N}\) be monotone and such that every \(i \in \mathbb{N}\) satisfies \(i < M(j + 1)\) for some \(j\). Let \(\sigma\) be the conjugate-sign sequence of \((x_n)\), \(n'\) and \(M\). For all \(k, i \in \mathbb{N}\) with \(M(k) \le i < M(k + 1)\), we have \(\sigma_i \, x_{n'(k)}(i) = |x_{n'(k)}(i)|\).

theorem schurSignSeq_mul (x : ℕ → lp (fun _ : ℕ => 𝕜) 1) (n' : ℕ → ℕ)
    (M' : ℕ → ℕ) (hmono : Monotone M') (hex : ∀ i, ∃ k, i < M' (k + 1)) (k : ℕ)
    {i : ℕ} (hi : i ∈ Finset.Ico (M' k) (M' (k + 1))) :
    schurSignSeq x n' M' hex i * x (n' k) i = (‖x (n' k) i‖ : 𝕜)

Uses 3 · Used by 1

Statement usesConjugate-sign sequence of a block decomposition

Proof usesBlock index for a cutoff sequence · Indices in block \(k\) have block index \(k\)

Used bySchur's theorem

TheoremSchur's theorem#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \((x_n)\) be a sequence in \(\ell^1(\mathbb{N}, \mathbb{K})\) and let \(x_0 \in \ell^1(\mathbb{N}, \mathbb{K})\). If \(F(x_n) \to F(x_0)\) for every continuous linear functional \(F\) on \(\ell^1(\mathbb{N}, \mathbb{K})\), that is, if \((x_n)\) converges weakly to \(x_0\), then \(x_n \to x_0\) in the \(\ell^1\) norm.

theorem schur_tendsto_of_weak_tendsto {x : ℕ → lp (fun _ : ℕ => 𝕜) 1}
    {x₀ : lp (fun _ : ℕ => 𝕜) 1}
    (hx : ∀ F : lp (fun _ : ℕ => 𝕜) 1 →L[𝕜] 𝕜,
      Tendsto (fun n => F (x n)) atTop (𝓝 (F x₀))) :
    Tendsto x atTop (𝓝 x₀)

Uses 10 · Used by 1

Proof usesPairing \(\ell^1\) with a sequence bounded by one · The \(\ell^1\) norm is the sum of the coordinate norms · The conjugate-sign sequence is bounded by one · Conjugate-sign sequence of a block decomposition · On block \(k\), the conjugate signs recover absolute values · The pairing of \(\ell^1\) with sequences bounded by \(1\) is summable · Tails of an \(\ell^1\) sequence are absolutely summable · Tail of the norm series of an \(\ell^1\) sequence · Splitting a series into a head, a middle block and a tail · Coordinate norms of an \(\ell^1\) family are summable

Used bySchur's theorem, norm form

TheoremSchur's theorem, norm form#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \((x_n)\) be a sequence in \(\ell^1(\mathbb{N}, \mathbb{K})\), and let \(x \in \ell^1(\mathbb{N}, \mathbb{K})\). If \(F(x_n) \to F(x)\) as \(n \to \infty\) for every continuous linear functional \(F : \ell^1(\mathbb{N}, \mathbb{K}) \to \mathbb{K}\), then \(\|x_n - x\| \to 0\) as \(n \to \infty\).

theorem schur_tendsto_norm_sub_of_weak_tendsto {x : ℕ → lp (fun _ : ℕ => 𝕜) 1}
    {x₀ : lp (fun _ : ℕ => 𝕜) 1}
    (hx : ∀ F : lp (fun _ : ℕ => 𝕜) 1 →L[𝕜] 𝕜,
      Tendsto (fun n => F (x n)) atTop (𝓝 (F x₀))) :
    Tendsto (fun n => ‖x n - x₀‖) atTop (𝓝 0)

Uses 1

Proof usesSchur's theorem

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.