Diagonal operators

DefinitionBounded diagonal operator on a Hilbert basis#✓fully proved

The bounded diagonal continuous linear map with coefficients a in the Hilbert basis b. Its uniform coefficient bound is part of the constructor.

noncomputable def diagonalOperator (b : HilbertBasis ι 𝕜 H) (a : ι → 𝕜) {C : ℝ}
    (hC : ∀ i, ‖a i‖ ≤ C) : H →L[𝕜] H :=
  b.repr.symm.toLinearIsometry.toContinuousLinearMap.comp
    ((lp.mapCLM 2 (fun i => a i • ContinuousLinearMap.id 𝕜 𝕜) (abs_nonneg C) (fun i => by
        simpa only [norm_smul, ContinuousLinearMap.norm_id, mul_one] using
          (hC i).trans (le_abs_self C))).comp
      b.repr.toLinearIsometry.toContinuousLinearMap)

Used by 8

Used byDiagonal operator on ℓ² · Coordinates of a diagonal operator on ℓ² · Action of a diagonal operator on the basis · Series formula for a diagonal operator · Square of a diagonal operator · Coordinates of a diagonal operator · The square root of the Green's operator is a diagonal operator · The square root of the Green's operator squares to the Green's operator

TheoremCoordinates of a diagonal operator#✓fully proved

Let \((b_i)_{i \in \iota}\) be a Hilbert basis of an inner product space \(H\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)), with inner product \(\langle \cdot, \cdot \rangle\) conjugate-linear in the first argument, let \(a : \iota \to \mathbb{K}\) satisfy \(|a_i| \le C\) for all \(i\), and let \(D\) be the diagonal operator with coefficients \(a\). For every \(x \in H\) and \(i \in \iota\), the \(i\)-th coordinate of \(D x\) in \(\ell^2(\iota)\) with respect to the basis \((b_i)\) is \(a_i \langle b_i, x \rangle\).

theorem repr_diagonalOperator_apply {b : HilbertBasis ι 𝕜 H} {a : ι → 𝕜} {C : ℝ}
    (hC : ∀ i, ‖a i‖ ≤ C) (x : H) (i : ι) :
    b.repr (diagonalOperator b a hC x) i = a i * ⟪b i, x⟫_𝕜

Uses 1 · Used by 2

Statement usesBounded diagonal operator on a Hilbert basis

Used byCoordinates of a diagonal operator on ℓ² · Square of a diagonal operator

TheoremSeries formula for a diagonal operator#✓fully proved

Let \((b_i)_{i \in \iota}\) be a Hilbert basis of an inner product space \(H\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)), with inner product \(\langle \cdot, \cdot \rangle\) conjugate-linear in the first argument, and let \(a : \iota \to \mathbb{K}\) satisfy \(|a_i| \le C\) for all \(i\). The diagonal operator \(D\) with coefficients \(a\) satisfies, for every \(x \in H\),

\[ D x = \sum_{i \in \iota} a_i \langle b_i, x \rangle \, b_i, \]

where the sum is the unconditional sum over \(\iota\) (taken to be \(0\) if the family is not summable).

theorem diagonalOperator_eq_tsum {b : HilbertBasis ι 𝕜 H} {a : ι → 𝕜} {C : ℝ}
    (hC : ∀ i, ‖a i‖ ≤ C) (x : H) :
    diagonalOperator b a hC x = ∑' i, (a i * ⟪b i, x⟫_𝕜) • b i

Uses 1 · Used by 3

Statement usesBounded diagonal operator on a Hilbert basis

Used byAction of a diagonal operator on the basis · The square root of the Green's operator is a diagonal operator · The square root of the Green's operator squares to the Green's operator

TheoremAction of a diagonal operator on the basis#✓fully proved

Let \((b_i)_{i \in \iota}\) be a Hilbert basis of an inner product space \(H\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)), let \(a : \iota \to \mathbb{K}\) satisfy \(|a_i| \le C\) for all \(i\), and let \(D\) be the diagonal operator with coefficients \(a\). Then \(D b_j = a_j b_j\) for every \(j \in \iota\).

theorem diagonalOperator_apply_basis {b : HilbertBasis ι 𝕜 H} {a : ι → 𝕜} {C : ℝ}
    (hC : ∀ i, ‖a i‖ ≤ C) (j : ι) :
    diagonalOperator b a hC (b j) = a j • b j

Uses 2

Statement usesBounded diagonal operator on a Hilbert basis

Proof usesSeries formula for a diagonal operator

TheoremSquare of a diagonal operator#✓fully proved

Let \((b_i)_{i \in \iota}\) be a Hilbert basis of an inner product space \(H\) over \(\mathbb{K}\) (\(\mathbb{R}\) or \(\mathbb{C}\)), and let \(a : \iota \to \mathbb{K}\) satisfy \(|a_i| \le C\) for all \(i\). Let \(D_a\) be the diagonal operator with coefficients \(a\), and let \(D_{a^2}\) be the diagonal operator with coefficients \(a_i^2\), which satisfy \(|a_i^2| \le C^2\). Then \(D_a(D_a x) = D_{a^2} x\) for every \(x \in H\).

theorem diagonalOperator_sq {b : HilbertBasis ι 𝕜 H} {a : ι → 𝕜} {C : ℝ}
    (hC : ∀ i, ‖a i‖ ≤ C) (x : H) :
    diagonalOperator b a hC (diagonalOperator b a hC x) =
      diagonalOperator b (fun i => (a i) ^ 2) (C := C ^ 2) (fun i => by
        rw [norm_pow]
        exact pow_le_pow_left₀ (norm_nonneg _) (hC i) 2) x

Uses 2 · Used by 1

Statement usesBounded diagonal operator on a Hilbert basis

Proof usesCoordinates of a diagonal operator

Used byThe square root of the Green's operator squares to the Green's operator

TheoremScalar multiplication on \(\ell^2\) is pointwise#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(c \in \mathbb{K}\), every \(x \in \ell^2(\iota, \mathbb{K})\) and every \(i \in \iota\), the \(i\)-th coordinate of \(c x\) is \((c x)_i = c \, x_i\).

theorem lp_smul_apply (c : 𝕜) (x : ℓ²(ι, 𝕜)) (i : ι) : (c • x) i = c * x i

Used by 2

Used bySelf-adjoint diagonal operators on \(\ell^2\) · Pointwise bound for diagonal operators

TheoremBounded multipliers preserve \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). If \(a : \iota \to \mathbb{K}\) is bounded, that is, \(|a_i| \le C\) for some real \(C\) and all \(i\), then for every \(x \in \ell^2(\iota, \mathbb{K})\) the sequence \((a_i x_i)_{i \in \iota}\) lies in \(\ell^2(\iota, \mathbb{K})\), that is, the family \((|a_i x_i|^2)_{i \in \iota}\) is summable.

theorem memℓp_diagonal (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C)
    (x : ℓ²(ι, 𝕜)) : Memℓp (fun i => a i * x i) 2

AbbreviationDiagonal operator on ℓ²#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type and let \(a : \iota \to \mathbb{K}\) be a bounded sequence, that is, \(\|a_i\| \le C\) for some real \(C\) and all \(i \in \iota\). The diagonal operator \(D_a\) with coefficients \(a\) is the bounded linear operator on \(\ell^2(\iota, \mathbb{K})\) that sends \(x\) to the sequence \((a_i x_i)_{i \in \iota}\).

It is defined as the Hilbert-basis diagonal operator for the standard Hilbert basis of \(\ell^2(\iota, \mathbb{K})\), using the bound \(\max(C, 0)\) for a chosen bound \(C\), so that empty index types also admit a nonnegative bound.

noncomputable abbrev diagonalCLM (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    ℓ²(ι, 𝕜) →L[𝕜] ℓ²(ι, 𝕜) :=
  MathlibExt.Analysis.InnerProductSpace.HilbertBasisDiagonal.diagonalOperator
    (HilbertBasis.ofRepr (LinearIsometryEquiv.refl 𝕜 (ℓ²(ι, 𝕜)))) a
    (C := max hbdd.choose 0)
    (fun i => (hbdd.choose_spec i).trans (le_max_left _ _))

Uses 1 · Used by 24

Statement usesBounded diagonal operator on a Hilbert basis

Used byAdjoint of a diagonal operator · Coordinates of a diagonal operator on ℓ² · Composition of diagonal operators · The diagonal operator with all coefficients one is the identity · Diagonal operators on standard basis vectors · Difference of diagonal operators · Diagonal operator on ℓ² as a linear map · Compact diagonal operators on ℓ² · Self-adjoint diagonal operators on \(\ell^2\) · Invertibility of a shifted diagonal operator · Operator norm of a diagonal operator · Operator norm bound for diagonal operators · Points off the closure of the coefficients are not in the spectrum · Every coefficient of a diagonal operator lies in its spectrum · Shifting a diagonal operator by a scalar · Spectrum of a diagonal operator · Adjoint of the weighted shift · Compactness criterion for weighted shifts · Norm of the weighted backward shift · Operator norm of a weighted shift · Uniform weight bounds bound the weighted shift · Weighted backward shift · Weighted forward shift operator · Weighted shift of a difference of weights

TheoremCoordinates of a diagonal operator on ℓ²#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type, let \(a : \iota \to \mathbb{K}\) be a bounded sequence and let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(a\). For every \(x \in \ell^2(\iota, \mathbb{K})\) and every \(i \in \iota\), the \(i\)-th coordinate of \(D_a x\) is \(a_i x_i\).

theorem diagonalCLM_apply (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C)
    (x : ℓ²(ι, 𝕜)) (i : ι) :
    diagonalCLM a hbdd x i = a i * x i

Uses 3 · Used by 11

Statement usesDiagonal operator on ℓ²

Proof usesBounded diagonal operator on a Hilbert basis · Coordinates of a diagonal operator

Used byAdjoint of a diagonal operator · Composition of diagonal operators · The diagonal operator with all coefficients one is the identity · Diagonal operators on standard basis vectors · Difference of diagonal operators · Coordinates of the diagonal linear map on ℓ² · Compact diagonal operators on ℓ² · Every coefficient of a diagonal operator lies in its spectrum · Shifting a diagonal operator by a scalar · Coordinates of the weighted backward shift · Coordinates of the weighted forward shift

AbbreviationDiagonal operator on ℓ² as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type and let \(a : \iota \to \mathbb{K}\) be a bounded sequence. This is the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(a\), regarded as a \(\mathbb{K}\)-linear map \(\ell^2(\iota, \mathbb{K}) \to \ell^2(\iota, \mathbb{K})\) by forgetting its continuity.

noncomputable abbrev diagonalLinMap (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    ℓ²(ι, 𝕜) →ₗ[𝕜] ℓ²(ι, 𝕜) :=
  (diagonalCLM a hbdd).toLinearMap

Uses 1 · Used by 2

Statement usesDiagonal operator on ℓ²

Used byCoordinates of the diagonal linear map on ℓ² · Pointwise bound for diagonal operators

TheoremCoordinates of the diagonal linear map on ℓ²#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type and let \(a : \iota \to \mathbb{K}\) be a bounded sequence. For every \(x \in \ell^2(\iota, \mathbb{K})\) and every \(i \in \iota\), the diagonal operator with coefficients \(a\), regarded as a linear map, sends \(x\) to a sequence whose \(i\)-th coordinate is \(a_i x_i\).

theorem diagonalLinMap_apply (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C)
    (x : ℓ²(ι, 𝕜)) (i : ι) :
    diagonalLinMap a hbdd x i = a i * x i

Uses 2 · Used by 1

Statement usesDiagonal operator on ℓ² as a linear map

Proof usesCoordinates of a diagonal operator on ℓ²

Used byPointwise bound for diagonal operators

TheoremPointwise bound for diagonal operators#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be bounded, and let \(D_a\) be the diagonal operator \(x \mapsto (a_i x_i)_{i \in \iota}\) on \(\ell^2(\iota, \mathbb{K})\), viewed as a linear map. If \(C \ge 0\) and \(|a_i| \le C\) for every \(i \in \iota\), then \(\|D_a x\| \le C \|x\|\) for every \(x \in \ell^2(\iota, \mathbb{K})\).

theorem norm_diagonalLinMap_le (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C)
    {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ i, ‖a i‖ ≤ C) (x : ℓ²(ι, 𝕜)) :
    ‖diagonalLinMap a hbdd x‖ ≤ C * ‖x‖

Uses 3 · Used by 1

Statement usesDiagonal operator on ℓ² as a linear map

Proof usesCoordinates of the diagonal linear map on ℓ² · Scalar multiplication on \(\ell^2\) is pointwise

Used byOperator norm bound for diagonal operators

TheoremDiagonal operators on standard basis vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type, let \(a : \iota \to \mathbb{K}\) be a bounded sequence and let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(a\). For \(i \in \iota\) let \(e_i \in \ell^2(\iota, \mathbb{K})\) be the sequence equal to \(1\) at \(i\) and \(0\) elsewhere. Then for every \(i \in \iota\) and every \(c \in \mathbb{K}\) we have \(D_a(c\,e_i) = a_i \, (c\,e_i)\).

theorem diagonalCLM_single [DecidableEq ι] (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C)
    (i : ι) (c : 𝕜) :
    diagonalCLM a hbdd (lp.single 2 i c) = a i • lp.single 2 i c

Uses 2 · Used by 3

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ²

Used byCompact diagonal operators on ℓ² · Self-adjoint diagonal operators on \(\ell^2\) · Operator norm of a diagonal operator

TheoremThe diagonal operator with all coefficients one is the identity#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\iota\) be a type. The diagonal operator on \(\ell^2(\iota, \mathbb{K})\) whose coefficients all equal \(1\) is the identity operator.

theorem diagonalCLM_one : diagonalCLM (fun _ : ι => (1 : 𝕜)) ⟨1, fun _ => by simp⟩ = 1

Uses 2 · Used by 1

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ²

Used byInvertibility of a shifted diagonal operator

TheoremComposition of diagonal operators#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type, and for a bounded sequence \(c : \iota \to \mathbb{K}\) let \(D_c\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(c\). For bounded sequences \(a, b : \iota \to \mathbb{K}\), we have \(D_b \circ D_a = D_{ba}\), where \(ba\) is the pointwise product \(i \mapsto b_i a_i\).

theorem diagonalCLM_comp (a b : ι → 𝕜) (ha : ∃ C, ∀ i, ‖a i‖ ≤ C)
    (hb : ∃ C, ∀ i, ‖b i‖ ≤ C) :
    diagonalCLM b hb ∘L diagonalCLM a ha =
      diagonalCLM (fun i => b i * a i) (by
        obtain ⟨Ca, _hCa0, hCa⟩ := exists_nonneg_bound ha
        obtain ⟨Cb, hCb0, hCb⟩ := exists_nonneg_bound hb
        exact ⟨Cb * Ca, fun i => by
          rw [norm_mul]
          exact mul_le_mul (hCb i) (hCa i) (norm_nonneg _) hCb0⟩)

Uses 2 · Used by 1

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ²

Used byInvertibility of a shifted diagonal operator

TheoremDifference of diagonal operators#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type, and for a bounded sequence \(c : \iota \to \mathbb{K}\) let \(D_c\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(c\). For bounded sequences \(a, b : \iota \to \mathbb{K}\), we have \(D_a - D_b = D_{a - b}\), where \(a - b\) is the sequence \(i \mapsto a_i - b_i\).

theorem diagonalCLM_sub (a b : ι → 𝕜) (ha : ∃ C, ∀ i, ‖a i‖ ≤ C)
    (hb : ∃ C, ∀ i, ‖b i‖ ≤ C) :
    diagonalCLM a ha - diagonalCLM b hb =
      diagonalCLM (fun i => a i - b i) (by
        obtain ⟨Ca, _hCa0, hCa⟩ := exists_nonneg_bound ha
        obtain ⟨Cb, _hCb0, hCb⟩ := exists_nonneg_bound hb
        exact ⟨Ca + Cb, fun i => by
          calc ‖a i - b i‖ ≤ ‖a i‖ + ‖b i‖ := norm_sub_le _ _
            _ ≤ Ca + Cb := add_le_add (hCa i) (hCb i)⟩)

Uses 2 · Used by 2

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ²

Used byCompact diagonal operators on ℓ² · Weighted shift of a difference of weights

TheoremOperator norm bound for diagonal operators#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be bounded, and let \(D_a\) be the diagonal operator \(x \mapsto (a_i x_i)_{i \in \iota}\) on \(\ell^2(\iota, \mathbb{K})\). If \(C \ge 0\) and \(|a_i| \le C\) for every \(i \in \iota\), then the operator norm satisfies \(\|D_a\| \le C\).

theorem norm_diagonalCLM_le (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C)
    {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ i, ‖a i‖ ≤ C) :
    ‖diagonalCLM a hbdd‖ ≤ C

Uses 2 · Used by 3

Statement usesDiagonal operator on ℓ²

Proof usesPointwise bound for diagonal operators

Used byCompact diagonal operators on ℓ² · Operator norm of a diagonal operator · Uniform weight bounds bound the weighted shift

TheoremOperator norm of a diagonal operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be bounded, and let \(D_a\) be the diagonal operator \(x \mapsto (a_i x_i)_{i \in \iota}\) on \(\ell^2(\iota, \mathbb{K})\). Then the operator norm of \(D_a\) is \(\|D_a\| = \sup_{i \in \iota} |a_i|\), where the supremum is taken to be \(0\) when \(\iota\) is empty.

theorem norm_diagonalCLM (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    ‖diagonalCLM a hbdd‖ = ⨆ i, ‖a i‖

Uses 3 · Used by 2

Statement usesDiagonal operator on ℓ²

Proof usesDiagonal operators on standard basis vectors · Operator norm bound for diagonal operators

Used byNorm of the weighted backward shift · Operator norm of a weighted shift

TheoremAdjoint of a diagonal operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type and let \(a : \iota \to \mathbb{K}\) be a bounded sequence. The adjoint of the diagonal operator \(D_a\) on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(a\) is the diagonal operator with the conjugate coefficients \(i \mapsto \overline{a_i}\).

theorem adjoint_diagonalCLM (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    (diagonalCLM a hbdd)† =
      diagonalCLM (fun i => star (a i)) (by
        obtain ⟨C, hC⟩ := hbdd
        exact ⟨C, fun i => by rw [norm_star]; exact hC i⟩)

Uses 2 · Used by 2

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ²

Used bySelf-adjoint diagonal operators on \(\ell^2\) · Adjoint of the weighted shift

TheoremSelf-adjoint diagonal operators on \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be bounded, and let \(D_a\) be the diagonal operator \(x \mapsto (a_i x_i)_{i \in \iota}\) on \(\ell^2(\iota, \mathbb{K})\). Then \(D_a\) is self-adjoint if and only if \(\overline{a_i} = a_i\), that is, \(a_i\) is real, for every \(i \in \iota\).

theorem isSelfAdjoint_diagonalCLM_iff (a : ι → 𝕜) (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    IsSelfAdjoint (diagonalCLM a hbdd) ↔ ∀ i, star (a i) = a i

Uses 4

Statement usesDiagonal operator on ℓ²

Proof usesAdjoint of a diagonal operator · Diagonal operators on standard basis vectors · Scalar multiplication on \(\ell^2\) is pointwise

TheoremRank-one term of the finite-support decomposition on \(\ell^2\)#✓fully proved

A rank-one term of the finite-support decomposition, evaluated pointwise.

theorem singleCLM_comp_evalCLM_apply [DecidableEq ι] (b : ι → 𝕜) (i : ι) (x : ℓ²(ι, 𝕜)) :
    (lp.singleContinuousLinearMap 𝕜 (fun _ : ι => 𝕜) 2 i ∘L
        ((b i) • lp.evalCLM 𝕜 (fun _ : ι => 𝕜) 2 i)) x
      = lp.single 2 i (b i * x i)

TheoremCompact diagonal operators on ℓ²#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\iota\) be a type and let \(a : \iota \to \mathbb{K}\) be a bounded sequence. The diagonal operator on \(\ell^2(\iota, \mathbb{K})\) with coefficients \(a\) is compact if and only if \(a\) tends to \(0\) along the cofinite filter on \(\iota\), that is, for every \(\varepsilon > 0\) only finitely many \(i \in \iota\) satisfy \(\|a_i\| \ge \varepsilon\).

theorem isCompactOperator_diagonalCLM_iff {a : ι → 𝕜}
    (hbdd : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    IsCompactOperator (diagonalCLM a hbdd) ↔ Tendsto a cofinite (𝓝 0)

Uses 5 · Used by 1

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ² · Diagonal operators on standard basis vectors · Difference of diagonal operators · Operator norm bound for diagonal operators

Used byCompactness criterion for weighted shifts

TheoremShifting a diagonal operator by a scalar#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be a bounded family of coefficients, let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) given by \((D_a x)_i = a_i x_i\), and let \(I\) be the identity operator. For every \(\mu \in \mathbb{K}\), \(\mu I - D_a = D_{\mu - a}\), the diagonal operator with coefficients \(\mu - a_i\).

theorem smul_one_sub_diagonalCLM_eq (μ : 𝕜) (a : ι → 𝕜)
    (ha : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    μ • (1 : ℓ²(ι, 𝕜) →L[𝕜] ℓ²(ι, 𝕜)) - diagonalCLM a ha =
      diagonalCLM (fun i => μ - a i) (by
        obtain ⟨C, hC⟩ := ha
        exact ⟨‖μ‖ + C, fun i => (norm_sub_le _ _).trans (add_le_add le_rfl (hC i))⟩)

Uses 2 · Used by 2

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ²

Used byInvertibility of a shifted diagonal operator · Every coefficient of a diagonal operator lies in its spectrum

TheoremInvertibility of a shifted diagonal operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be a bounded family of coefficients, let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) given by \((D_a x)_i = a_i x_i\), and let \(I\) be the identity operator. If \(\mu \in \mathbb{K}\) does not lie in the closure of \(\{a_i : i \in \iota\}\), then \(\mu I - D_a\) is invertible in the algebra of bounded operators on \(\ell^2(\iota, \mathbb{K})\).

theorem isUnit_smul_one_sub_diagonalCLM_of_not_mem_closure_range {a : ι → 𝕜}
    (ha : ∃ C, ∀ i, ‖a i‖ ≤ C) {μ : 𝕜} (hμ : μ ∉ closure (Set.range a)) :
    IsUnit (μ • (1 : ℓ²(ι, 𝕜) →L[𝕜] ℓ²(ι, 𝕜)) - diagonalCLM a ha)

Uses 4 · Used by 1

Statement usesDiagonal operator on ℓ²

Proof usesComposition of diagonal operators · The diagonal operator with all coefficients one is the identity · Shifting a diagonal operator by a scalar

Used byPoints off the closure of the coefficients are not in the spectrum

TheoremPoints off the closure of the coefficients are not in the spectrum#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be a bounded family of coefficients, and let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) given by \((D_a x)_i = a_i x_i\). If \(\mu \in \mathbb{K}\) does not lie in the closure of \(\{a_i : i \in \iota\}\), then \(\mu\) is not in the spectrum of \(D_a\) over \(\mathbb{K}\), that is, \(\mu I - D_a\) is invertible as a bounded operator, where \(I\) is the identity operator.

theorem not_mem_spectrum_of_not_mem_closure_range {a : ι → 𝕜}
    (ha : ∃ C, ∀ i, ‖a i‖ ≤ C) {μ : 𝕜} (hμ : μ ∉ closure (Set.range a)) :
    μ ∉ spectrum 𝕜 (diagonalCLM a ha)

Uses 2 · Used by 1

Statement usesDiagonal operator on ℓ²

Proof usesInvertibility of a shifted diagonal operator

Used bySpectrum of a diagonal operator

TheoremEvery coefficient of a diagonal operator lies in its spectrum#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be a bounded family of coefficients, and let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) given by \((D_a x)_i = a_i x_i\). Then every \(a_j\) with \(j \in \iota\) lies in the spectrum of \(D_a\) over \(\mathbb{K}\), the set of \(\mu \in \mathbb{K}\) for which \(\mu I - D_a\) is not invertible as a bounded operator, where \(I\) is the identity operator.

For each \(j \in \iota\), the \(j\)-th coordinate vector lies in the kernel of \(a_j I - D_a\).

theorem range_subset_spectrum {a : ι → 𝕜} (ha : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    Set.range a ⊆ spectrum 𝕜 (diagonalCLM a ha)

Uses 3 · Used by 1

Statement usesDiagonal operator on ℓ²

Proof usesCoordinates of a diagonal operator on ℓ² · Shifting a diagonal operator by a scalar

Used bySpectrum of a diagonal operator

TheoremSpectrum of a diagonal operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(a : \iota \to \mathbb{K}\) be a bounded family of coefficients, and let \(D_a\) be the diagonal operator on \(\ell^2(\iota, \mathbb{K})\) given by \((D_a x)_i = a_i x_i\). The spectrum of \(D_a\) over \(\mathbb{K}\), the set of \(\mu \in \mathbb{K}\) for which \(\mu I - D_a\) is not invertible as a bounded operator (\(I\) the identity operator), is the closure of \(\{a_i : i \in \iota\}\).

theorem spectrum_diagonalCLM (a : ι → 𝕜) (ha : ∃ C, ∀ i, ‖a i‖ ≤ C) :
    spectrum 𝕜 (diagonalCLM a ha) = closure (Set.range a)

Uses 3

Statement usesDiagonal operator on ℓ²

Proof usesPoints off the closure of the coefficients are not in the spectrum · Every coefficient of a diagonal operator lies in its spectrum

27 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.