Weighted shifts

DefinitionWeighted forward shift of a sequence#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For a weight sequence \(w : \mathbb{N} \to \mathbb{K}\) and a sequence \(x : \mathbb{N} \to \mathbb{K}\), the weighted forward shift of \(x\) is the sequence \(y\) with \(y_0 = 0\) and \(y_{n+1} = w_n x_n\) for every \(n \in \mathbb{N}\).

def weightedShiftFun (w : ℕ → 𝕜) (x : ℕ → 𝕜) : ℕ → 𝕜
  | 0 => 0
  | n + 1 => w n * x n

Used by 10

Used byThe weighted backward shift after the forward shift is diagonal · Weighted forward shifts preserve square-summability · Forward-after-backward weighted shift is diagonal · Coordinates of the weighted forward shift · The weighted forward shift agrees with the shift of sequences · The weighted forward shift with unit weights is the unilateral shift · The weighted forward shift on basis vectors · Weighted forward shift at a successor index · Weighted forward shift at index zero · Coordinates of the weighted forward shift linear map

DefinitionWeighted backward shift of a sequence#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For weights \(w : \mathbb{N} \to \mathbb{K}\) and a sequence \(x : \mathbb{N} \to \mathbb{K}\), the weighted backward shift of \(x\) is the sequence whose term at index \(i\) is \(\overline{w_i}\, x_{i+1}\).

The weights are conjugated so that the resulting operator on \(\ell^2\) is the adjoint of the weighted forward shift.

def weightedBackwardFun (w : ℕ → 𝕜) (x : ℕ → 𝕜) (i : ℕ) : 𝕜 :=
  conj (w i) * x (i + 1)

Used by 7

Used byThe weighted backward shift after the forward shift is diagonal · Weighted backward shifts preserve square-summability · Coordinates of the weighted backward shift · Unit weights give the plain backward shift · Weighted backward shift on basis vectors · Coordinates of the weighted backward-shift function · The weighted backward shift linear map agrees with the shift of sequences

TheoremWeighted forward shift at index zero#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For all weights \(w : \mathbb{N} \to \mathbb{K}\) and every sequence \(x : \mathbb{N} \to \mathbb{K}\), the term at index \(0\) of the weighted forward shift of \(x\) is \(0\).

@[simp] theorem weightedShiftFun_zero (w : ℕ → 𝕜) (x : ℕ → 𝕜) :
    weightedShiftFun w x 0 = 0

Uses 1

Statement usesWeighted forward shift of a sequence

TheoremWeighted forward shift at a successor index#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For weights \(w : \mathbb{N} \to \mathbb{K}\), a sequence \(x : \mathbb{N} \to \mathbb{K}\) and \(n \in \mathbb{N}\), the term at index \(n + 1\) of the weighted forward shift of \(x\) is \(w_n x_n\).

@[simp] theorem weightedShiftFun_succ (w : ℕ → 𝕜) (x : ℕ → 𝕜) (n : ℕ) :
    weightedShiftFun w x (n + 1) = w n * x n

Uses 1 · Used by 1

Statement usesWeighted forward shift of a sequence

Used byThe weighted backward shift after the forward shift is diagonal

TheoremCoordinates of the weighted backward-shift function#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For weights \(w : \mathbb{N} \to \mathbb{K}\), a sequence \(x : \mathbb{N} \to \mathbb{K}\) and \(i \in \mathbb{N}\), the weighted backward-shift function of \(w\) applied to \(x\) takes the value \(\overline{w_i}\, x_{i+1}\) at \(i\).

@[simp] theorem weightedBackwardFun_apply (w : ℕ → 𝕜) (x : ℕ → 𝕜) (i : ℕ) :
    weightedBackwardFun w x i = conj (w i) * x (i + 1)

Uses 1 · Used by 1

Statement usesWeighted backward shift of a sequence

Used byThe weighted backward shift after the forward shift is diagonal

DefinitionWeighted forward shift operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with \(\sup_n |w_n| < \infty\). The weighted forward shift with weights \(w\) is the bounded operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) obtained by first applying the diagonal operator \(x \mapsto (w_n x_n)_{n}\) and then the unilateral forward shift \((x_0, x_1, \dots) \mapsto (0, x_0, x_1, \dots)\).

noncomputable def weightedShiftCLM (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  LpShiftOperator.shiftCLM ∘L LpDiagonalOperator.diagonalCLM w (by
    exact exists_uniform_bound hw)

Uses 2 · Used by 21

Statement usesDiagonal operator on ℓ² · The unilateral shift operator

Used byAdjoint of the weighted shift · The weighted backward shift after the forward shift is diagonal · The weighted backward shift is a left inverse for unimodular weights · Weighted shifts with nonzero weights are injective · Compactness criterion for weighted shifts · Weighted shifts with eventually vanishing weights are compact · Isometric weighted shifts · Weighted forward shifts preserve square-summability · Operator norm of a weighted shift · Weighted shifts with unimodular weights preserve norms · Uniform weight bounds bound the weighted shift · Norm bound for weighted shift images · A vanishing weight makes the weighted shift non-injective · Forward-after-backward weighted shift is diagonal · Weighted shifts with truncated weights converge in operator norm · Coordinates of the weighted forward shift · The weighted forward shift agrees with the shift of sequences · The weighted forward shift with unit weights is the unilateral shift · The weighted forward shift on basis vectors · Weighted shift of a difference of weights · Weighted forward shift as a linear map

DefinitionWeighted backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli. The weighted backward shift \(B_w\) is the bounded operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) obtained by applying the backward shift \((x_0, x_1, \dots) \mapsto (x_1, x_2, \dots)\) and then multiplying coordinate \(i\) by \(\overline{w_i}\); thus \((B_w x)_i = \overline{w_i}\, x_{i+1}\).

noncomputable def weightedBackwardCLM (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  LpDiagonalOperator.diagonalCLM (fun n => star (w n)) (by
    simpa only [norm_star] using exists_uniform_bound hw) ∘L
    LpShiftOperator.backwardCLM

Uses 2 · Used by 11

Statement usesDiagonal operator on ℓ² · Backward shift

Used byAdjoint of the weighted shift · The weighted backward shift after the forward shift is diagonal · The weighted backward shift is a left inverse for unimodular weights · Norm of the weighted backward shift · Norm bound for the weighted backward shift · Weighted shifts with unimodular weights preserve norms · Forward-after-backward weighted shift is diagonal · Coordinates of the weighted backward shift · Unit weights give the plain backward shift · Weighted backward shift on basis vectors · Weighted backward shift as a linear map

AbbreviationWeighted forward shift as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(w : \mathbb{N} \to \mathbb{K}\) be a weight sequence whose norms \(\|w_n\|\) are bounded above. The weighted forward shift linear map is the \(\mathbb{K}\)-linear map \(\ell^2(\mathbb{N}, \mathbb{K}) \to \ell^2(\mathbb{N}, \mathbb{K})\) underlying the bounded weighted forward shift operator (multiplication by \(w\) followed by the forward shift), which sends \(x\) to the sequence \(y\) with \(y_0 = 0\) and \(y_{n+1} = w_n x_n\).

noncomputable abbrev weightedShiftLinMap (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) :=
  (weightedShiftCLM w hw).toLinearMap

Uses 1 · Used by 2

Statement usesWeighted forward shift operator

Used byNorm bound for weighted shift images · Coordinates of the weighted forward shift linear map

AbbreviationWeighted backward shift as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with \(\sup_n |w_n| < \infty\). The weighted backward shift linear map with weights \(w\) is the bounded weighted backward shift operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) with weights \(w\), regarded as a \(\mathbb{K}\)-linear map from \(\ell^2(\mathbb{N}, \mathbb{K})\) to itself (forgetting continuity).

noncomputable abbrev weightedBackwardLinMap (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) :=
  (weightedBackwardCLM w hw).toLinearMap

Uses 1 · Used by 3

Statement usesWeighted backward shift

Used byWeighted backward shifts preserve square-summability · Norm bound for the weighted backward shift · The weighted backward shift linear map agrees with the shift of sequences

TheoremCoordinates of the weighted forward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be weights with \(\sup_n |w_n| < \infty\), and let \(S_w\) be the weighted forward shift operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) with weights \(w\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the coordinate \((S_w x)_i\) is the term at index \(i\) of the weighted forward shift of the sequence \(x\); that is, \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\).

theorem weightedShiftCLM_apply (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    weightedShiftCLM w hw x i = weightedShiftFun w (x : ℕ → 𝕜) i

Uses 3 · Used by 6

Statement usesWeighted forward shift operator · Weighted forward shift of a sequence

Proof usesCoordinates of a diagonal operator on ℓ²

Used byThe weighted backward shift after the forward shift is diagonal · Weighted shifts with nonzero weights are injective · Forward-after-backward weighted shift is diagonal · The weighted forward shift agrees with the shift of sequences · The weighted forward shift with unit weights is the unilateral shift · The weighted forward shift on basis vectors

TheoremCoordinates of the weighted backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli, and let \(B_w\) be the weighted backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the \(i\)-th coordinate of \(B_w x\) is the weighted backward-shift function of \(w\) applied to \(x\) at \(i\), that is, \((B_w x)_i = \overline{w_i}\, x_{i+1}\).

theorem weightedBackwardCLM_apply (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    weightedBackwardCLM w hw x i = weightedBackwardFun w (x : ℕ → 𝕜) i

Uses 4 · Used by 5

Statement usesWeighted backward shift · Weighted backward shift of a sequence

Proof usesCoordinates of a diagonal operator on ℓ² · Backward shift

Used byThe weighted backward shift after the forward shift is diagonal · Forward-after-backward weighted shift is diagonal · Unit weights give the plain backward shift · Weighted backward shift on basis vectors · The weighted backward shift linear map agrees with the shift of sequences

TheoremThe weighted forward shift agrees with the shift of sequences#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with \(\sup_n |w_n| < \infty\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the image of \(x\) under the weighted forward shift operator with weights \(w\) is as a sequence the weighted forward shift of \(x\): its term at index \(0\) is \(0\) and its term at index \(n + 1\) is \(w_n x_n\) for every \(n\).

theorem weightedShiftCLM_apply_coe (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) :
    ⇑(weightedShiftCLM w hw x) = weightedShiftFun w (x : ℕ → 𝕜)

Uses 3 · Used by 2

Statement usesWeighted forward shift operator · Weighted forward shift of a sequence

Proof usesCoordinates of the weighted forward shift

Used byWeighted forward shifts preserve square-summability · Coordinates of the weighted forward shift linear map

TheoremCoordinates of the weighted forward shift linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(w : \mathbb{N} \to \mathbb{K}\) be a weight sequence whose norms \(\|w_n\|\) are bounded above. For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the image of \(x\) under the weighted forward shift linear map, viewed as a sequence, is the weighted forward shift of \(x\): its coordinate \(0\) is \(0\) and its coordinate \(n + 1\) is \(w_n x_n\) for every \(n\).

theorem weightedShiftLinMap_apply_coe (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) :
    ⇑(weightedShiftLinMap w hw x) = weightedShiftFun w (x : ℕ → 𝕜)

Uses 3

Statement usesWeighted forward shift of a sequence · Weighted forward shift as a linear map

Proof usesThe weighted forward shift agrees with the shift of sequences

TheoremThe weighted backward shift linear map agrees with the shift of sequences#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with \(\sup_n |w_n| < \infty\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the image of \(x\) under the weighted backward shift with weights \(w\), regarded as a linear map on \(\ell^2(\mathbb{N}, \mathbb{K})\), is as a sequence the weighted backward shift of \(x\): its term at index \(i\) is \(\overline{w_i}\, x_{i+1}\) for every \(i\).

theorem weightedBackwardLinMap_apply_coe (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) :
    ⇑(weightedBackwardLinMap w hw x) = weightedBackwardFun w (x : ℕ → 𝕜)

Uses 3 · Used by 1

Statement usesWeighted backward shift of a sequence · Weighted backward shift as a linear map

Proof usesCoordinates of the weighted backward shift

Used byWeighted backward shifts preserve square-summability

TheoremWeighted forward shifts preserve square-summability#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the sequence \(y\) with \(y_0 = 0\) and \(y_{n+1} = w_n x_n\) is square-summable.

theorem memℓp_weightedShiftFun {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) {x : ℓ²(ℕ, 𝕜)} :
    Memℓp (weightedShiftFun w (x : ℕ → 𝕜)) 2

Uses 3

Statement usesWeighted forward shift of a sequence

Proof usesWeighted forward shift operator · The weighted forward shift agrees with the shift of sequences

TheoremWeighted backward shifts preserve square-summability#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the sequence \((\overline{w_i}\, x_{i+1})_{i \in \mathbb{N}}\) is square-summable.

theorem memℓp_weightedBackwardFun {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) {x : ℓ²(ℕ, 𝕜)} :
    Memℓp (weightedBackwardFun w (x : ℕ → 𝕜)) 2

Uses 3

Statement usesWeighted backward shift of a sequence

Proof usesWeighted backward shift as a linear map · The weighted backward shift linear map agrees with the shift of sequences

TheoremThe weighted forward shift on basis vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be weights with \(\sup_n |w_n| < \infty\), and let \((e_n)_{n \in \mathbb{N}}\) be the standard basis vectors of \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(n\), the weighted forward shift operator with weights \(w\) sends \(e_n\) to \(w_n e_{n+1}\).

theorem weightedShiftCLM_single (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (n : ℕ) :
    weightedShiftCLM w hw (lp.single 2 n (1 : 𝕜)) = lp.single 2 (n + 1) (w n)

Uses 3 · Used by 3

Statement usesWeighted forward shift operator

Proof usesCoordinates of the weighted forward shift · Weighted forward shift of a sequence

Used byIsometric weighted shifts · Operator norm of a weighted shift · A vanishing weight makes the weighted shift non-injective

TheoremWeighted backward shift on basis vectors#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli, and write \(e_n\) for the \(n\)-th standard basis vector of \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(n\), the weighted backward shift \(B_w\) satisfies \(B_w e_{n+1} = \overline{w_n}\, e_n\).

theorem weightedBackwardCLM_single_succ (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (n : ℕ) :
    weightedBackwardCLM w hw (lp.single 2 (n + 1) (1 : 𝕜)) =
      lp.single 2 n (conj (w n))

Uses 3 · Used by 1

Statement usesWeighted backward shift

Proof usesCoordinates of the weighted backward shift · Weighted backward shift of a sequence

Used byNorm of the weighted backward shift

TheoremUniform weight bounds bound the weighted shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli, and let \(S_w\) be the weighted forward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\). If \(C\) is a real number with \(|w_n| \le C\) for every \(n\), then the operator norm of \(S_w\) is at most \(C\).

theorem norm_weightedShiftCLM_le_of_forall_le {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) {C : ℝ} (hC : ∀ n, ‖w n‖ ≤ C) :
    ‖weightedShiftCLM w hw‖ ≤ C

Uses 5 · Used by 1

Statement usesWeighted forward shift operator

Proof usesDiagonal operator on ℓ² · Operator norm bound for diagonal operators · The unilateral shift has operator norm one · The unilateral shift operator

Used byWeighted shifts with truncated weights converge in operator norm

TheoremOperator norm of a weighted shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli. The weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\) has operator norm \(\|S_w\| = \sup_n |w_n|\).

theorem norm_weightedShiftCLM {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) :
    ‖weightedShiftCLM w hw‖ = ⨆ n, ‖w n‖

Uses 6 · Used by 2

Statement usesWeighted forward shift operator

Proof usesDiagonal operator on ℓ² · Operator norm of a diagonal operator · The unilateral shift has operator norm one · The unilateral shift operator · The weighted forward shift on basis vectors

Used byWeighted shifts with unimodular weights preserve norms · Norm bound for weighted shift images

TheoremAdjoint of the weighted shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\). The adjoint of the weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\), is the weighted backward shift \(B_w\), given by \((B_w x)_i = \overline{w_i}\, x_{i+1}\); that is, \(S_w^* = B_w\).

theorem adjoint_weightedShiftCLM {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) :
    (weightedShiftCLM w hw)† = weightedBackwardCLM w hw

Uses 7

Statement usesWeighted backward shift · Weighted forward shift operator

Proof usesAdjoint of a diagonal operator · Diagonal operator on ℓ² · Adjoint of the unilateral shift · Backward shift · The unilateral shift operator

TheoremNorm of the weighted backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\). The weighted backward shift \(B_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((B_w x)_i = \overline{w_i}\, x_{i+1}\), has operator norm \(\|B_w\| = \sup_n |w_n|\).

theorem norm_weightedBackwardCLM {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) :
    ‖weightedBackwardCLM w hw‖ = ⨆ n, ‖w n‖

Uses 6 · Used by 2

Statement usesWeighted backward shift

Proof usesDiagonal operator on ℓ² · Operator norm of a diagonal operator · Backward shift · The backward shift has operator norm at most one · Weighted backward shift on basis vectors

Used byNorm bound for the weighted backward shift · Weighted shifts with unimodular weights preserve norms

TheoremNorm bound for weighted shift images#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli. For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the weighted forward shift \(S_w\), viewed as a linear map, satisfies \(\|S_w x\| \le \left(\sup_n |w_n|\right) \|x\|\).

theorem norm_weightedShiftLinMap_apply_le {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) :
    ‖weightedShiftLinMap w hw x‖ ≤ (⨆ n, ‖w n‖) * ‖x‖

Uses 3

Statement usesWeighted forward shift as a linear map

Proof usesOperator norm of a weighted shift · Weighted forward shift operator

TheoremNorm bound for the weighted backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\), and let \(B_w\) be the weighted backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((B_w x)_i = \overline{w_i}\, x_{i+1}\). Then \(\|B_w x\| \le (\sup_n |w_n|)\, \|x\|\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem norm_weightedBackwardLinMap_apply_le {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) :
    ‖weightedBackwardLinMap w hw x‖ ≤ (⨆ n, ‖w n‖) * ‖x‖

Uses 3

Statement usesWeighted backward shift as a linear map

Proof usesNorm of the weighted backward shift · Weighted backward shift

TheoremThe weighted backward shift after the forward shift is diagonal#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\), and on \(\ell^2(\mathbb{N}, \mathbb{K})\) let \(S_w\) be the weighted forward shift, \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\), and \(B_w\) the weighted backward shift, \((B_w x)_i = \overline{w_i}\, x_{i+1}\). Then \((B_w S_w x)_i = |w_i|^2 x_i\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\).

theorem backward_comp_shift_apply (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (weightedBackwardCLM w hw ∘L weightedShiftCLM w hw) x i =
      (‖w i‖ ^ 2 : 𝕜) * (x : ℕ → 𝕜) i

Uses 8 · Used by 1

Statement usesWeighted backward shift · Weighted forward shift operator

Proof usesCoordinates of the weighted backward shift · Weighted backward shift of a sequence · Coordinates of the weighted backward-shift function · Coordinates of the weighted forward shift · Weighted forward shift of a sequence · Weighted forward shift at a successor index

Used byThe weighted backward shift is a left inverse for unimodular weights

TheoremForward-after-backward weighted shift is diagonal#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli, and let \(S_w\) and \(B_w\) be the weighted forward and backward shifts on \(\ell^2(\mathbb{N}, \mathbb{K})\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the composite \(S_w B_w\) satisfies \((S_w B_w x)_0 = 0\) and \((S_w B_w x)_i = |w_{i-1}|^2 x_i\) for every \(i \ge 1\).

theorem shift_comp_backward_apply (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (weightedShiftCLM w hw ∘L weightedBackwardCLM w hw) x i =
      if i = 0 then 0 else (‖w (i - 1)‖ ^ 2 : 𝕜) * (x : ℕ → 𝕜) i

Uses 5

Statement usesWeighted backward shift · Weighted forward shift operator

Proof usesCoordinates of the weighted backward shift · Coordinates of the weighted forward shift · Weighted forward shift of a sequence

TheoremThe weighted backward shift is a left inverse for unimodular weights#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a sequence in \(\mathbb{K}\) with \(|w_n| = 1\) for every \(n\). On \(\ell^2(\mathbb{N}, \mathbb{K})\) let \(S_w\) be the weighted forward shift, \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\), and \(B_w\) the weighted backward shift, \((B_w x)_i = \overline{w_i}\, x_{i+1}\). Then \(B_w S_w\) is the identity operator.

theorem backward_comp_shift_eq_one (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (h : ∀ n, ‖w n‖ = 1) :
    weightedBackwardCLM w hw ∘L weightedShiftCLM w hw =
      (1 : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))

Uses 3 · Used by 1

Statement usesWeighted backward shift · Weighted forward shift operator

Proof usesThe weighted backward shift after the forward shift is diagonal

Used byWeighted shifts with unimodular weights preserve norms

TheoremWeighted shifts with nonzero weights are injective#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\) with \(w_n \neq 0\) for every \(n\). Then the weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\), is injective.

The coordinates of \(x\) are recovered from \(S_w x\) one by one: \(x_n = (S_w x)_{n+1} / w_n\).

theorem injective_weightedShiftCLM (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (h : ∀ n, w n ≠ 0) :
    Function.Injective (weightedShiftCLM w hw)

Uses 2

Statement usesWeighted forward shift operator

Proof usesCoordinates of the weighted forward shift

TheoremA vanishing weight makes the weighted shift non-injective#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be weights with bounded moduli. If \(w_n = 0\) for some \(n\), then the weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\) is not injective.

Indeed, \(S_w\) sends the \(n\)-th standard basis vector to \(0\).

theorem not_injective_weightedShiftCLM (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (n : ℕ) (hn : w n = 0) :
    ¬ Function.Injective (weightedShiftCLM w hw)

Uses 2

Statement usesWeighted forward shift operator

Proof usesThe weighted forward shift on basis vectors

TheoremWeighted shifts with unimodular weights preserve norms#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a sequence in \(\mathbb{K}\) with \(|w_n| = 1\) for every \(n\). Then the weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\), satisfies \(\|S_w x\| = \|x\|\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem norm_weightedShiftCLM_apply_of_forall_norm_eq_one (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (h : ∀ n, ‖w n‖ = 1)
    (x : ℓ²(ℕ, 𝕜)) : ‖weightedShiftCLM w hw x‖ = ‖x‖

Uses 5 · Used by 1

Statement usesWeighted forward shift operator

Proof usesThe weighted backward shift is a left inverse for unimodular weights · Norm of the weighted backward shift · Operator norm of a weighted shift · Weighted backward shift

Used byIsometric weighted shifts

TheoremIsometric weighted shifts#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \((w_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(\mathbb{K}\). The weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), given by \((S_w x)_0 = 0\) and \((S_w x)_{n+1} = w_n x_n\), is an isometry if and only if \(|w_n| = 1\) for every \(n\).

theorem isometry_weightedShiftCLM_iff (w : ℕ → 𝕜)
    (hw : BddAbove (Set.range fun n => ‖w n‖)) :
    Isometry (weightedShiftCLM w hw) ↔ ∀ n, ‖w n‖ = 1

Uses 3

Statement usesWeighted forward shift operator

Proof usesWeighted shifts with unimodular weights preserve norms · The weighted forward shift on basis vectors

TheoremThe weighted forward shift with unit weights is the unilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The weighted forward shift operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) whose weights are all equal to \(1\) is the unilateral forward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\).

theorem weightedShiftCLM_one {𝕜 : Type*} [RCLike 𝕜]
    (hw : BddAbove (Set.range fun _ : ℕ => ‖(1 : 𝕜)‖)) :
    weightedShiftCLM (fun _ : ℕ => (1 : 𝕜)) hw = LpShiftOperator.shiftCLM

Uses 4

Statement usesThe unilateral shift operator · Weighted forward shift operator

Proof usesCoordinates of the weighted forward shift · Weighted forward shift of a sequence

TheoremUnit weights give the plain backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). With every weight equal to \(1\), the weighted backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\) is the canonical backward shift.

theorem weightedBackwardCLM_one {𝕜 : Type*} [RCLike 𝕜]
    (hw : BddAbove (Set.range fun _ : ℕ => ‖(1 : 𝕜)‖)) :
    weightedBackwardCLM (fun _ : ℕ => (1 : 𝕜)) hw = LpShiftOperator.backwardCLM

Uses 4

Statement usesBackward shift · Weighted backward shift

Proof usesCoordinates of the weighted backward shift · Weighted backward shift of a sequence

DefinitionTruncated weights#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For a sequence \(w : \mathbb{N} \to \mathbb{K}\) and \(N \in \mathbb{N}\), the truncation of \(w\) after \(N\) coordinates is the sequence \(w^{(N)}\) with \(w^{(N)}_n = w_n\) for \(n < N\) and \(w^{(N)}_n = 0\) for \(n \ge N\).

def truncWeights (w : ℕ → 𝕜) (N : ℕ) : ℕ → 𝕜 := fun n => if n < N then w n else 0

Used by 4

Used byTruncated weights are bounded · Weighted shifts with truncated weights converge in operator norm · Truncated weights vanish from the cutoff on · Truncated weights agree with the weights below the cutoff

TheoremTruncated weights agree with the weights below the cutoff#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\), and let \(N, n \in \mathbb{N}\) with \(n < N\). Then the truncation \(w^{(N)}\) of \(w\) after \(N\) coordinates (equal to \(w_k\) for \(k < N\) and to \(0\) for \(k \ge N\)) satisfies \(w^{(N)}_n = w_n\).

theorem truncWeights_apply_lt {w : ℕ → 𝕜} {N n : ℕ} (h : n < N) :
    truncWeights w N n = w n

Uses 1 · Used by 2

Statement usesTruncated weights

Used byTruncated weights are bounded · Weighted shifts with truncated weights converge in operator norm

TheoremTruncated weights vanish from the cutoff on#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\), and let \(N, n \in \mathbb{N}\) with \(n \ge N\). Then the truncation \(w^{(N)}\) of \(w\) after \(N\) coordinates (equal to \(w_k\) for \(k < N\) and to \(0\) for \(k \ge N\)) satisfies \(w^{(N)}_n = 0\).

theorem truncWeights_apply_ge {w : ℕ → 𝕜} {N n : ℕ} (h : ¬ n < N) :
    truncWeights w N n = 0

Uses 1 · Used by 2

Statement usesTruncated weights

Used byTruncated weights are bounded · Weighted shifts with truncated weights converge in operator norm

TheoremTruncated weights are bounded#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be bounded, that is, \(|w_n| \le C\) for all \(n\) for some constant \(C\), and let \(N \in \mathbb{N}\). Then the truncation \(w^{(N)}\) of \(w\) after \(N\) coordinates, given by \(w^{(N)}_n = w_n\) for \(n < N\) and \(w^{(N)}_n = 0\) for \(n \ge N\), is bounded as well.

theorem bddAbove_truncWeights {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) (N : ℕ) :
    BddAbove (Set.range fun n => ‖truncWeights w N n‖)

Uses 3 · Used by 1

Statement usesTruncated weights

Proof usesTruncated weights vanish from the cutoff on · Truncated weights agree with the weights below the cutoff

Used byWeighted shifts with truncated weights converge in operator norm

TheoremDifferences of bounded sequences are bounded#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(w, v : \mathbb{N} \to \mathbb{K}\) be bounded sequences, that is, there are constants \(C\) and \(D\) with \(|w_n| \le C\) and \(|v_n| \le D\) for all \(n\). Then \(w - v\) is bounded: there is a constant \(E\) with \(|w_n - v_n| \le E\) for all \(n\).

theorem bddAbove_sub {w v : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖))
    (hv : BddAbove (Set.range fun n => ‖v n‖)) :
    BddAbove (Set.range fun n => ‖w n - v n‖)

Used by 1

Used byWeighted shifts with truncated weights converge in operator norm

TheoremWeighted shift of a difference of weights#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(w, v : \mathbb{N} \to \mathbb{K}\) be sequences such that \(w\), \(v\) and \(w - v\) are bounded. Writing \(S_u\) for the weighted forward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\) with bounded weights \(u\), sending \(x\) to \((0, u_0 x_0, u_1 x_1, \dots)\), we have \(S_{w - v} = S_w - S_v\).

theorem weightedShiftCLM_sub {w v : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖))
    (hv : BddAbove (Set.range fun n => ‖v n‖))
    (hsub : BddAbove (Set.range fun n => ‖w n - v n‖)) :
    weightedShiftCLM (w - v) hsub =
      weightedShiftCLM w hw - weightedShiftCLM v hv

Uses 4 · Used by 1

Statement usesWeighted forward shift operator

Proof usesDiagonal operator on ℓ² · Difference of diagonal operators · The unilateral shift operator

Used byWeighted shifts with truncated weights converge in operator norm

TheoremWeighted shifts with truncated weights converge in operator norm#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be a bounded sequence with \(w_n \to 0\). For \(N \in \mathbb{N}\) let \(w^{(N)}\) be the truncation of \(w\) after \(N\) coordinates, with \(w^{(N)}_n = w_n\) for \(n < N\) and \(w^{(N)}_n = 0\) for \(n \ge N\), and for bounded weights \(u\) let \(S_u\) be the weighted forward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\), sending \(x\) to \((0, u_0 x_0, u_1 x_1, \dots)\). Then \(S_{w^{(N)}} \to S_w\) in operator norm as \(N \to \infty\).

theorem tendsto_weightedShiftCLM_trunc {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖))
    (hw0 : Tendsto w atTop (𝓝 0)) :
    Tendsto (fun N => weightedShiftCLM (truncWeights w N) (bddAbove_truncWeights hw N))
      atTop (𝓝 (weightedShiftCLM w hw))

Uses 8

Statement usesTruncated weights are bounded · Truncated weights · Weighted forward shift operator

Proof usesDifferences of bounded sequences are bounded · Truncated weights vanish from the cutoff on · Truncated weights agree with the weights below the cutoff · Weighted shift of a difference of weights · Uniform weight bounds bound the weighted shift

TheoremCompactness criterion for weighted shifts#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(w : \mathbb{N} \to \mathbb{K}\) be a bounded sequence of weights, that is, \(|w_n| \le C\) for all \(n\) for some constant \(C\). The weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), which sends \(x\) to \((0, w_0 x_0, w_1 x_1, \dots)\), is a compact operator if and only if \(w_n \to 0\) as \(n \to \infty\).

theorem isCompactOperator_weightedShiftCLM_iff {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) :
    IsCompactOperator (weightedShiftCLM w hw) ↔ Tendsto w atTop (𝓝 0)

Uses 6 · Used by 1

Statement usesWeighted forward shift operator

Proof usesDiagonal operator on ℓ² · Compact diagonal operators on ℓ² · Backward shift · Left inverse of the unilateral shift · The unilateral shift operator

Used byWeighted shifts with eventually vanishing weights are compact

TheoremWeighted shifts with eventually vanishing weights are compact#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(w : \mathbb{N} \to \mathbb{K}\) be a bounded sequence of weights, and suppose there is \(N \in \mathbb{N}\) with \(w_n = 0\) for all \(n \ge N\). Then the weighted forward shift \(S_w\) on \(\ell^2(\mathbb{N}, \mathbb{K})\), which sends \(x\) to \((0, w_0 x_0, w_1 x_1, \dots)\), is a compact operator.

theorem isCompactOperator_weightedShift_of_forall_eq_zero {w : ℕ → 𝕜}
    (hw : BddAbove (Set.range fun n => ‖w n‖)) {N : ℕ}
    (hN : ∀ n, N ≤ n → w n = 0) :
    IsCompactOperator (weightedShiftCLM w hw)

Uses 2

Statement usesWeighted forward shift operator

Proof usesCompactness criterion for weighted shifts

42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.