Cesàro operator

AbbreviationThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\)#✓fully proved

For \(\mathbb{K}\) equal to \(\mathbb{R}\) or \(\mathbb{C}\), this is the space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences \(x : \mathbb{N} \to \mathbb{K}\), with the norm \(\|x\| = \left(\sum_{n} |x(n)|^2\right)^{1/2}\).

abbrev CesaroSpace (𝕜 : Type*) [RCLike 𝕜] := lp (fun _ : ℕ => 𝕜) 2

Used by 28

Used byAdjoint of the Cesàro operator · The adjoint of the Cesàro operator fixes the first basis vector · Cesàro operator on square-summable sequences · Formula for the Cesàro operator · Second coordinate of the Cesàro operator at the first basis vector · The Cesàro operator agrees with the Cesàro linear map · The Cesàro operator is injective · The Cesàro operator on standard basis vectors · The Cesàro operator on a test vector, past its support · The Cesàro operator on a test vector, within its support · The first standard basis vector of \(\ell^2\) · The Cesàro operator as a linear map · The alternating harmonic sequence in \(\ell^2\) · One step of inverting the Cesàro operator · Partial sums from Cesàro means · Cesàro test vectors · Lower bound for the Cesàro operator on the test vectors · Cesàro means preserve square-summability · The Cesàro operator has norm at most 2 · The first basis vector is a unit vector · The Cesàro operator is bounded by 2 · The Cesàro test vectors are unit vectors · The Cesàro operator is not compact · The Cesàro operator is not self-adjoint · The Cesàro operator is not surjective · The Cesàro operator has norm at least one · Cesàro means of square-summable sequences are square-summable · The Cesàro images of the test vectors tend to zero coordinatewise

DefinitionCesàro means of a sequence#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For a sequence \(x : \mathbb{N} \to \mathbb{K}\) and \(n \in \mathbb{N}\), the \(n\)-th Cesàro mean of \(x\) is the average of its first \(n + 1\) terms, \(\frac{1}{n+1} \sum_{k=0}^{n} x(k)\).

def cesaroMean (x : ℕ → 𝕜) (n : ℕ) : 𝕜 :=
  (∑ k ∈ Finset.range (n + 1), x k) / ((n : 𝕜) + 1)

Used by 4

Used byThe Cesàro operator as a linear map · Cesàro means preserve square-summability · A Cesàro mean is bounded by the mean of the norms · Cesàro means of square-summable sequences are square-summable

LemmaNorm of the Cesàro denominator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every natural number \(n\), the element \(n + 1\) of \(\mathbb{K}\) (the denominator of the \(n\)-th Cesàro mean) has norm equal to the real number \(n + 1\).

lemma norm_cesaro_den (n : ℕ) : ‖((n : 𝕜) + 1)‖ = (n : ℝ) + 1

Used by 3

Used byThe alternating harmonic sequence in \(\ell^2\) · Lower bound for the Cesàro operator on the test vectors · A Cesàro mean is bounded by the mean of the norms

LemmaA Cesàro mean is bounded by the mean of the norms#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(x : \mathbb{N} \to \mathbb{K}\) be any sequence and let \(n\) be a natural number. Then \(\|\frac{1}{n+1} \sum_{k=0}^{n} x_k\| \le \frac{1}{n+1} \sum_{k=0}^{n} \|x_k\|\).

lemma norm_cesaroMean_le (x : ℕ → 𝕜) (n : ℕ) :
    ‖cesaroMean x n‖ ≤ (∑ k ∈ Finset.range (n + 1), ‖x k‖) / ((n : ℝ) + 1)

Uses 2 · Used by 2

Statement usesCesàro means of a sequence

Proof usesNorm of the Cesàro denominator

Used byThe Cesàro operator is bounded by 2 · Cesàro means of square-summable sequences are square-summable

LemmaCesàro means of square-summable sequences are square-summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the Cesàro means \(\sigma_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\) satisfy: the series \(\sum_n |\sigma_n|^2\) converges.

This follows from Hardy's inequality at \(p = 2\).

lemma summable_norm_sq_cesaroMean (x : CesaroSpace 𝕜) :
    Summable fun n => ‖cesaroMean (x : ℕ → 𝕜) n‖ ^ (2 : ℝ)

Uses 4 · Used by 2

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro means of a sequence

Proof usesA Cesàro mean is bounded by the mean of the norms · Hardy's inequality

Used byCesàro means preserve square-summability · The Cesàro operator is bounded by 2

LemmaCesàro means preserve square-summability#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). If \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), then the sequence of its Cesàro means \(n \mapsto \frac{1}{n+1} \sum_{k=0}^{n} x_k\) also lies in \(\ell^2(\mathbb{N}, \mathbb{K})\).

lemma memℓp_cesaroMean (x : CesaroSpace 𝕜) : Memℓp (cesaroMean (x : ℕ → 𝕜)) 2

Uses 3 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro means of a sequence

Proof usesCesàro means of square-summable sequences are square-summable

Used byThe Cesàro operator as a linear map

DefinitionThe Cesàro operator as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator is the \(\mathbb{K}\)-linear map \(C\) from \(\ell^2(\mathbb{N}, \mathbb{K})\) to itself that sends a sequence \(x\) to its sequence of Cesàro means, \((Cx)(n) = \frac{1}{n+1} \sum_{k=0}^{n} x(k)\) for \(n \in \mathbb{N}\).

That \(Cx\) is again square-summable follows from Hardy's inequality.

def cesaroLinearMap : CesaroSpace 𝕜 →ₗ[𝕜] CesaroSpace 𝕜 where
  toFun x := ⟨cesaroMean (x : ℕ → 𝕜), memℓp_cesaroMean x⟩
  map_add' x y := by
    ext n
    simp only [cesaroMean, lp.coeFn_add, Pi.add_apply]
    rw [Finset.sum_add_distrib, add_div]
  map_smul' c x := by
    ext n
    simp only [cesaroMean, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
    rw [← Finset.mul_sum, mul_div_assoc]

Uses 3 · Used by 4

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro means of a sequence · Cesàro means preserve square-summability

Used byCesàro operator on square-summable sequences · The Cesàro operator agrees with the Cesàro linear map · The Cesàro operator has norm at most 2 · The Cesàro operator is bounded by 2

LemmaThe Cesàro operator is bounded by 2#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), viewed as a linear map, given by \((Cx)_n = \frac{1}{n+1} \sum_{k=0}^{n} x_k\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), \(\|Cx\| \le 2 \|x\|\).

lemma norm_cesaroLinearMap_le (x : CesaroSpace 𝕜) :
    ‖cesaroLinearMap (𝕜 := 𝕜) x‖ ≤ 2 * ‖x‖

Uses 5 · Used by 2

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · The Cesàro operator as a linear map

Proof usesA Cesàro mean is bounded by the mean of the norms · Cesàro means of square-summable sequences are square-summable · Hardy's inequality

Used byCesàro operator on square-summable sequences · The Cesàro operator has norm at most 2

DefinitionCesàro operator on square-summable sequences#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator \(C\) is the continuous linear map from \(\ell^2(\mathbb{N}, \mathbb{K})\) to itself that sends a sequence \(x\) to its sequence of averages, \((Cx)_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\). It is obtained from the Cesàro linear map with the bound \(\|Cx\| \le 2 \|x\|\).

def cesaroCLM : CesaroSpace 𝕜 →L[𝕜] CesaroSpace 𝕜 :=
  LinearMap.mkContinuous cesaroLinearMap 2 (fun x => norm_cesaroLinearMap_le x)

Uses 3 · Used by 18

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · The Cesàro operator as a linear map · The Cesàro operator is bounded by 2

Used byAdjoint of the Cesàro operator · The adjoint of the Cesàro operator fixes the first basis vector · Formula for the Cesàro operator · Second coordinate of the Cesàro operator at the first basis vector · The Cesàro operator agrees with the Cesàro linear map · The Cesàro operator is injective · The Cesàro operator on standard basis vectors · The Cesàro operator on a test vector, past its support · The Cesàro operator on a test vector, within its support · One step of inverting the Cesàro operator · Partial sums from Cesàro means · Lower bound for the Cesàro operator on the test vectors · The Cesàro operator has norm at most 2 · The Cesàro operator is not compact · The Cesàro operator is not self-adjoint · The Cesàro operator is not surjective · The Cesàro operator has norm at least one · The Cesàro images of the test vectors tend to zero coordinatewise

TheoremFormula for the Cesàro operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(n \in \mathbb{N}\), \((Cx)_n = \bigl(\sum_{k=0}^{n} x_k\bigr)/(n + 1)\).

theorem cesaroCLM_apply (x : CesaroSpace 𝕜) (n : ℕ) :
    cesaroCLM (𝕜 := 𝕜) x n = (∑ k ∈ Finset.range (n + 1), (x : ℕ → 𝕜) k) / ((n : 𝕜) + 1)

Uses 2 · Used by 6

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Used bySecond coordinate of the Cesàro operator at the first basis vector · The Cesàro operator on standard basis vectors · The Cesàro operator on a test vector, past its support · The Cesàro operator on a test vector, within its support · Partial sums from Cesàro means · The Cesàro operator has norm at least one

LemmaPartial sums from Cesàro means#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(n \in \mathbb{N}\), \(\sum_{k=0}^{n} x(k) = (n+1)\,(Cx)(n)\).

lemma cesaro_sum_eq (x : CesaroSpace 𝕜) (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1), (x : ℕ → 𝕜) k) = ((n : 𝕜) + 1) * cesaroCLM (𝕜 := 𝕜) x n

Uses 3 · Used by 2

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesFormula for the Cesàro operator

Used byThe Cesàro operator is injective · One step of inverting the Cesàro operator

LemmaThe Cesàro operator agrees with the Cesàro linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the Cesàro operator, as a continuous linear map on \(\ell^2(\mathbb{N}, \mathbb{K})\), takes the same value at \(x\) as the Cesàro linear map, the same averaging map considered only as a linear map.

lemma cesaroCLM_eq (x : CesaroSpace 𝕜) :
    cesaroCLM (𝕜 := 𝕜) x = cesaroLinearMap (𝕜 := 𝕜) x

Uses 3 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · The Cesàro operator as a linear map

Used byThe Cesàro operator has norm at most 2

TheoremThe Cesàro operator has norm at most 2#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator \(C\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = \frac{1}{n+1} \sum_{k=0}^{n} x_k\), has operator norm \(\|C\| \le 2\).

theorem norm_cesaroCLM_le : ‖cesaroCLM (𝕜 := 𝕜)‖ ≤ 2

Uses 5

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesThe Cesàro operator agrees with the Cesàro linear map · The Cesàro operator as a linear map · The Cesàro operator is bounded by 2

DefinitionThe first standard basis vector of \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The vector \(e_0 \in \ell^2(\mathbb{N}, \mathbb{K})\) is the sequence with \(e_0(0) = 1\) and \(e_0(n) = 0\) for every \(n \ge 1\).

def cesaroE0 : CesaroSpace 𝕜 := lp.single (E := fun _ : ℕ => 𝕜) 2 0 (1 : 𝕜)

Uses 1 · Used by 6

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\)

Used byThe adjoint of the Cesàro operator fixes the first basis vector · Second coordinate of the Cesàro operator at the first basis vector · Coordinates of the first standard basis vector of \(\ell^2\) · The first basis vector is a unit vector · The Cesàro operator is not self-adjoint · The Cesàro operator has norm at least one

LemmaCoordinates of the first standard basis vector of \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(e_0 \in \ell^2(\mathbb{N}, \mathbb{K})\) be the first standard basis vector. For every \(n \in \mathbb{N}\), \(e_0(n) = 1\) if \(n = 0\) and \(e_0(n) = 0\) otherwise.

lemma cesaroE0_apply (n : ℕ) : cesaroE0 (𝕜 := 𝕜) n = if n = 0 then 1 else 0

Uses 1 · Used by 4

Statement usesThe first standard basis vector of \(\ell^2\)

Used byThe adjoint of the Cesàro operator fixes the first basis vector · Second coordinate of the Cesàro operator at the first basis vector · The Cesàro operator is not self-adjoint · The Cesàro operator has norm at least one

LemmaThe first basis vector is a unit vector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The first standard basis vector \(e_0 = (1, 0, 0, \dots)\) of \(\ell^2(\mathbb{N}, \mathbb{K})\) has norm \(\|e_0\| = 1\).

lemma norm_cesaroE0 : ‖cesaroE0 (𝕜 := 𝕜)‖ = 1

Uses 2 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · The first standard basis vector of \(\ell^2\)

Used byThe Cesàro operator has norm at least one

TheoremThe Cesàro operator has norm at least one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator \(C\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\), has operator norm \(\|C\| \ge 1\).

This is seen on the first basis vector \(e_0\), for which \(\|e_0\| = 1\) and \((C e_0)_0 = 1\).

theorem one_le_norm_cesaroCLM : 1 ≤ ‖cesaroCLM (𝕜 := 𝕜)‖

Uses 6

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesFormula for the Cesàro operator · The first standard basis vector of \(\ell^2\) · Coordinates of the first standard basis vector of \(\ell^2\) · The first basis vector is a unit vector

LemmaOne step of inverting the Cesàro operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(n \in \mathbb{N}\), \(x(n+1) = (n+2)\,(Cx)(n+1) - (n+1)\,(Cx)(n)\).

lemma cesaro_preimage_succ (x : CesaroSpace 𝕜) (n : ℕ) :
    (x : ℕ → 𝕜) (n + 1) =
      ((n : 𝕜) + 2) * cesaroCLM (𝕜 := 𝕜) x (n + 1) -
        ((n : 𝕜) + 1) * cesaroCLM (𝕜 := 𝕜) x n

Uses 3 · Used by 2

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesPartial sums from Cesàro means

Used byThe Cesàro operator is injective · The Cesàro operator is not surjective

TheoremThe Cesàro operator is injective#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator \(C\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = (x_0 + \dots + x_n)/(n + 1)\), is injective.

theorem cesaroCLM_injective : Function.Injective (cesaroCLM (𝕜 := 𝕜))

Uses 4

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesOne step of inverting the Cesàro operator · Partial sums from Cesàro means

DefinitionThe alternating harmonic sequence in \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The sequence \(y\) with \(y(n) = (-1)^n / (n + 1)\) for \(n \in \mathbb{N}\) is square-summable, and it is regarded as an element of \(\ell^2(\mathbb{N}, \mathbb{K})\).

MathlibExt.Analysis.FunctionalAnalysis.CesaroOperator.cesaroNonRange · 16 lines

def cesaroNonRange : CesaroSpace 𝕜 :=
  ⟨fun n => (-1 : 𝕜) ^ n / ((n : 𝕜) + 1), by
    apply memℓp_gen
    have hto : (2 : ℝ≥0∞).toReal = 2 := by simp
    rw [hto]
    have hnorm : ∀ n : ℕ, ‖(-1 : 𝕜) ^ n / ((n : 𝕜) + 1)‖ = 1 / ((n : ℝ) + 1) := by
      intro n
      rw [norm_div, norm_pow, norm_neg, norm_one, one_pow, norm_cesaro_den, one_div]
    have hs : Summable fun n : ℕ => (1 / ((n : ℝ) + 1)) ^ (2 : ℝ) := by
      have h1 : Summable fun n : ℕ => (1 / (n : ℝ) ^ 2) :=
        Real.summable_one_div_nat_pow.mpr (by norm_num)
      have h2 := (summable_nat_add_iff (f := fun n : ℕ => (1 / (n : ℝ) ^ 2)) 1).mpr h1
      refine h2.congr (fun n => ?_)
      rw [Real.rpow_two, div_pow, one_pow]
      norm_cast
    exact hs.congr fun n => by rw [hnorm n]⟩

Uses 2 · Used by 2

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Norm of the Cesàro denominator

Used byCoordinates of the alternating harmonic sequence in \(\ell^2\) · The Cesàro operator is not surjective

LemmaCoordinates of the alternating harmonic sequence in \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(y\) be the alternating harmonic sequence, viewed as an element of \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(n \in \mathbb{N}\), \(y(n) = (-1)^n / (n + 1)\).

lemma cesaroNonRange_apply (n : ℕ) :
    cesaroNonRange (𝕜 := 𝕜) n = (-1 : 𝕜) ^ n / ((n : 𝕜) + 1)

Uses 1 · Used by 1

Statement usesThe alternating harmonic sequence in \(\ell^2\)

Used byThe Cesàro operator is not surjective

TheoremThe Cesàro operator is not surjective#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The sequence \(y \in \ell^2(\mathbb{N}, \mathbb{K})\) with \(y_n = (-1)^n/(n + 1)\) is not in the range of the Cesàro operator \(C\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\). In particular \(C\) is not surjective.

A preimage \(x\) would have to satisfy \(x_{n+1} = -2(-1)^n\) for all \(n\), so it would not be square-summable.

theorem notMem_range_cesaroCLM : cesaroNonRange (𝕜 := 𝕜) ∉ Set.range (cesaroCLM (𝕜 := 𝕜))

Uses 5

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · The alternating harmonic sequence in \(\ell^2\)

Proof usesCoordinates of the alternating harmonic sequence in \(\ell^2\) · One step of inverting the Cesàro operator

LemmaThe Cesàro operator on standard basis vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), and for \(n \in \mathbb{N}\) let \(e_n\) be the standard basis vector with \(1\) in coordinate \(n\) and \(0\) elsewhere. For all \(n, k \in \mathbb{N}\), \((C e_n)_k = 1/(k + 1)\) if \(n \le k\), and \((C e_n)_k = 0\) if \(k < n\).

lemma cesaroCLM_single_apply (n k : ℕ) :
    cesaroCLM (𝕜 := 𝕜) (lp.single (E := fun _ : ℕ => 𝕜) 2 n (1 : 𝕜)) k =
      if n ≤ k then 1 / ((k : 𝕜) + 1) else 0

Uses 3 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesFormula for the Cesàro operator

Used byAdjoint of the Cesàro operator

TheoremAdjoint of the Cesàro operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = (x_0 + \dots + x_n)/(n + 1)\). For every \(y \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(n \in \mathbb{N}\), the adjoint \(C^*\) of \(C\) satisfies

\[(C^* y)_n = \sum_{k=0}^{\infty} \frac{y_{n+k}}{n + k + 1}.\]

theorem cesaro_adjoint_apply (y : CesaroSpace 𝕜) (n : ℕ) :
    ContinuousLinearMap.adjoint (cesaroCLM (𝕜 := 𝕜)) y n =
      ∑' k, (y : ℕ → 𝕜) (n + k) / (((n + k : ℕ) : 𝕜) + 1)

Uses 3 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesThe Cesàro operator on standard basis vectors

Used byThe adjoint of the Cesàro operator fixes the first basis vector

TheoremThe adjoint of the Cesàro operator fixes the first basis vector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), and let \(e_0 = (1, 0, 0, \dots)\) be the first standard basis vector. Then \(C^* e_0 = e_0\), where \(C^*\) is the adjoint of \(C\).

theorem cesaro_adjoint_single_zero :
    ContinuousLinearMap.adjoint (cesaroCLM (𝕜 := 𝕜)) cesaroE0 = cesaroE0

Uses 5 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · The first standard basis vector of \(\ell^2\)

Proof usesCoordinates of the first standard basis vector of \(\ell^2\) · Adjoint of the Cesàro operator

Used byThe Cesàro operator is not self-adjoint

TheoremSecond coordinate of the Cesàro operator at the first basis vector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), and let \(e_0 = (1, 0, 0, \dots)\) be the first standard basis vector. With coordinates indexed from \(0\), \((C e_0)_1 = 1/2\).

theorem cesaroCLM_e0_apply_one : cesaroCLM (𝕜 := 𝕜) cesaroE0 1 = 1 / 2

Uses 5 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · The first standard basis vector of \(\ell^2\)

Proof usesFormula for the Cesàro operator · Coordinates of the first standard basis vector of \(\ell^2\)

Used byThe Cesàro operator is not self-adjoint

TheoremThe Cesàro operator is not self-adjoint#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator \(C\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\), is not self-adjoint.

Indeed, its adjoint fixes the first basis vector \(e_0\), while \((C e_0)_1 = 1/2\).

theorem not_isSelfAdjoint_cesaroCLM : ¬ IsSelfAdjoint (cesaroCLM (𝕜 := 𝕜))

Uses 6

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesSecond coordinate of the Cesàro operator at the first basis vector · The first standard basis vector of \(\ell^2\) · Coordinates of the first standard basis vector of \(\ell^2\) · The adjoint of the Cesàro operator fixes the first basis vector

DefinitionCesàro test vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(e_i\) be the \(i\)-th standard basis vector of \(\ell^2(\mathbb{N}, \mathbb{K})\). For a natural number \(N\), the test vector \(t_N = \sum_{i < N} \frac{1}{\sqrt{N}} e_i\) has coordinate \(1/\sqrt{N}\) at each \(j < N\) and \(0\) at each \(j \ge N\); in particular \(t_0 = 0\).

These vectors are used to show that the Cesàro operator is not compact.

def cesaroTest (N : ℕ) : CesaroSpace 𝕜 :=
  ∑ i ∈ Finset.range N, ((Real.sqrt N : ℝ) : 𝕜)⁻¹ • lp.single (E := fun _ : ℕ => 𝕜) 2 i (1 : 𝕜)

Uses 1 · Used by 7

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\)

Used byThe Cesàro operator on a test vector, past its support · The Cesàro operator on a test vector, within its support · Coordinates of the Cesàro test vectors · Lower bound for the Cesàro operator on the test vectors · The Cesàro test vectors are unit vectors · The Cesàro operator is not compact · The Cesàro images of the test vectors tend to zero coordinatewise

LemmaCoordinates of the Cesàro test vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(N\) and \(j\) be natural numbers. The \(j\)-th coordinate of the Cesàro test vector \(t_N \in \ell^2(\mathbb{N}, \mathbb{K})\) is \(1/\sqrt{N}\) if \(j < N\), and \(0\) if \(j \ge N\).

lemma cesaroTest_apply (N : ℕ) (j : ℕ) :
    cesaroTest (𝕜 := 𝕜) N j = if j < N then ((Real.sqrt N : ℝ) : 𝕜)⁻¹ else 0

Uses 1 · Used by 3

Statement usesCesàro test vectors

Used byThe Cesàro operator on a test vector, past its support · The Cesàro operator on a test vector, within its support · The Cesàro test vectors are unit vectors

LemmaNorm of the Cesàro test-vector coefficient#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every natural number \(N\), the norm of \((\sqrt{N})^{-1}\), computed in \(\mathbb{K}\), equals the real number \((\sqrt{N})^{-1}\); for \(N = 0\) both sides are \(0\), with the convention \(0^{-1} = 0\).

lemma norm_cesaroTest_sqrt (N : ℕ) :
    ‖((Real.sqrt N : ℝ) : 𝕜)⁻¹‖ = (Real.sqrt N)⁻¹

Used by 2

Used byLower bound for the Cesàro operator on the test vectors · The Cesàro test vectors are unit vectors

LemmaThe Cesàro test vectors are unit vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every natural number \(N \ge 1\), the test vector \(t_N \in \ell^2(\mathbb{N}, \mathbb{K})\), equal to \(1/\sqrt{N}\) at the coordinates \(0, \dots, N - 1\) and to \(0\) elsewhere, has norm \(\|t_N\| = 1\).

lemma norm_cesaroTest (N : ℕ) (hN : 1 ≤ N) : ‖cesaroTest (𝕜 := 𝕜) N‖ = 1

Uses 4 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro test vectors

Proof usesCoordinates of the Cesàro test vectors · Norm of the Cesàro test-vector coefficient

Used byThe Cesàro operator is not compact

LemmaThe Cesàro operator on a test vector, within its support#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\). For \(N \in \mathbb{N}\) let \(t_N\) be the test vector whose first \(N\) coordinates equal \(1/\sqrt{N}\) and whose other coordinates are \(0\). For all \(n, N \in \mathbb{N}\) with \(n < N\), \((C t_N)_n = 1/\sqrt{N}\).

lemma cesaroCLM_test_apply_lt {N : ℕ} {n : ℕ} (hn : n < N) :
    cesaroCLM (𝕜 := 𝕜) (cesaroTest N) n = ((Real.sqrt N : ℝ) : 𝕜)⁻¹

Uses 5 · Used by 2

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · Cesàro test vectors

Proof usesFormula for the Cesàro operator · Coordinates of the Cesàro test vectors

Used byLower bound for the Cesàro operator on the test vectors · The Cesàro images of the test vectors tend to zero coordinatewise

LemmaThe Cesàro operator on a test vector, past its support#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\). For \(N \in \mathbb{N}\) let \(t_N\) be the test vector whose first \(N\) coordinates equal \((\sqrt{N})^{-1}\) and whose other coordinates are \(0\). For all \(N, n \in \mathbb{N}\) with \(N \le n\), \((C t_N)_n = N (\sqrt{N})^{-1}/(n + 1)\), where \((\sqrt{0})^{-1}\) is read as \(0\).

lemma cesaroCLM_test_apply_ge {N : ℕ} {n : ℕ} (hn : N ≤ n) :
    cesaroCLM (𝕜 := 𝕜) (cesaroTest N) n
      = (N : 𝕜) * ((Real.sqrt N : ℝ) : 𝕜)⁻¹ / ((n : 𝕜) + 1)

Uses 5 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · Cesàro test vectors

Proof usesFormula for the Cesàro operator · Coordinates of the Cesàro test vectors

Used byLower bound for the Cesàro operator on the test vectors

LemmaLower bound for the Cesàro operator on the test vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) and let \(t_N\) be the \(N\)-th Cesàro test vector. For every natural number \(N \ge 1\), \(\|C t_N\|^2 \ge 5/4\).

The first \(N\) coordinates of \(C t_N\) contribute \(1\) to \(\|C t_N\|^2\), and the next \(N\) contribute at least \(1/4\).

lemma five_div_four_le_norm_sq_cesaro_test (N : ℕ) (hN : 1 ≤ N) :
    (5 : ℝ) / 4 ≤ ‖cesaroCLM (𝕜 := 𝕜) (cesaroTest N)‖ ^ 2

Uses 7 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · Cesàro test vectors

Proof usesThe Cesàro operator on a test vector, past its support · The Cesàro operator on a test vector, within its support · Norm of the Cesàro test-vector coefficient · Norm of the Cesàro denominator

Used byThe Cesàro operator is not compact

LemmaThe Cesàro images of the test vectors tend to zero coordinatewise#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(C\) be the Cesàro operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), \((Cx)_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\), and for \(N \ge 1\) let \(t_N\) be the vector equal to \(1/\sqrt{N}\) at the coordinates \(0, \dots, N - 1\) and to \(0\) elsewhere. Then for every fixed coordinate \(n\), \((C t_{N+1})_n \to 0\) as \(N \to \infty\).

lemma tendsto_cesaro_test_coord_zero (n : ℕ) :
    Filter.Tendsto (fun N => cesaroCLM (𝕜 := 𝕜) (cesaroTest (N + 1)) n) Filter.atTop
      (𝓝 0)

Uses 4 · Used by 1

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences · Cesàro test vectors

Proof usesThe Cesàro operator on a test vector, within its support

Used byThe Cesàro operator is not compact

TheoremThe Cesàro operator is not compact#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The Cesàro operator \(C\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((Cx)_n = (x_0 + x_1 + \dots + x_n)/(n + 1)\), is not a compact operator.

For \(N \ge 1\) let \(t_N\) be the unit vector equal to \(1/\sqrt{N}\) at the coordinates \(0, \dots, N - 1\) and to \(0\) elsewhere. Then \(\|C t_N\|^2 \ge 5/4\) for every \(N\), while each coordinate of \(C t_N\) tends to \(0\) as \(N \to \infty\), so no subsequence of \((C t_N)\) converges in norm.

theorem not_isCompactOperator_cesaroCLM : ¬ IsCompactOperator (cesaroCLM (𝕜 := 𝕜))

Uses 6

Statement usesThe sequence space \(\ell^2(\mathbb{N}, \mathbb{K})\) · Cesàro operator on square-summable sequences

Proof usesCesàro test vectors · Lower bound for the Cesàro operator on the test vectors · The Cesàro test vectors are unit vectors · The Cesàro images of the test vectors tend to zero coordinatewise

36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.