Unilateral shift

DefinitionForward shift of a sequence#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The forward shift of a sequence \(x : \mathbb{N} \to \mathbb{K}\) is the sequence \(S x\) with \((S x)_0 = 0\) and \((S x)_{n+1} = x_n\) for every \(n \in \mathbb{N}\).

def shiftFun (x : ℕ → 𝕜) : ℕ → 𝕜
  | 0 => 0
  | n + 1 => x n
Used by 9
Used byShifted unilateral shift has trivial kernel · The forward shift of a square-summable sequence is square-summable · Coordinates of the unilateral shift · Pointwise action of a power of the unilateral shift · Powers of the unilateral shift as iterates of the shift map · Iterated forward shift inserts leading zeroes · Forward shift as a linear map · Coordinates of the forward-shift linear map · Square sum of the forward shift

DefinitionBackward shift of a sequence#✓fully proved

For any type \(K\), the backward shift of a sequence \(x \colon \mathbb{N} \to K\) is the sequence \(n \mapsto x_{n+1}\): it drops the coordinate \(x_0\) and shifts every other coordinate down by one.

def backwardFun (x : ℕ → 𝕜) (i : ℕ) : 𝕜 := x (i + 1)
Used by 8
Used byCoordinates of the backward shift · Pointwise action of a power of the backward shift · Powers of the backward shift as iterates of the backward map · Iterated backward shift drops leading coordinates · Backward shift as a linear map · Coordinates of the backward-shift linear map · The backward shift of an \(\ell^2\) sequence is in \(\ell^2\) · Square sum of the backward shift

TheoremThe forward shift of a square-summable sequence is square-summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every square-summable sequence \(x = (x_0, x_1, x_2, \dots)\) in \(\mathbb{K}\), the forward-shifted sequence \((0, x_0, x_1, \dots)\) is also square-summable, that is, it belongs to \(\ell^2(\mathbb{N}, \mathbb{K})\).

theorem memℓp_shiftFun {x : ℓ²(ℕ, 𝕜)} : Memℓp (shiftFun (x : ℕ → 𝕜)) 2
Uses 1 · Used by 2
Statement usesForward shift of a sequence
Used byForward shift as a linear map · Square sum of the forward shift

TheoremThe backward shift of an \(\ell^2\) sequence is in \(\ell^2\)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the backward shift \(n \mapsto x_{n+1}\) of the sequence \(x\) is square-summable, that is, it lies in \(\ell^2(\mathbb{N}, \mathbb{K})\).

Its squared absolute values are a tail of the squared absolute values of \(x\).

theorem memℓp_backwardFun {x : ℓ²(ℕ, 𝕜)} : Memℓp (backwardFun (x : ℕ → 𝕜)) 2
Uses 1 · Used by 1
Statement usesBackward shift of a sequence
Used byBackward shift as a linear map

DefinitionForward shift as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The forward shift is the \(\mathbb{K}\)-linear map \(\ell^2(\mathbb{N}, \mathbb{K}) \to \ell^2(\mathbb{N}, \mathbb{K})\) sending \(x\) to the forward shift of the sequence \(x\), that is, to \((0, x_0, x_1, \dots)\), which is again square-summable.

MathlibExt.Analysis.InnerProductSpace.LpShiftOperator.shiftLinMap · 18 lines 
noncomputable def shiftLinMap : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨shiftFun (x : ℕ → 𝕜), memℓp_shiftFun⟩
  map_add' x y := by
    apply lp.ext
    funext i
    cases i with
    | zero =>
        simp only [lp.coeFn_add, shiftFun_zero, Pi.add_apply, add_zero]
    | succ n => simp only [lp.coeFn_add, shiftFun_succ, Pi.add_apply]
  map_smul' c x := by
    apply lp.ext
    funext i
    cases i with
    | zero =>
        simp only [lp.coeFn_smul, shiftFun_zero, Pi.smul_apply, smul_zero]
    | succ n =>
        simp only [lp.coeFn_smul, shiftFun_succ, Pi.smul_apply, smul_eq_mul,
          RingHom.id_apply]
Uses 2 · Used by 4
Statement usesThe forward shift of a square-summable sequence is square-summable · Forward shift of a sequence
Used byThe unilateral shift has operator norm one · The forward shift linear map preserves norms · The unilateral shift operator · Coordinates of the forward-shift linear map

DefinitionBackward shift as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The backward-shift linear map is the \(\mathbb{K}\)-linear map \(B\) from \(\ell^2(\mathbb{N}, \mathbb{K})\) to itself given by \((Bx)_n = x_{n+1}\) for all \(x\) and all \(n \in \mathbb{N}\).

noncomputable def backwardLinMap : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨backwardFun (x : ℕ → 𝕜), memℓp_backwardFun⟩
  map_add' x y := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_add, backwardFun_apply, Pi.add_apply]
  map_smul' c x := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_smul, backwardFun_apply, Pi.smul_apply, smul_eq_mul,
      RingHom.id_apply]
Uses 2 · Used by 4
Statement usesBackward shift of a sequence · The backward shift of an \(\ell^2\) sequence is in \(\ell^2\)
Used byBackward shift · Coordinates of the backward-shift linear map · The backward shift has operator norm at most one · The backward shift linear map does not increase norms

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

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the \(i\)-th coordinate of the forward-shift linear map applied to \(x\) equals the \(i\)-th term of the forward shift of the sequence \(x\), namely \(0\) for \(i = 0\) and \(x_{i-1}\) for \(i \ge 1\).

theorem shiftLinMap_apply (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    shiftLinMap x i = shiftFun (x : ℕ → 𝕜) i
Uses 2
Statement usesForward shift of a sequence · Forward shift as a linear map

TheoremCoordinates of the backward-shift linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the \(i\)-th coordinate of the image of \(x\) under the backward-shift linear map \(B\) is the \(i\)-th term of the backward shift of the sequence \(x\), that is, \((Bx)_i = x_{i+1}\).

theorem backwardLinMap_apply (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    backwardLinMap x i = backwardFun (x : ℕ → 𝕜) i
Uses 2
Statement usesBackward shift of a sequence · Backward shift as a linear map

TheoremSquare sum of the forward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the forward shift \(S x = (0, x_0, x_1, \dots)\) of \(x\) satisfies \(\sum_{i=0}^{\infty} |(S x)_i|^2 = \sum_{i=0}^{\infty} |x_i|^2\).

theorem tsum_shiftFun_norm (x : ℓ²(ℕ, 𝕜)) :
    ∑' i, ‖shiftFun (x : ℕ → 𝕜) i‖ ^ (2 : ℝ≥0∞).toReal =
      ∑' i, ‖(x : ℕ → 𝕜) i‖ ^ (2 : ℝ≥0∞).toReal
Uses 2 · Used by 1
Statement usesForward shift of a sequence
Proof usesThe forward shift of a square-summable sequence is square-summable
Used byThe forward shift linear map preserves norms

TheoremSquare sum of the backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\), the backward shift \((x_1, x_2, \dots)\) of \(x\) satisfies \(\sum_{i=0}^{\infty} |x_{i+1}|^2 \le \sum_{i=0}^{\infty} |x_i|^2\): the left side is a tail of the right side.

theorem tsum_backwardFun_norm_le (x : ℓ²(ℕ, 𝕜)) :
    ∑' i, ‖backwardFun (x : ℕ → 𝕜) i‖ ^ (2 : ℝ≥0∞).toReal ≤
      ∑' i, ‖(x : ℕ → 𝕜) i‖ ^ (2 : ℝ≥0∞).toReal
Uses 1 · Used by 1
Statement usesBackward shift of a sequence
Used byThe backward shift linear map does not increase norms

TheoremThe forward shift linear map preserves norms#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) be the forward shift on the space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\), viewed as a linear map and given by \(S(x_0, x_1, \dots) = (0, x_0, x_1, \dots)\). Then \(\|Sx\| = \|x\|\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem norm_shiftLinMap_apply (x : ℓ²(ℕ, 𝕜)) : ‖shiftLinMap x‖ = ‖x‖
Uses 2 · Used by 3
Statement usesForward shift as a linear map
Proof usesSquare sum of the forward shift
Used byThe unilateral shift has operator norm one · The unilateral shift preserves norms · The unilateral shift operator

TheoremThe backward shift linear map does not increase norms#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(B\) be the backward shift on the space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\), viewed as a linear map and given by \((Bx)_n = x_{n+1}\). Then \(\|Bx\| \le \|x\|\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem norm_backwardLinMap_apply_le (x : ℓ²(ℕ, 𝕜)) : ‖backwardLinMap x‖ ≤ ‖x‖
Uses 2 · Used by 3
Statement usesBackward shift as a linear map
Proof usesSquare sum of the backward shift
Used byPowers of the backward shift do not increase norms · Backward shift · The backward shift has operator norm at most one

DefinitionThe unilateral shift operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The unilateral shift is the bounded linear operator \(S\) on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\) given by \(S(x_0, x_1, x_2, \dots) = (0, x_0, x_1, \dots)\). It is bounded because \(\|Sx\| = \|x\|\) for every \(x\).

noncomputable def shiftCLM : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  shiftLinMap.mkContinuous 1 (fun x => by
    rw [one_mul]
    exact le_of_eq (norm_shiftLinMap_apply x))
Uses 2 · Used by 63
Statement usesThe forward shift linear map preserves norms · Forward shift as a linear map
Used byRolewicz's theorem · Powers of the forward shift preserve norms · Distance from the periodic approximant to the truncation · Norm of a term of the periodic approximant · Periodic approximant of a truncated sequence · Periodic approximant is a periodic point · Action of the scaled backward shift power on approximant terms · First term of the periodic approximant is the truncation · Summability of the shifted periodic approximant terms · Summability of the periodic approximant terms · Diagonal slices are powers of the forward or backward shift · Adjoint of the unilateral shift · Backward shift power inverts the shift power modulo finite rank · Shift power inverts the backward shift power modulo finite rank · Backward shift power is a left inverse of the shift power · Left inverse of the unilateral shift · Essential spectrum of the unilateral shift is the unit circle · Dimension of the cokernel of a unilateral shift power · Fredholm index of the unilateral shift is \(-1\) · Fredholm index of a unilateral shift power is \(-n\) · Shift composed with backward shift has Fredholm index zero · Shifted unilateral shift has index \(-1\) inside the unit disk · Shifted unilateral shift has index zero outside the unit disk · The unilateral shift is injective · Injectivity of powers of the unilateral shift · Shifted unilateral shift has trivial kernel · Powers of the backward shift are Fredholm · Powers of the unilateral shift are Fredholm · Shift composed with backward shift is Fredholm · Shifted unilateral shift is Fredholm inside the unit disk · Shifted unilateral shift is Fredholm outside the unit disk · Shifted unilateral shift is invertible outside the unit disk · The unilateral shift preserves distances · Kernel of the first-coordinates map is the range of the shift power · Membership in the essential spectrum of the unilateral shift · Open unit disc lies in the forward shift's numerical range · Range of a power of the unilateral shift · The open unit ball lies in the spectrum of the unilateral shift · Forward shift's numerical range lies in the open unit disc · The unilateral shift has operator norm one · The unilateral shift preserves norms · Squared norm of the shifted shift on the truncated geometric vector · Shifted unilateral shift is not Fredholm on the unit circle · The unilateral shift is not surjective · Numerical range of the unilateral shift is the open unit disc · Forward shift quadratic form at a geometric vector · Quadratic form of the forward shift as a series · Coordinates of the unilateral shift · Pointwise action of a power of the unilateral shift · Powers of the unilateral shift as iterates of the shift map · The unilateral shift composed with the backward shift · Coordinates of the unilateral shift after the backward shift · Factorization of the shifted unilateral shift · Spectrum of the unilateral shift · Shifted unilateral shift on the truncated geometric vector · Surjectivity of powers of the backward shift · Adjoint of the weighted shift · Compactness criterion for weighted shifts · Operator norm of a weighted shift · Uniform weight bounds bound the weighted shift · Weighted forward shift operator · The weighted forward shift with unit weights is the unilateral shift · Weighted shift of a difference of weights

DefinitionBackward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The backward shift is the bounded linear operator \(B\) on \(\ell^2(\mathbb{N}, \mathbb{K})\) given by \((Bx)_n = x_{n+1}\) for all \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and \(n \in \mathbb{N}\).

noncomputable def backwardCLM : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  backwardLinMap.mkContinuous 1 (fun x => by
    rw [one_mul]
    exact norm_backwardLinMap_apply_le x)
Uses 2 · Used by 61
Statement usesBackward shift as a linear map · The backward shift linear map does not increase norms
Used byBackward shift annihilates truncations after \(N\) steps · Periodic points of \(\mu B\) are dense iff \(|\mu| > 1\) · Dense periodic points of the Rolewicz operator for \(|\mu| > 1\) · No nonzero periodic points of \(\mu B\) when \(|\mu| \le 1\) · Rolewicz's theorem · Powers of the backward shift do not increase norms · Periodic approximant is a periodic point · Action of the scaled backward shift power on approximant terms · Coordinate recurrence for periodic points of \(\mu B\) · Powers of a scaled backward shift as operators · Coordinates of powers of a scaled backward shift · Powers of a scalar multiple of the backward shift · Summability of the shifted periodic approximant terms · Diagonal slices are powers of the forward or backward shift · Adjoint of the unilateral shift · Backward shift power inverts the shift power modulo finite rank · Shift power inverts the backward shift power modulo finite rank · Coordinates of the backward shift · Backward shift of the geometric vector · Pointwise action of a power of the backward shift · Powers of the backward shift as iterates of the backward map · Backward shift power is a left inverse of the shift power · Left inverse of the unilateral shift · Kernel vectors of a backward shift power are zero-extended tuples · Finite-dimensionality of the kernel of a backward shift power · Dimension of the kernel of a backward shift power · Fredholm index of the backward shift is \(1\) · Fredholm index of a backward shift power is \(n\) · Shift composed with backward shift has Fredholm index zero · The unilateral shift is injective · Injectivity of powers of the unilateral shift · Powers of the backward shift are Fredholm · One minus a small multiple of the backward shift is Fredholm · Powers of the unilateral shift are Fredholm · Shift composed with backward shift is Fredholm · Shifted unilateral shift is Fredholm inside the unit disk · One minus a small multiple of the backward shift is invertible · Kernel of the backward shift power as a space of finite tuples · Kernel of the first-coordinates map is the range of the shift power · Kernel of a power of the backward shift · Open unit disc lies in the backward shift's numerical range · Range of a power of the unilateral shift · The open unit ball lies in the spectrum of the backward shift · The open unit ball lies in the spectrum of the unilateral shift · The backward shift has operator norm at most one · Backward shift's numerical range lies in the open unit disc · Numerical range of the backward shift is the open unit disc · Pointwise action of one minus a scaled backward shift · Backward shift quadratic form at a geometric vector · Quadratic form of the backward shift as a series · The unilateral shift composed with the backward shift · Coordinates of the unilateral shift after the backward shift · Factorization of the shifted unilateral shift · Spectrum of the backward shift · Surjectivity of powers of the backward shift · Adjoint of the weighted shift · Compactness criterion for weighted shifts · Norm of the weighted backward shift · Weighted backward shift · Coordinates of the weighted backward shift · Unit weights give the plain backward shift

TheoremCoordinates of the unilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) be the unilateral shift on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the coordinate \((Sx)_i\) is the \(i\)-th term of the forward shift of \(x\): \((Sx)_0 = 0\) and \((Sx)_{n+1} = x_n\) for every \(n \in \mathbb{N}\).

theorem shiftCLM_apply (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    shiftCLM x i = shiftFun (x : ℕ → 𝕜) i
Uses 2 · Used by 1
Statement usesThe unilateral shift operator · Forward shift of a sequence
Used byPowers of the unilateral shift as iterates of the shift map

TheoremCoordinates of the backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). For every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the \(i\)-th coordinate of the backward shift \(Bx\) is the \(i\)-th term of the backward shift of the sequence \(x\), that is, \((Bx)_i = x_{i+1}\).

theorem backwardCLM_apply (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    backwardCLM x i = backwardFun (x : ℕ → 𝕜) i
Uses 2 · Used by 1
Statement usesBackward shift · Backward shift of a sequence
Used byPowers of the backward shift as iterates of the backward map

TheoremThe unilateral shift preserves norms#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) be the unilateral shift on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\), given by \(S(x_0, x_1, \dots) = (0, x_0, x_1, \dots)\). Then \(\|Sx\| = \|x\|\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem norm_shiftCLM_apply (x : ℓ²(ℕ, 𝕜)) : ‖shiftCLM x‖ = ‖x‖
Uses 2 · Used by 3
Statement usesThe unilateral shift operator
Proof usesThe forward shift linear map preserves norms
Used byPowers of the forward shift preserve norms · The unilateral shift preserves distances · The unilateral shift has operator norm one

TheoremThe unilateral shift preserves distances#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The unilateral shift \(S\) on \(\ell^2(\mathbb{N}, \mathbb{K})\) is an isometry: \(\|Sx - Sy\| = \|x - y\|\) for all \(x, y \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem isometry_shiftCLM : Isometry (shiftCLM (𝕜 := 𝕜))
Uses 2
Statement usesThe unilateral shift operator
Proof usesThe unilateral shift preserves norms

TheoremThe unilateral shift has operator norm one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) be the unilateral shift on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\), given by \(S(x_0, x_1, \dots) = (0, x_0, x_1, \dots)\). Then the operator norm of \(S\) is \(\|S\| = 1\).

theorem norm_shiftCLM : ‖shiftCLM (𝕜 := 𝕜)‖ = 1
Uses 4 · Used by 4
Statement usesThe unilateral shift operator
Proof usesThe unilateral shift preserves norms · The forward shift linear map preserves norms · Forward shift as a linear map
Used byShifted unilateral shift is invertible outside the unit disk · Spectrum of the unilateral shift · Operator norm of a weighted shift · Uniform weight bounds bound the weighted shift

TheoremThe backward shift has operator norm at most one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(B\) be the backward shift on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\), given by \((Bx)_n = x_{n+1}\). Then the operator norm of \(B\) satisfies \(\|B\| \le 1\).

theorem norm_backwardCLM_le : ‖backwardCLM (𝕜 := 𝕜)‖ ≤ 1
Uses 3 · Used by 3
Statement usesBackward shift
Proof usesBackward shift as a linear map · The backward shift linear map does not increase norms
Used byOne minus a small multiple of the backward shift is invertible · Spectrum of the backward shift · Norm of the weighted backward shift

TheoremAdjoint of the unilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The adjoint of the unilateral shift \(S\) on \(\ell^2(\mathbb{N}, \mathbb{K})\) is the backward shift \(B\): \(S^* = B\).

theorem adjoint_shiftCLM : (shiftCLM (𝕜 := 𝕜))† = backwardCLM
Uses 2 · Used by 2
Statement usesBackward shift · The unilateral shift operator
Used byThe open unit ball lies in the spectrum of the unilateral shift · Adjoint of the weighted shift

TheoremLeft inverse of the unilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The backward shift \(B\) is a left inverse of the unilateral shift \(S\) on \(\ell^2(\mathbb{N}, \mathbb{K})\): \(BS = I\), where \(I\) is the identity operator.

theorem backward_comp_shift : backwardCLM ∘L shiftCLM = (1 : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))
Uses 2 · Used by 2
Statement usesBackward shift · The unilateral shift operator
Used byThe unilateral shift is injective · Compactness criterion for weighted shifts

TheoremThe unilateral shift is injective#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The unilateral shift on \(\ell^2(\mathbb{N}, \mathbb{K})\) is injective.

theorem injective_shiftCLM : Function.Injective (shiftCLM (𝕜 := 𝕜))
Uses 3
Statement usesThe unilateral shift operator
Proof usesBackward shift · Left inverse of the unilateral shift

TheoremCoordinates of the unilateral shift after the backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\) let \(S\) be the unilateral shift, \(S(x_0, x_1, \dots) = (0, x_0, x_1, \dots)\), and \(B\) the backward shift, \((Bx)_n = x_{n+1}\). Then for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\) and every \(i \in \mathbb{N}\), the coordinate \((SBx)_i\) is \(0\) if \(i = 0\) and is \(x_i\) if \(i \ne 0\).

theorem shift_comp_backward_apply (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (shiftCLM ∘L backwardCLM) x i = if i = 0 then 0 else x i
Uses 2 · Used by 1
Statement usesBackward shift · The unilateral shift operator
Used byThe unilateral shift composed with the backward shift

TheoremThe unilateral shift composed with the backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be the unilateral (forward) shift and \(B\) the backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\), and let \(e_0\) be the first standard basis vector. Then \(S \circ B = 1 - P\), where \(P\) is the rank-one operator \(P x = \langle e_0, x \rangle e_0 = x_0 e_0\).

Thus \(S \circ B\) is the orthogonal projection onto \(\{e_0\}^\perp\).

theorem shift_comp_backward :
    shiftCLM ∘L backwardCLM =
      (1 : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)) -
        InnerProductSpace.rankOne 𝕜 (lp.single 2 0 (1 : 𝕜) : ℓ²(ℕ, 𝕜))
          (lp.single 2 0 (1 : 𝕜) : ℓ²(ℕ, 𝕜))
Uses 3
Statement usesBackward shift · The unilateral shift operator
Proof usesCoordinates of the unilateral shift after the backward shift

TheoremThe unilateral shift is not surjective#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S\) be the unilateral shift on the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences in \(\mathbb{K}\), given by \(S(x_0, x_1, \dots) = (0, x_0, x_1, \dots)\). Then \(S\) is not surjective.

The first standard basis vector \(e_0 = (1, 0, 0, \dots)\) is not in the range of \(S\), since every vector in the range has \(0\) in coordinate \(0\).

theorem not_surjective_shiftCLM : ¬ Function.Surjective (shiftCLM (𝕜 := 𝕜))
Uses 1
Statement usesThe unilateral shift operator

TheoremGeometric sequences with ratio of norm less than one are square-summable#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(c \in \mathbb{K}\) with \(\|c\| < 1\). Then the sequence \((c^i)_{i \in \mathbb{N}}\) lies in \(\ell^2\), that is, \(\sum_{i} \|c^i\|^2 < \infty\).

theorem memℓp_geometric {c : 𝕜} (hc : ‖c‖ < 1) : Memℓp (fun i : ℕ => c ^ i) 2
Used by 1
Used byGeometric vector

DefinitionGeometric vector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(c \in \mathbb{K}\) with \(\|c\| < 1\). The geometric vector of \(c\) is the sequence \((1, c, c^2, \dots)\), that is \(i \mapsto c^i\), regarded as an element of the Hilbert space \(\ell^2(\mathbb{N}, \mathbb{K})\) of square-summable sequences.

noncomputable def geometricVec {c : 𝕜} (hc : ‖c‖ < 1) : ℓ²(ℕ, 𝕜) :=
  ⟨fun i => c ^ i, memℓp_geometric hc⟩
Uses 1 · Used by 5
Statement usesGeometric sequences with ratio of norm less than one are square-summable
Used byBackward shift of the geometric vector · Coordinates of the geometric vector · The geometric vector is nonzero · The open unit ball lies in the spectrum of the backward shift · The open unit ball lies in the spectrum of the unilateral shift

TheoremCoordinates of the geometric vector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(c \in \mathbb{K}\) with \(\|c\| < 1\). For every \(i \in \mathbb{N}\), the \(i\)-th coordinate of the geometric vector of \(c\) in \(\ell^2(\mathbb{N}, \mathbb{K})\) is \(c^i\).

theorem geometricVec_apply {c : 𝕜} (hc : ‖c‖ < 1) (i : ℕ) :
    geometricVec hc i = c ^ i
Uses 1 · Used by 1
Statement usesGeometric vector
Used byThe geometric vector is nonzero

TheoremThe geometric vector is nonzero#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(c \in \mathbb{K}\) with \(\|c\| < 1\). The geometric vector \((1, c, c^2, \dots)\) in \(\ell^2(\mathbb{N}, \mathbb{K})\) is nonzero, since its \(0\)-th coordinate is \(1\).

theorem geometricVec_ne_zero {c : 𝕜} (hc : ‖c‖ < 1) : geometricVec hc ≠ 0
Uses 2 · Used by 2
Statement usesGeometric vector
Proof usesCoordinates of the geometric vector
Used byThe open unit ball lies in the spectrum of the backward shift · The open unit ball lies in the spectrum of the unilateral shift

TheoremBackward shift of the geometric vector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(c \in \mathbb{K}\) with \(\|c\| < 1\). Let \(v = (1, c, c^2, \dots)\) be the geometric vector of \(c\) in \(\ell^2(\mathbb{N}, \mathbb{K})\) and let \(B\) be the backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\). Then \(Bv = c\,v\).

theorem backwardCLM_geometricVec {c : 𝕜} (hc : ‖c‖ < 1) :
    backwardCLM (geometricVec hc) = c • geometricVec hc
Uses 2 · Used by 2
Statement usesBackward shift · Geometric vector
Used byThe open unit ball lies in the spectrum of the backward shift · The open unit ball lies in the spectrum of the unilateral shift

TheoremThe identity on ℓ²(ℕ) has norm at most one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The operator norm of the identity operator on \(\ell^2(\mathbb{N}, \mathbb{K})\) is at most \(1\).

theorem norm_one_le : ‖(1 : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))‖ ≤ 1
Used by 2
Used bySpectrum of the backward shift · Spectrum of the unilateral shift

TheoremApplying a scalar operator minus an operator on ℓ²(ℕ)#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(T\) be a bounded linear operator on \(\ell^2(\mathbb{N}, \mathbb{K})\), let \(\mu \in \mathbb{K}\), and let \(\mu I\) be the image of \(\mu\) under the algebra map from \(\mathbb{K}\) into the bounded operators, i.e. \(\mu\) times the identity \(I\). Then \((\mu I - T)x = \mu x - Tx\) for every \(x \in \ell^2(\mathbb{N}, \mathbb{K})\).

theorem algebraMap_sub_apply (T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)) (μ : 𝕜)
    (x : ℓ²(ℕ, 𝕜)) :
    (algebraMap 𝕜 (ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)) μ - T) x = μ • x - T x
Used by 2
Used byThe open unit ball lies in the spectrum of the backward shift · The open unit ball lies in the spectrum of the unilateral shift

TheoremThe open unit ball lies in the spectrum of the unilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(S\) be the unilateral shift on \(\ell^2(\mathbb{N}, \mathbb{K})\). Every \(\mu \in \mathbb{K}\) with \(\|\mu\| < 1\) lies in the spectrum of \(S\) in the algebra of bounded operators on \(\ell^2(\mathbb{N}, \mathbb{K})\).

Indeed, write \(I\) for the identity operator. If \(\mu I - S\) were invertible it would be surjective, so \((\mu I - S)x = v\) for some \(x\), where \(v = (1, \bar\mu, \bar\mu^2, \dots)\) is the geometric vector of the conjugate \(\bar\mu\). Since the adjoint of \(S\) is the backward shift \(B\) and \(Bv = \bar\mu v\), pairing \((\mu I - S)x = v\) with \(v\) gives \(\|v\|^2 = 0\), contradicting \(v \neq 0\).

theorem mem_spectrum_shiftCLM_of_norm_lt {μ : 𝕜} (hμ : ‖μ‖ < 1) :
    μ ∈ spectrum 𝕜 (shiftCLM (𝕜 := 𝕜))
Uses 7 · Used by 1
Statement usesThe unilateral shift operator
Proof usesAdjoint of the unilateral shift · Backward shift · Applying a scalar operator minus an operator on ℓ²(ℕ) · Backward shift of the geometric vector · Geometric vector · The geometric vector is nonzero
Used bySpectrum of the unilateral shift

TheoremThe open unit ball lies in the spectrum of the backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(B\) be the backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\). Every \(\mu \in \mathbb{K}\) with \(\|\mu\| < 1\) lies in the spectrum of \(B\) in the algebra of bounded operators on \(\ell^2(\mathbb{N}, \mathbb{K})\).

Indeed, writing \(I\) for the identity operator, the geometric vector \((1, \mu, \mu^2, \dots)\) lies in the kernel of \(\mu I - B\), so \(\mu I - B\) is not injective, hence not invertible.

theorem mem_spectrum_backwardCLM_of_norm_lt {μ : 𝕜} (hμ : ‖μ‖ < 1) :
    μ ∈ spectrum 𝕜 (backwardCLM (𝕜 := 𝕜))
Uses 5 · Used by 1
Statement usesBackward shift
Proof usesApplying a scalar operator minus an operator on ℓ²(ℕ) · Backward shift of the geometric vector · Geometric vector · The geometric vector is nonzero
Used bySpectrum of the backward shift

TheoremSpectrum of the unilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The spectrum over \(\mathbb{K}\) of the unilateral shift on \(\ell^2(\mathbb{N}, \mathbb{K})\) is the closed unit ball \(\{\mu \in \mathbb{K} : |\mu| \le 1\}\) of \(\mathbb{K}\).

theorem spectrum_shiftCLM :
    spectrum 𝕜 (shiftCLM (𝕜 := 𝕜)) = Metric.closedBall 0 1
Uses 4
Statement usesThe unilateral shift operator
Proof usesThe unilateral shift has operator norm one · The open unit ball lies in the spectrum of the unilateral shift · The identity on ℓ²(ℕ) has norm at most one

TheoremSpectrum of the backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The spectrum of the backward shift on \(\ell^2(\mathbb{N}, \mathbb{K})\), in the algebra of bounded operators, is the closed unit ball \(\{\mu \in \mathbb{K} : \|\mu\| \le 1\}\): the closed unit disc when \(\mathbb{K} = \mathbb{C}\) and the interval \([-1, 1]\) when \(\mathbb{K} = \mathbb{R}\).

theorem spectrum_backwardCLM :
    spectrum 𝕜 (backwardCLM (𝕜 := 𝕜)) = Metric.closedBall 0 1
Uses 4
Statement usesBackward shift
Proof usesThe backward shift has operator norm at most one · The open unit ball lies in the spectrum of the backward shift · The identity on ℓ²(ℕ) has norm at most one

TheoremIterated forward shift inserts leading zeroes#✓fully proved

Iterating the forward-shift function n times inserts n zeroes in front of the sequence.

theorem shiftFun_iterate_apply (n : ℕ) (x : ℕ → 𝕜) (i : ℕ) :
    (shiftFun^[n]) x i = if i < n then 0 else x (i - n)
Uses 1 · Used by 1
Statement usesForward shift of a sequence
Used byPointwise action of a power of the unilateral shift

TheoremIterated backward shift drops leading coordinates#✓fully proved

Iterating the backward-shift function n times drops the first n coordinates.

theorem backwardFun_iterate_apply (n : ℕ) (x : ℕ → 𝕜) (i : ℕ) :
    (backwardFun^[n]) x i = x (i + n)
Uses 1 · Used by 1
Statement usesBackward shift of a sequence
Used byPointwise action of a power of the backward shift

TheoremPowers of the unilateral shift as iterates of the shift map#✓fully proved

The coercion of S ^ n is the n-fold iterate of shiftFun.

theorem shiftCLM_pow_coe (n : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    ((shiftCLM (𝕜 := 𝕜) ^ n) x : ℕ → 𝕜) = (shiftFun^[n]) (x : ℕ → 𝕜)
Uses 3 · Used by 1
Statement usesThe unilateral shift operator · Forward shift of a sequence
Proof usesCoordinates of the unilateral shift
Used byPointwise action of a power of the unilateral shift

TheoremPowers of the backward shift as iterates of the backward map#✓fully proved

The coercion of B ^ n is the n-fold iterate of backwardFun.

theorem backwardCLM_pow_coe (n : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    ((backwardCLM (𝕜 := 𝕜) ^ n) x : ℕ → 𝕜) = (backwardFun^[n]) (x : ℕ → 𝕜)
Uses 3 · Used by 1
Statement usesBackward shift · Backward shift of a sequence
Proof usesCoordinates of the backward shift
Used byPointwise action of a power of the backward shift

TheoremPointwise action of a power of the unilateral shift#✓fully proved

Pointwise action of S ^ n: it inserts n zeroes in front.

theorem shiftCLM_pow_apply (n : ℕ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (shiftCLM (𝕜 := 𝕜) ^ n) x i = if i < n then 0 else x (i - n)
Uses 4 · Used by 4
Statement usesThe unilateral shift operator
Proof usesForward shift of a sequence · Powers of the unilateral shift as iterates of the shift map · Iterated forward shift inserts leading zeroes
Used byDiagonal slices are powers of the forward or backward shift · Backward shift power is a left inverse of the shift power · Kernel of the first-coordinates map is the range of the shift power · Range of a power of the unilateral shift

TheoremPointwise action of a power of the backward shift#✓fully proved

Pointwise action of B ^ n: it drops the first n coordinates.

theorem backwardCLM_pow_apply (n : ℕ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    (backwardCLM (𝕜 := 𝕜) ^ n) x i = x (i + n)
Uses 4 · Used by 8
Statement usesBackward shift
Proof usesBackward shift of a sequence · Powers of the backward shift as iterates of the backward map · Iterated backward shift drops leading coordinates
Used byBackward shift annihilates truncations after \(N\) steps · Rolewicz's theorem · Coordinates of powers of a scaled backward shift · Diagonal slices are powers of the forward or backward shift · Backward shift power is a left inverse of the shift power · Kernel of the first-coordinates map is the range of the shift power · Kernel of a power of the backward shift · Range of a power of the unilateral shift

TheoremBackward shift power is a left inverse of the shift power#✓fully proved

B ^ n is a left inverse of S ^ n: shifting up then down recovers the original sequence.

theorem backwardCLM_pow_comp_shiftCLM_pow (n : ℕ) :
    (backwardCLM (𝕜 := 𝕜) ^ n) ∘L (shiftCLM (𝕜 := 𝕜) ^ n) = (1 : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))
Uses 4 · Used by 6
Statement usesBackward shift · The unilateral shift operator
Proof usesPointwise action of a power of the backward shift · Pointwise action of a power of the unilateral shift
Used byRolewicz's theorem · Action of the scaled backward shift power on approximant terms · Backward shift power inverts the shift power modulo finite rank · Shift power inverts the backward shift power modulo finite rank · Injectivity of powers of the unilateral shift · Surjectivity of powers of the backward shift

TheoremInjectivity of powers of the unilateral shift#✓fully proved

The unilateral shift power is injective.

theorem injective_shiftCLM_pow (n : ℕ) :
    Function.Injective ⇑(shiftCLM (𝕜 := 𝕜) ^ n)
Uses 3 · Used by 1
Statement usesThe unilateral shift operator
Proof usesBackward shift · Backward shift power is a left inverse of the shift power
Used byFredholm index of a unilateral shift power is \(-n\)

TheoremSurjectivity of powers of the backward shift#✓fully proved

The backward shift power is surjective.

theorem surjective_backwardCLM_pow (n : ℕ) :
    Function.Surjective ⇑(backwardCLM (𝕜 := 𝕜) ^ n)
Uses 3 · Used by 1
Statement usesBackward shift
Proof usesThe unilateral shift operator · Backward shift power is a left inverse of the shift power
Used byFredholm index of a backward shift power is \(n\)

TheoremKernel of a power of the backward shift#✓fully proved

A vector is in the kernel of B ^ n iff its coordinates from n onwards all vanish.

theorem mem_ker_backwardCLM_pow (n : ℕ) (x : ℓ²(ℕ, 𝕜)) :
    (backwardCLM (𝕜 := 𝕜) ^ n) x = 0 ↔ ∀ i, x (i + n) = 0
Uses 2 · Used by 2
Statement usesBackward shift
Proof usesPointwise action of a power of the backward shift
Used byKernel vectors of a backward shift power are zero-extended tuples · Kernel of the backward shift power as a space of finite tuples

TheoremRange of a power of the unilateral shift#✓fully proved

A vector is in the range of S ^ n iff its first n coordinates vanish.

theorem mem_range_shiftCLM_pow (n : ℕ) (y : ℓ²(ℕ, 𝕜)) :
    (∃ x, (shiftCLM (𝕜 := 𝕜) ^ n) x = y) ↔ ∀ i < n, y i = 0
Uses 4
Statement usesThe unilateral shift operator
Proof usesBackward shift · Pointwise action of a power of the backward shift · Pointwise action of a power of the unilateral shift

DefinitionFirst-coordinates map on square-summable sequences#✓fully proved

The map taking a sequence to its first n coordinates.

noncomputable def firstCoords (n : ℕ) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] (Fin n → 𝕜) where
  toFun x i := (x : ℕ → 𝕜) (i : ℕ)
  map_add' x y := by
    funext i
    simp
  map_smul' c x := by
    funext i
    simp [lp.coeFn_smul]
Used by 5
Used byKernel vectors of a backward shift power are zero-extended tuples · Dimension of the cokernel of a unilateral shift power · First coordinates of a zero extension recover the tuple · Kernel of the backward shift power as a space of finite tuples · Kernel of the first-coordinates map is the range of the shift power

DefinitionExtension of a finite tuple by zeroes#✓fully proved

The extension of a tuple of n coordinates by zeroes.

def extZeroFun {n : ℕ} (v : Fin n → 𝕜) (j : ℕ) : 𝕜 :=
  if h : j < n then v ⟨j, h⟩ else 0
Used by 6
Used byLinear extension-by-zero map into \(\ell^2\) · Pointwise action of the extension-by-zero map · Kernel vectors of a backward shift power are zero-extended tuples · First coordinates of a zero extension recover the tuple · Kernel of the backward shift power as a space of finite tuples · Zero-extended finite tuples are square-summable

TheoremZero-extended finite tuples are square-summable#✓fully proved

A finitely supported sequence is in ℓ².

theorem memℓp_extZeroFun {n : ℕ} (v : Fin n → 𝕜) : Memℓp (extZeroFun v) 2
Uses 1 · Used by 1
Statement usesExtension of a finite tuple by zeroes
Used byLinear extension-by-zero map into \(\ell^2\)

DefinitionLinear extension-by-zero map into \(\ell^2\)#✓fully proved

The linear extension-by-zero map (Fin n → 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜).

MathlibExt.Analysis.InnerProductSpace.ShiftFredholmIndex.extZero · 18 lines 
noncomputable def extZero (n : ℕ) : (Fin n → 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun v := ⟨extZeroFun v, memℓp_extZeroFun v⟩
  map_add' v w := by
    apply lp.ext
    funext j
    show extZeroFun (v + w) j = extZeroFun v j + extZeroFun w j
    by_cases hj : j < n
    · rw [extZeroFun_apply_of_lt (v + w) hj, extZeroFun_apply_of_lt v hj,
        extZeroFun_apply_of_lt w hj, Pi.add_apply]
    · rw [extZeroFun_apply_of_ge (v + w) hj, extZeroFun_apply_of_ge v hj,
        extZeroFun_apply_of_ge w hj, add_zero]
  map_smul' c v := by
    apply lp.ext
    funext j
    show extZeroFun (c • v) j = c • extZeroFun v j
    by_cases hj : j < n
    · rw [extZeroFun_apply_of_lt (c • v) hj, extZeroFun_apply_of_lt v hj, Pi.smul_apply]
    · rw [extZeroFun_apply_of_ge (c • v) hj, extZeroFun_apply_of_ge v hj, smul_zero]
Uses 2 · Used by 5
Statement usesExtension of a finite tuple by zeroes · Zero-extended finite tuples are square-summable
Used byPointwise action of the extension-by-zero map · Kernel vectors of a backward shift power are zero-extended tuples · Dimension of the cokernel of a unilateral shift power · First coordinates of a zero extension recover the tuple · Kernel of the backward shift power as a space of finite tuples

TheoremPointwise action of the extension-by-zero map#✓fully proved

Pointwise action of the extension-by-zero map.

theorem extZero_apply (n : ℕ) (v : Fin n → 𝕜) (j : ℕ) :
    (extZero n v : ℕ → 𝕜) j = extZeroFun v j
Uses 2 · Used by 3
Statement usesLinear extension-by-zero map into \(\ell^2\) · Extension of a finite tuple by zeroes
Used byKernel vectors of a backward shift power are zero-extended tuples · First coordinates of a zero extension recover the tuple · Kernel of the backward shift power as a space of finite tuples

TheoremFirst coordinates of a zero extension recover the tuple#✓fully proved

Taking first coordinates after extension by zeroes is the identity.

theorem firstCoords_extZero (n : ℕ) (v : Fin n → 𝕜) :
    firstCoords n (extZero n v) = v
Uses 4 · Used by 2
Statement usesLinear extension-by-zero map into \(\ell^2\) · First-coordinates map on square-summable sequences
Proof usesExtension of a finite tuple by zeroes · Pointwise action of the extension-by-zero map
Used byDimension of the cokernel of a unilateral shift power · Kernel of the backward shift power as a space of finite tuples

TheoremKernel vectors of a backward shift power are zero-extended tuples#✓fully proved

A vector in the kernel of B ^ n is determined by its first n coordinates: extending those coordinates by zeroes recovers it.

theorem extZero_firstCoords_of_mem_ker (n : ℕ) {x : ℓ²(ℕ, 𝕜)}
    (hx : x ∈ (↑(backwardCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)).ker) :
    extZero n (firstCoords n x) = x
Uses 6 · Used by 1
Statement usesBackward shift · Linear extension-by-zero map into \(\ell^2\) · First-coordinates map on square-summable sequences
Proof usesExtension of a finite tuple by zeroes · Pointwise action of the extension-by-zero map · Kernel of a power of the backward shift
Used byKernel of the backward shift power as a space of finite tuples

DefinitionKernel of the backward shift power as a space of finite tuples#✓fully proved

The kernel of B ^ n is linearly equivalent to Fin n → 𝕜: a vector in the kernel is exactly its first n coordinates.

noncomputable def kerBackwardCLM_powEquiv (n : ℕ) :
    (↑(backwardCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)).ker ≃ₗ[𝕜] (Fin n → 𝕜) where
  toFun x := firstCoords n x
  invFun v := ⟨extZero n v, by
    rw [LinearMap.mem_ker]
    exact (mem_ker_backwardCLM_pow n (extZero n v)).mpr (fun i => by
      rw [extZero_apply, extZeroFun_apply_of_ge _ (by omega : ¬ i + n < n)])⟩
  left_inv x := by
    apply Subtype.ext
    exact extZero_firstCoords_of_mem_ker n x.property
  right_inv v := firstCoords_extZero n v
  map_add' x y := by simp
  map_smul' c x := by simp
Uses 8 · Used by 2
Statement usesBackward shift · Linear extension-by-zero map into \(\ell^2\) · Extension of a finite tuple by zeroes · Pointwise action of the extension-by-zero map · Kernel vectors of a backward shift power are zero-extended tuples · First-coordinates map on square-summable sequences · First coordinates of a zero extension recover the tuple · Kernel of a power of the backward shift
Used byFinite-dimensionality of the kernel of a backward shift power · Dimension of the kernel of a backward shift power

TheoremFinite-dimensionality of the kernel of a backward shift power#✓fully proved

The kernel of B ^ n is finite-dimensional.

theorem finiteDimensional_ker_backwardCLM_pow (n : ℕ) :
    FiniteDimensional 𝕜 (↑(backwardCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)).ker
Uses 2 · Used by 1
Statement usesBackward shift
Proof usesKernel of the backward shift power as a space of finite tuples
Used byShift power inverts the backward shift power modulo finite rank

TheoremDimension of the kernel of a backward shift power#✓fully proved

The kernel of B ^ n has dimension n.

theorem finrank_ker_backwardCLM_pow (n : ℕ) :
    Module.finrank 𝕜 (↑(backwardCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)).ker = n
Uses 2 · Used by 1
Statement usesBackward shift
Proof usesKernel of the backward shift power as a space of finite tuples
Used byFredholm index of a backward shift power is \(n\)

TheoremKernel of the first-coordinates map is the range of the shift power#✓fully proved

The kernel of the first-n-coordinates map is the range of S ^ n: both consist of the sequences whose first n coordinates vanish.

theorem ker_firstCoords_eq_range_shiftCLM_pow (n : ℕ) :
    (firstCoords n).ker = (↑(shiftCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)).range
Uses 5 · Used by 1
Statement usesThe unilateral shift operator · First-coordinates map on square-summable sequences
Proof usesBackward shift · Pointwise action of a power of the backward shift · Pointwise action of a power of the unilateral shift
Used byDimension of the cokernel of a unilateral shift power

TheoremDimension of the cokernel of a unilateral shift power#✓fully proved

The cokernel of S ^ n has dimension n: the quotient of ℓ² by the range of S ^ n is equivalent to Fin n → 𝕜 via the first n coordinates.

theorem finrank_quotient_range_shiftCLM_pow (n : ℕ) :
    Module.finrank 𝕜 (ℓ²(ℕ, 𝕜) ⧸ (↑(shiftCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)).range) = n
Uses 5 · Used by 1
Statement usesThe unilateral shift operator
Proof usesLinear extension-by-zero map into \(\ell^2\) · First-coordinates map on square-summable sequences · First coordinates of a zero extension recover the tuple · Kernel of the first-coordinates map is the range of the shift power
Used byFredholm index of a unilateral shift power is \(-n\)

TheoremBackward shift power inverts the shift power modulo finite rank#✓fully proved

The quasi-inverse relation B ^ n ∘L S ^ n = 1 holds exactly, hence also modulo finite-rank operators.

theorem approx_backward_comp_shift (n : ℕ) :
    (↑(backwardCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)) ∘ₗ ↑(shiftCLM (𝕜 := 𝕜) ^ n) ≈
      LinearMap.id
Uses 3 · Used by 2
Statement usesBackward shift · The unilateral shift operator
Proof usesBackward shift power is a left inverse of the shift power
Used byPowers of the backward shift are Fredholm · Powers of the unilateral shift are Fredholm

TheoremShift power inverts the backward shift power modulo finite rank#✓fully proved

The defect S ^ n ∘L B ^ n - 1 has finite rank: its range lies in the finite-dimensional kernel of B ^ n, since applying B ^ n after it gives 0.

theorem approx_shift_comp_backward (n : ℕ) :
    (↑(shiftCLM (𝕜 := 𝕜) ^ n) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜)) ∘ₗ ↑(backwardCLM (𝕜 := 𝕜) ^ n) ≈
      LinearMap.id
Uses 4 · Used by 3
Statement usesBackward shift · The unilateral shift operator
Proof usesBackward shift power is a left inverse of the shift power · Finite-dimensionality of the kernel of a backward shift power
Used byPowers of the backward shift are Fredholm · Powers of the unilateral shift are Fredholm · Shifted unilateral shift is Fredholm inside the unit disk

TheoremPowers of the unilateral shift are Fredholm#✓fully proved

Every power of the unilateral shift is a Fredholm operator: B ^ n is a quasi-inverse.

theorem isFredholm_shiftCLM_pow (n : ℕ) : (shiftCLM (𝕜 := 𝕜) ^ n).IsFredholm
Uses 4 · Used by 3
Statement usesThe unilateral shift operator
Proof usesBackward shift · Backward shift power inverts the shift power modulo finite rank · Shift power inverts the backward shift power modulo finite rank
Used byShift composed with backward shift has Fredholm index zero · Shift composed with backward shift is Fredholm · Shifted unilateral shift is Fredholm inside the unit disk

TheoremPowers of the backward shift are Fredholm#✓fully proved

Every power of the backward shift is a Fredholm operator: S ^ n is a quasi-inverse.

theorem isFredholm_backwardCLM_pow (n : ℕ) : (backwardCLM (𝕜 := 𝕜) ^ n).IsFredholm
Uses 4 · Used by 2
Statement usesBackward shift
Proof usesThe unilateral shift operator · Backward shift power inverts the shift power modulo finite rank · Shift power inverts the backward shift power modulo finite rank
Used byShift composed with backward shift has Fredholm index zero · Shift composed with backward shift is Fredholm

TheoremFredholm index of a unilateral shift power is \(-n\)#✓fully proved

The Fredholm index of S ^ n is -n: the shift power is injective, and its cokernel has dimension n.

theorem index_shiftCLM_pow (n : ℕ) : (shiftCLM (𝕜 := 𝕜) ^ n).index = -(n : ℤ)
Uses 3 · Used by 1
Statement usesThe unilateral shift operator
Proof usesDimension of the cokernel of a unilateral shift power · Injectivity of powers of the unilateral shift
Used byFredholm index of the unilateral shift is \(-1\)

TheoremFredholm index of a backward shift power is \(n\)#✓fully proved

The Fredholm index of B ^ n is n: the backward shift power is surjective, and its kernel has dimension n.

theorem index_backwardCLM_pow (n : ℕ) : (backwardCLM (𝕜 := 𝕜) ^ n).index = (n : ℤ)
Uses 3 · Used by 1
Statement usesBackward shift
Proof usesDimension of the kernel of a backward shift power · Surjectivity of powers of the backward shift
Used byFredholm index of the backward shift is \(1\)

TheoremFredholm index of the unilateral shift is \(-1\)#✓fully proved

The Fredholm index of the unilateral shift is -1.

theorem index_shiftCLM : (shiftCLM : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)).index = -1
Uses 2 · Used by 2
Statement usesThe unilateral shift operator
Proof usesFredholm index of a unilateral shift power is \(-n\)
Used byShift composed with backward shift has Fredholm index zero · Shifted unilateral shift has index \(-1\) inside the unit disk

TheoremFredholm index of the backward shift is \(1\)#✓fully proved

The Fredholm index of the backward shift is 1.

theorem index_backwardCLM : (backwardCLM : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)).index = 1
Uses 2 · Used by 1
Statement usesBackward shift
Proof usesFredholm index of a backward shift power is \(n\)
Used byShift composed with backward shift has Fredholm index zero

TheoremShift composed with backward shift is Fredholm#✓fully proved

S ∘L B is Fredholm: it is the composite of two Fredholm operators.

theorem isFredholm_shift_comp_backward : (shiftCLM (𝕜 := 𝕜) ∘L backwardCLM (𝕜 := 𝕜)).IsFredholm
Uses 4
Statement usesBackward shift · The unilateral shift operator
Proof usesPowers of the backward shift are Fredholm · Powers of the unilateral shift are Fredholm

TheoremShift composed with backward shift has Fredholm index zero#✓fully proved

S ∘L B has Fredholm index 0, as index additivity under composition demands: (-1) + 1 = 0.

theorem index_shift_comp_backward : (shiftCLM (𝕜 := 𝕜) ∘L backwardCLM (𝕜 := 𝕜)).index = 0
Uses 6
Statement usesBackward shift · The unilateral shift operator
Proof usesFredholm index of the backward shift is \(1\) · Fredholm index of the unilateral shift is \(-1\) · Powers of the backward shift are Fredholm · Powers of the unilateral shift are Fredholm

DefinitionEssential spectrum of a bounded operator#✓fully proved

The essential spectrum of a bounded operator T: the set of scalars μ for which T - μ • 1 is not a Fredholm operator.

def essentialSpectrum {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    (T : E →L[𝕜] E) : Set 𝕜 :=
  {μ | ¬ (T - μ • 1).IsFredholm}
Used by 2
Used byEssential spectrum of the unilateral shift is the unit circle · Membership in the essential spectrum of the unilateral shift

TheoremPointwise action of one minus a scaled backward shift#✓fully proved

Pointwise action of 1 - μ • B.

theorem one_sub_smul_backward_apply (μ : 𝕜) (x : ℓ²(ℕ, 𝕜)) (j : ℕ) :
    ((1 - μ • LpShiftOperator.backwardCLM (𝕜 := 𝕜)) x : ℕ → 𝕜) j =
      (x : ℕ → 𝕜) j - μ * (x : ℕ → 𝕜) (j + 1)
Uses 1
Statement usesBackward shift

TheoremFactorization of the shifted unilateral shift#✓fully proved

The key factorization: S - μ = S (1 - μ B) + μ (S B - 1).

theorem shift_sub_smul_one_eq (μ : 𝕜) :
    LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1 =
      LpShiftOperator.shiftCLM (𝕜 := 𝕜) ∘L (1 - μ • LpShiftOperator.backwardCLM (𝕜 := 𝕜)) +
        μ • (LpShiftOperator.shiftCLM (𝕜 := 𝕜) ∘L LpShiftOperator.backwardCLM (𝕜 := 𝕜) - 1)
Uses 2 · Used by 1
Statement usesBackward shift · The unilateral shift operator
Used byShifted unilateral shift is Fredholm inside the unit disk

TheoremShifted unilateral shift has trivial kernel#✓fully proved

S - μ • 1 has trivial kernel for every μ: the coordinate equations force every coordinate to vanish.

theorem injective_shift_sub (μ : 𝕜) :
    Function.Injective ⇑(LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1 : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜))
Uses 2 · Used by 1
Statement usesThe unilateral shift operator
Proof usesForward shift of a sequence
Used byShifted unilateral shift is not Fredholm on the unit circle

TheoremOne minus a small multiple of the backward shift is invertible#✓fully proved

1 - μ • B is a unit when ‖μ‖ < 1, by the Neumann-series criterion isUnit_one_sub_of_norm_lt_one.

theorem isUnit_one_sub_smul_backward {μ : 𝕜} (hμ : ‖μ‖ < 1) :
    IsUnit (1 - μ • LpShiftOperator.backwardCLM (𝕜 := 𝕜))
Uses 2 · Used by 1
Statement usesBackward shift
Proof usesThe backward shift has operator norm at most one
Used byOne minus a small multiple of the backward shift is Fredholm

TheoremInvertible operators are Fredholm#✓fully proved

A unit operator is Fredholm, via IsHomeomorph and IsInvertible.isFredholm.

theorem isFredholm_of_isUnit {T : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜)} (hT : IsUnit T) :
    T.IsFredholm
Used by 2
Used byOne minus a small multiple of the backward shift is Fredholm · Shifted unilateral shift is Fredholm outside the unit disk

TheoremOne minus a small multiple of the backward shift is Fredholm#✓fully proved

1 - μ • B is Fredholm when ‖μ‖ < 1.

theorem isFredholm_one_sub_smul_backward {μ : 𝕜} (hμ : ‖μ‖ < 1) :
    (1 - μ • LpShiftOperator.backwardCLM (𝕜 := 𝕜)).IsFredholm
Uses 3 · Used by 1
Statement usesBackward shift
Proof usesInvertible operators are Fredholm · One minus a small multiple of the backward shift is invertible
Used byShifted unilateral shift is Fredholm inside the unit disk

TheoremShifted unilateral shift is Fredholm inside the unit disk#✓fully proved

For ‖μ‖ < 1, S - μ • 1 is Fredholm: it is the Fredholm operator S (1 - μ B) plus the finite-rank operator μ (S B - 1).

theorem isFredholm_shift_sub_smul_one_of_norm_lt_one {μ : 𝕜} (hμ : ‖μ‖ < 1) :
    (LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1).IsFredholm
Uses 6 · Used by 2
Statement usesThe unilateral shift operator
Proof usesBackward shift · One minus a small multiple of the backward shift is Fredholm · Factorization of the shifted unilateral shift · Shift power inverts the backward shift power modulo finite rank · Powers of the unilateral shift are Fredholm
Used byEssential spectrum of the unilateral shift is the unit circle · Shifted unilateral shift has index \(-1\) inside the unit disk

TheoremShifted unilateral shift has index \(-1\) inside the unit disk#✓fully proved

The index of S - μ • 1 is -1 for ‖μ‖ < 1: the canonical homotopy theorem makes the index constant along S - (t μ) • 1, t ∈ [0, 1], and the canonical shift has index -1 at t = 0.

theorem index_shift_sub_smul_one_of_norm_lt_one {μ : 𝕜} (hμ : ‖μ‖ < 1) :
    (LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1).index = -1
Uses 4
Statement usesThe unilateral shift operator
Proof usesShifted unilateral shift is Fredholm inside the unit disk · Fredholm index of the unilateral shift is \(-1\) · Fredholm index is constant along a globally continuous path

TheoremShifted unilateral shift is invertible outside the unit disk#✓fully proved

For ‖μ‖ > 1, S - μ • 1 is a unit: it equals (algebraMap (-μ)) * (1 - μ⁻¹ • S), a product of units.

theorem isUnit_shift_sub_smul_one_of_one_lt_norm {μ : 𝕜} (hμ : 1 < ‖μ‖) :
    IsUnit (LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1)
Uses 2 · Used by 2
Statement usesThe unilateral shift operator
Proof usesThe unilateral shift has operator norm one
Used byShifted unilateral shift has index zero outside the unit disk · Shifted unilateral shift is Fredholm outside the unit disk

TheoremShifted unilateral shift is Fredholm outside the unit disk#✓fully proved

For ‖μ‖ > 1, S - μ • 1 is Fredholm, as it is a unit.

theorem isFredholm_shift_sub_smul_one_of_one_lt_norm {μ : 𝕜} (hμ : 1 < ‖μ‖) :
    (LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1).IsFredholm
Uses 3 · Used by 1
Statement usesThe unilateral shift operator
Proof usesInvertible operators are Fredholm · Shifted unilateral shift is invertible outside the unit disk
Used byEssential spectrum of the unilateral shift is the unit circle

TheoremShifted unilateral shift has index zero outside the unit disk#✓fully proved

For ‖μ‖ > 1, S - μ • 1 has index 0: a unit is bijective.

theorem index_shift_sub_smul_one_of_one_lt_norm {μ : 𝕜} (hμ : 1 < ‖μ‖) :
    (LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1).index = 0
Uses 2
Statement usesThe unilateral shift operator
Proof usesShifted unilateral shift is invertible outside the unit disk

DefinitionTruncated geometric sequence#✓fully proved

The truncated geometric sequence (1, μ̄, μ̄², …, μ̄ᴺ, 0, …).

def approxFun (μ : 𝕜) (N : ℕ) : ℕ → 𝕜 := fun n => if n ≤ N then (star μ) ^ n else 0
Used by 3
Used byTruncated geometric vector in \(\ell^2\) · Truncated geometric sequence is square-summable · Squared norm of the shifted shift on the truncated geometric vector

TheoremTruncated geometric sequence is square-summable#✓fully proved

The truncated geometric sequence is in ℓ²: it has finite support.

theorem memℓp_approxFun (μ : 𝕜) (N : ℕ) : Memℓp (approxFun μ N) 2
Uses 1 · Used by 1
Statement usesTruncated geometric sequence
Used byTruncated geometric vector in \(\ell^2\)

DefinitionTruncated geometric vector in \(\ell^2\)#✓fully proved

The truncated geometric sequence as an ℓ² vector.

noncomputable def approxVec (μ : 𝕜) (N : ℕ) : ℓ²(ℕ, 𝕜) := ⟨approxFun μ N, memℓp_approxFun μ N⟩
Uses 2 · Used by 4
Statement usesTruncated geometric sequence · Truncated geometric sequence is square-summable
Used bySquared norm of the truncated geometric vector · Squared norm of the shifted shift on the truncated geometric vector · Shifted unilateral shift is not Fredholm on the unit circle · Shifted unilateral shift on the truncated geometric vector

TheoremSquared norm of the truncated geometric vector#✓fully proved

The squared norm of the truncated geometric vector is N + 1, when ‖μ‖ = 1.

theorem norm_sq_approxVec {μ : 𝕜} (hμ : ‖μ‖ = 1) (N : ℕ) :
    ‖approxVec μ N‖ ^ 2 = (N + 1 : ℝ)
Uses 1 · Used by 1
Statement usesTruncated geometric vector in \(\ell^2\)
Used byShifted unilateral shift is not Fredholm on the unit circle

TheoremShifted unilateral shift on the truncated geometric vector#✓fully proved

The coordinates of (S - μ • 1) applied to the truncated geometric vector: -μ at 0, (star μ)^N at N + 1, and 0 elsewhere, when ‖μ‖ = 1.

theorem sub_smul_one_approxVec_apply_zero {μ : 𝕜} (N : ℕ) :
    ((LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1) (approxVec μ N)) 0 = -μ
Uses 2 · Used by 1
Statement usesThe unilateral shift operator · Truncated geometric vector in \(\ell^2\)
Used bySquared norm of the shifted shift on the truncated geometric vector

TheoremSquared norm of the shifted shift on the truncated geometric vector#✓fully proved

The squared norm of (S - μ • 1) applied to the truncated geometric vector is 2, when ‖μ‖ = 1.

theorem norm_sq_sub_smul_one_approxVec {μ : 𝕜} (hμ : ‖μ‖ = 1) (N : ℕ) :
    ‖(LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1) (approxVec μ N)‖ ^ 2 = 2
Uses 4 · Used by 1
Statement usesThe unilateral shift operator · Truncated geometric vector in \(\ell^2\)
Proof usesTruncated geometric sequence · Shifted unilateral shift on the truncated geometric vector
Used byShifted unilateral shift is not Fredholm on the unit circle

TheoremShifted unilateral shift is not Fredholm on the unit circle#✓fully proved

For ‖μ‖ = 1, S - μ • 1 is not Fredholm: it has trivial kernel and closed range would make it bounded below, contradicting the approximate eigenvectors.

theorem not_isFredholm_shift_sub_smul_one_of_norm_eq_one {μ : 𝕜} (hμ : ‖μ‖ = 1) :
    ¬ (LpShiftOperator.shiftCLM (𝕜 := 𝕜) - μ • 1).IsFredholm
Uses 5 · Used by 1
Statement usesThe unilateral shift operator
Proof usesTruncated geometric vector in \(\ell^2\) · Shifted unilateral shift has trivial kernel · Squared norm of the truncated geometric vector · Squared norm of the shifted shift on the truncated geometric vector
Used byEssential spectrum of the unilateral shift is the unit circle

TheoremEssential spectrum of the unilateral shift is the unit circle#✓fully proved

The essential spectrum of the unilateral shift is the unit circle: S - μ • 1 is Fredholm exactly off the circle.

theorem essentialSpectrum_shiftCLM :
    essentialSpectrum (LpShiftOperator.shiftCLM (𝕜 := 𝕜)) = Metric.sphere (0 : 𝕜) 1
Uses 5 · Used by 1
Statement usesThe unilateral shift operator · Essential spectrum of a bounded operator
Proof usesShifted unilateral shift is Fredholm inside the unit disk · Shifted unilateral shift is Fredholm outside the unit disk · Shifted unilateral shift is not Fredholm on the unit circle
Used byMembership in the essential spectrum of the unilateral shift

TheoremMembership in the essential spectrum of the unilateral shift#✓fully proved

Membership form: μ is in the essential spectrum of the shift iff ‖μ‖ = 1.

theorem mem_essentialSpectrum_shiftCLM {μ : 𝕜} :
    μ ∈ essentialSpectrum (LpShiftOperator.shiftCLM (𝕜 := 𝕜)) ↔ ‖μ‖ = 1
Uses 3
Statement usesThe unilateral shift operator · Essential spectrum of a bounded operator
Proof usesEssential spectrum of the unilateral shift is the unit circle

TheoremQuadratic form of the forward shift as a series#✓fully proved

The quadratic form of the forward shift as a series over consecutive coordinates: ⟪S x, x⟫ = ∑' n, conj (x n) * x (n + 1).

theorem quadForm_fwdShift_eq_tsum (x : ℓ²(ℕ, ℂ)) :
    ⟪LpShiftOperator.shiftCLM x, x⟫_ℂ = ∑' n, (starRingEnd ℂ) (x n) * x (n + 1)
Uses 1 · Used by 2
Statement usesThe unilateral shift operator
Used byForward shift's numerical range lies in the open unit disc · Forward shift quadratic form at a geometric vector

TheoremQuadratic form of the backward shift as a series#✓fully proved

The quadratic form of the backward shift as a series over consecutive coordinates: ⟪B x, x⟫ = ∑' n, conj (x (n + 1)) * x n.

theorem quadForm_bwdShift_eq_tsum (x : ℓ²(ℕ, ℂ)) :
    ⟪LpShiftOperator.backwardCLM x, x⟫_ℂ = ∑' n, (starRingEnd ℂ) (x (n + 1)) * x n
Uses 1 · Used by 2
Statement usesBackward shift
Used byBackward shift's numerical range lies in the open unit disc · Backward shift quadratic form at a geometric vector

TheoremStrict AM-GM bound on consecutive coordinates of a unit vector#✓fully proved

For a unit vector x, the sum of the products of consecutive coordinate norms is strictly less than 1: termwise AM–GM gives a bound of (1 + (1 - ‖x 0‖²)) / 2 ≤ 1, and the AM–GM inequality is strict at the coordinate supplied by exists_norm_ne_norm_succ.

theorem sum_norm_mul_succ_lt_one {x : ℓ²(ℕ, ℂ)} (hx : ‖x‖ = 1) :
    ∑' n, ‖(x : ℕ → ℂ) n‖ * ‖(x : ℕ → ℂ) (n + 1)‖ < 1
Used by 2
Used byBackward shift's numerical range lies in the open unit disc · Forward shift's numerical range lies in the open unit disc

TheoremSquare-summability of the scaled geometric sequence#✓fully proved

The geometric sequence attached to u, with coordinates √(1 - ‖u‖²) * u ^ n, is in ℓ². When ‖u‖ ≥ 1 the square root is 0 and the sequence is identically 0; the interesting case is ‖u‖ < 1.

theorem memℓp_geom (u : ℂ) :
    Memℓp (fun n => ((Real.sqrt (1 - ‖u‖ ^ 2) : ℝ) : ℂ) * u ^ n) 2
Used by 1
Used byGeometric unit vector attached to a point of the disc

DefinitionGeometric unit vector attached to a point of the disc#✓fully proved

The geometric vector attached to u: the ℓ² sequence with coordinates √(1 - ‖u‖²) * u ^ n.

noncomputable def geom (u : ℂ) : ℓ²(ℕ, ℂ) :=
  ⟨fun n => ((Real.sqrt (1 - ‖u‖ ^ 2) : ℝ) : ℂ) * u ^ n, memℓp_geom u⟩
Uses 1 · Used by 6
Statement usesSquare-summability of the scaled geometric sequence
Used byPointwise action of the geometric vector · Open unit disc lies in the backward shift's numerical range · Open unit disc lies in the forward shift's numerical range · Geometric vector of a point in the open disc is a unit vector · Backward shift quadratic form at a geometric vector · Forward shift quadratic form at a geometric vector

TheoremPointwise action of the geometric vector#✓fully proved

Pointwise action of the geometric vector.

theorem geom_apply (u : ℂ) (n : ℕ) :
    (geom u : ℕ → ℂ) n = ((Real.sqrt (1 - ‖u‖ ^ 2) : ℝ) : ℂ) * u ^ n
Uses 1
Statement usesGeometric unit vector attached to a point of the disc

TheoremGeometric vector of a point in the open disc is a unit vector#✓fully proved

The geometric vector attached to u with ‖u‖ < 1 is a unit vector.

theorem norm_geom {u : ℂ} (hu : ‖u‖ < 1) : ‖geom u‖ = 1
Uses 1 · Used by 2
Statement usesGeometric unit vector attached to a point of the disc
Used byOpen unit disc lies in the backward shift's numerical range · Open unit disc lies in the forward shift's numerical range

TheoremForward shift quadratic form at a geometric vector#✓fully proved

The quadratic form of the forward shift at the geometric vector attached to u is u itself.

theorem quadForm_fwd_geom {u : ℂ} (hu : ‖u‖ < 1) :
    ⟪LpShiftOperator.shiftCLM (geom u), geom u⟫_ℂ = u
Uses 3 · Used by 1
Statement usesThe unilateral shift operator · Geometric unit vector attached to a point of the disc
Proof usesQuadratic form of the forward shift as a series
Used byOpen unit disc lies in the forward shift's numerical range

TheoremBackward shift quadratic form at a geometric vector#✓fully proved

The quadratic form of the backward shift at the geometric vector attached to u is conj u.

theorem quadForm_bwd_geom {u : ℂ} (hu : ‖u‖ < 1) :
    ⟪LpShiftOperator.backwardCLM (geom u), geom u⟫_ℂ = (starRingEnd ℂ) u
Uses 3 · Used by 1
Statement usesBackward shift · Geometric unit vector attached to a point of the disc
Proof usesQuadratic form of the backward shift as a series
Used byOpen unit disc lies in the backward shift's numerical range

TheoremOpen unit disc lies in the forward shift's numerical range#✓fully proved

Every u with ‖u‖ < 1 lies in the numerical range of the forward shift, witnessed by the geometric vector attached to u.

theorem mem_numericalRange_fwdShift_of_norm_lt_one {u : ℂ} (hu : ‖u‖ < 1) :
    u ∈ ToeplitzHausdorffWanted.numericalRange (LpShiftOperator.shiftCLM (𝕜 := ℂ))
Uses 5 · Used by 1
Statement usesThe unilateral shift operator · Numerical range
Proof usesGeometric unit vector attached to a point of the disc · Geometric vector of a point in the open disc is a unit vector · Forward shift quadratic form at a geometric vector
Used byNumerical range of the unilateral shift is the open unit disc

TheoremOpen unit disc lies in the backward shift's numerical range#✓fully proved

Every w with ‖w‖ < 1 lies in the numerical range of the backward shift, witnessed by the geometric vector attached to conj w.

theorem mem_numericalRange_bwdShift_of_norm_lt_one {w : ℂ} (hw : ‖w‖ < 1) :
    w ∈ ToeplitzHausdorffWanted.numericalRange (LpShiftOperator.backwardCLM (𝕜 := ℂ))
Uses 5 · Used by 1
Statement usesBackward shift · Numerical range
Proof usesGeometric unit vector attached to a point of the disc · Geometric vector of a point in the open disc is a unit vector · Backward shift quadratic form at a geometric vector
Used byNumerical range of the backward shift is the open unit disc

TheoremForward shift's numerical range lies in the open unit disc#✓fully proved

Every point of the numerical range of the forward shift has norm strictly less than 1, by the AM–GM strict bound.

theorem norm_lt_one_of_mem_numericalRange_fwdShift {w : ℂ}
    (hw : w ∈ ToeplitzHausdorffWanted.numericalRange (LpShiftOperator.shiftCLM (𝕜 := ℂ))) :
    ‖w‖ < 1
Uses 5 · Used by 1
Statement usesThe unilateral shift operator · Numerical range
Proof usesQuadratic form of the forward shift as a series · Strict AM-GM bound on consecutive coordinates of a unit vector · Membership in the numerical range
Used byNumerical range of the unilateral shift is the open unit disc

TheoremBackward shift's numerical range lies in the open unit disc#✓fully proved

Every point of the numerical range of the backward shift has norm strictly less than 1, by the AM–GM strict bound.

theorem norm_lt_one_of_mem_numericalRange_bwdShift {w : ℂ}
    (hw : w ∈ ToeplitzHausdorffWanted.numericalRange (LpShiftOperator.backwardCLM (𝕜 := ℂ))) :
    ‖w‖ < 1
Uses 5 · Used by 1
Statement usesBackward shift · Numerical range
Proof usesQuadratic form of the backward shift as a series · Strict AM-GM bound on consecutive coordinates of a unit vector · Membership in the numerical range
Used byNumerical range of the backward shift is the open unit disc

TheoremNumerical range of the unilateral shift is the open unit disc#✓fully proved

The numerical range of the unilateral shift on ℓ²(ℕ, ℂ) is the open unit disc.

theorem numericalRange_fwdShiftCLM :
    ToeplitzHausdorffWanted.numericalRange
      (LpShiftOperator.shiftCLM (𝕜 := ℂ)) = Metric.ball (0 : ℂ) 1
Uses 4
Statement usesThe unilateral shift operator · Numerical range
Proof usesOpen unit disc lies in the forward shift's numerical range · Forward shift's numerical range lies in the open unit disc

TheoremNumerical range of the backward shift is the open unit disc#✓fully proved

The numerical range of the backward shift on ℓ²(ℕ, ℂ) is the open unit disc.

theorem numericalRange_bwdShiftCLM :
    ToeplitzHausdorffWanted.numericalRange
      (LpShiftOperator.backwardCLM (𝕜 := ℂ)) = Metric.ball (0 : ℂ) 1
Uses 4
Statement usesBackward shift · Numerical range
Proof usesOpen unit disc lies in the backward shift's numerical range · Backward shift's numerical range lies in the open unit disc

DefinitionUnilateral shift operator#✓fully proved

A bounded linear operator \(T\) on a complex inner product space \(H\) is a unilateral shift if there is a Hilbert basis \((b_n)_{n \in \mathbb{N}}\) of \(H\) such that \(T b_n = b_{n+1}\) for every \(n \in \mathbb{N}\).

def IsShift
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    (T : H →L[ℂ] H) : Prop :=
  ∃ b : HilbertBasis ℕ ℂ H, ∀ n : ℕ, T (b n) = b (n + 1)
Used by 1
Used byIsometric characterization of the unilateral shift

TheoremIsometric characterization of the unilateral shift#●ready to prove

Let \(H\) be a separable complex Hilbert space, and call a bounded linear operator \(T : H \to H\) a shift if there is an orthonormal basis \((e_n)_{n \in \mathbb{N}}\) of \(H\) with \(T e_n = e_{n+1}\) for every \(n \in \mathbb{N}\). Then a bounded linear operator \(T : H \to H\) is a shift if and only if the following three conditions hold: \(T\) is an isometry, that is, \(\langle T x, T y \rangle = \langle x, y \rangle\) for all \(x, y \in H\); the ranges of the powers of \(T\) satisfy \(\bigcap_{n \ge 1} \mathrm{Ran}(T^n) = \{0\}\); and the orthogonal complement \((\mathrm{Ran}\, T)^\perp\) of the range of \(T\) has dimension \(1\).

public theorem_wanted isShift_iff_isometry_iInf_range_pow_eq_bot_finrank_orthogonal_eq_one
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [TopologicalSpace.SeparableSpace H]
    (T : H →L[ℂ] H) :
    IsShift T ↔
      (∀ x y : H, inner ℂ (T x) (T y) = inner ℂ x y) ∧
        (⨅ n : ℕ, LinearMap.range (T.toLinearMap ^ (n + 1))) = ⊥ ∧
        Module.rank ℂ (T.rangeᗮ) = 1
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; Special classes of linear operators), problem ma_proofbench_l2_33.
Uses 1
Statement usesUnilateral shift operator
107 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.