Bilateral shift

DefinitionBilateral shift of a sequence#✓fully proved

For a function \(x : \mathbb{Z} \to K\) with values in any set \(K\), the bilateral (forward) shift of \(x\) is the function \(Sx : \mathbb{Z} \to K\) given by \((Sx)(n) = x(n - 1)\).

def bilateralShiftFun (x : ℤ → 𝕜) (n : ℤ) : 𝕜 := x (n - 1)

Used by 2

Used byBilateral shift operator · Bilateral shift as a linear map

DefinitionBilateral backward shift of a sequence#✓fully proved

For a function \(x : \mathbb{Z} \to K\) with values in any set \(K\), the bilateral backward shift of \(x\) is the function \(Bx : \mathbb{Z} \to K\) given by \((Bx)(n) = x(n + 1)\).

def bilateralBackwardFun (x : ℤ → 𝕜) (n : ℤ) : 𝕜 := x (n + 1)

Used by 4

Used byBilateral backward shift operator · Bilateral backward shift as a linear map · Spectrum of the bilateral backward shift · Spectrum of the bilateral shift

DefinitionBilateral shift as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\ell^2(\mathbb{Z}, \mathbb{K})\) be the space of square-summable functions \(\mathbb{Z} \to \mathbb{K}\). The bilateral shift is the \(\mathbb{K}\)-linear map \(S : \ell^2(\mathbb{Z}, \mathbb{K}) \to \ell^2(\mathbb{Z}, \mathbb{K})\) given by \((Sx)(n) = x(n - 1)\) for all \(n \in \mathbb{Z}\).

noncomputable def bilateralShiftLinMap : ℓ²(ℤ, 𝕜) →ₗ[𝕜] ℓ²(ℤ, 𝕜) where
  toFun x := ⟨bilateralShiftFun (x : ℤ → 𝕜), memℓp_bilateralShiftFun⟩
  map_add' x y := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_add, bilateralShiftFun_apply, Pi.add_apply]
  map_smul' c x := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_smul, bilateralShiftFun_apply, Pi.smul_apply, smul_eq_mul,
      RingHom.id_apply]

Uses 1 · Used by 1

Statement usesBilateral shift of a sequence

Used byBilateral shift operator

DefinitionBilateral backward shift as a linear map#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\ell^2(\mathbb{Z}, \mathbb{K})\) be the space of square-summable functions \(\mathbb{Z} \to \mathbb{K}\). The bilateral backward shift is the \(\mathbb{K}\)-linear map \(B : \ell^2(\mathbb{Z}, \mathbb{K}) \to \ell^2(\mathbb{Z}, \mathbb{K})\) given by \((Bx)(n) = x(n + 1)\) for all \(n \in \mathbb{Z}\).

noncomputable def bilateralBackwardLinMap : ℓ²(ℤ, 𝕜) →ₗ[𝕜] ℓ²(ℤ, 𝕜) where
  toFun x := ⟨bilateralBackwardFun (x : ℤ → 𝕜), memℓp_bilateralBackwardFun⟩
  map_add' x y := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_add, bilateralBackwardFun_apply, Pi.add_apply]
  map_smul' c x := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_smul, bilateralBackwardFun_apply, Pi.smul_apply, smul_eq_mul,
      RingHom.id_apply]

Uses 1 · Used by 1

Statement usesBilateral backward shift of a sequence

Used byBilateral backward shift operator

DefinitionBilateral shift operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\ell^2(\mathbb{Z}, \mathbb{K})\) be the Hilbert space of square-summable functions \(\mathbb{Z} \to \mathbb{K}\). The bilateral shift is the bounded \(\mathbb{K}\)-linear operator \(S\) on \(\ell^2(\mathbb{Z}, \mathbb{K})\) given by \((Sx)(n) = x(n - 1)\) for all \(n \in \mathbb{Z}\).

noncomputable def bilateralShiftCLM : ℓ²(ℤ, 𝕜) →L[𝕜] ℓ²(ℤ, 𝕜) :=
  bilateralShiftLinMap.mkContinuous 1 (fun x => by
    rw [one_mul]
    exact le_of_eq (norm_bilateralShiftLinMap_apply x))

Uses 2 · Used by 5

Statement usesBilateral shift of a sequence · Bilateral shift as a linear map

Used byEvery point of the unit circle lies in the spectrum of the bilateral shift · Residual of the truncated approximate eigenvector · Coordinates of the residual of the truncated approximate eigenvector · Spectrum of the bilateral backward shift · Spectrum of the bilateral shift

DefinitionBilateral backward shift operator#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(\ell^2(\mathbb{Z}, \mathbb{K})\) be the Hilbert space of square-summable functions \(\mathbb{Z} \to \mathbb{K}\). The bilateral backward shift is the bounded \(\mathbb{K}\)-linear operator \(B\) on \(\ell^2(\mathbb{Z}, \mathbb{K})\) given by \((Bx)(n) = x(n + 1)\) for all \(n \in \mathbb{Z}\).

noncomputable def bilateralBackwardCLM : ℓ²(ℤ, 𝕜) →L[𝕜] ℓ²(ℤ, 𝕜) :=
  bilateralBackwardLinMap.mkContinuous 1 (fun x => by
    rw [one_mul]
    exact le_of_eq (norm_bilateralBackwardLinMap_apply x))

Uses 2 · Used by 2

Statement usesBilateral backward shift of a sequence · Bilateral backward shift as a linear map

Used bySpectrum of the bilateral backward shift · Spectrum of the bilateral shift

TheoremA unit scalar times its conjugate is one#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). If \(\mu \in \mathbb{K}\) satisfies \(|\mu| = 1\), then \(\mu \bar{\mu} = 1\), where \(\bar{\mu}\) is the complex conjugate of \(\mu\).

theorem mul_star_eq_one_of_norm_eq_one {μ : 𝕜} (hμ : ‖μ‖ = 1) : μ * star μ = 1

Used by 1

Used byMultiplying a power of the conjugate by a unit scalar

TheoremConjugates of unimodular scalars are nonzero#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). If \(\mu \in \mathbb{K}\) satisfies \(|\mu| = 1\), then its conjugate \(\bar{\mu}\) is nonzero.

theorem star_ne_zero_of_norm_eq_one {μ : 𝕜} (hμ : ‖μ‖ = 1) : star μ ≠ 0

Used by 1

Used byMultiplying a power of the conjugate by a unit scalar

TheoremMultiplying a power of the conjugate by a unit scalar#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), and write \(\bar{\mu}\) for the complex conjugate of \(\mu \in \mathbb{K}\). If \(|\mu| = 1\), then for every integer \(n\), \(\mu \bar{\mu}^{\,n} = \bar{\mu}^{\,n-1}\).

theorem mul_star_zpow {μ : 𝕜} (hμ : ‖μ‖ = 1) (n : ℤ) :
    μ * (star μ) ^ n = (star μ) ^ (n - 1)

Uses 2 · Used by 1

Proof usesA unit scalar times its conjugate is one · Conjugates of unimodular scalars are nonzero

Used byResidual of the truncated approximate eigenvector

DefinitionTruncated approximate eigenfunction of the bilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\mu \in \mathbb{K}\) and \(N \in \mathbb{N}\), and write \(\bar{\mu}\) for the complex conjugate of \(\mu\). This is the function \(f_{\mu,N} : \mathbb{Z} \to \mathbb{K}\) with \(f_{\mu,N}(n) = \bar{\mu}^{\,n}\) for \(-N \le n \le N\) and \(f_{\mu,N}(n) = 0\) otherwise (negative powers are inverses, with the convention \(0^{n} = 0\) for \(n < 0\)).

It is used for \(\mu\) on the unit circle, where it gives approximate eigenvectors of the bilateral shift.

def approxEigenFun (μ : 𝕜) (N : ℕ) (n : ℤ) : 𝕜 :=
  if n ∈ Finset.Icc (-(N : ℤ)) (N : ℤ) then (star μ) ^ n else 0

Used by 4

Used byTruncated approximate eigenvector of the bilateral shift · Norm of the truncated approximate eigenvector · Residual of the truncated approximate eigenvector · Coordinates of the residual of the truncated approximate eigenvector

DefinitionTruncated approximate eigenvector of the bilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\mu \in \mathbb{K}\) and \(N \in \mathbb{N}\), and write \(\bar{\mu}\) for the complex conjugate of \(\mu\). This is the vector \(v_{\mu,N} \in \ell^2(\mathbb{Z}, \mathbb{K})\) whose \(n\)-th coordinate is the truncated approximate eigenfunction \(f_{\mu,N}(n)\), that is, \(\bar{\mu}^{\,n}\) for \(-N \le n \le N\) and \(0\) otherwise; it lies in \(\ell^2\) because it has finite support.

It is used for \(\mu\) on the unit circle, where it is an approximate eigenvector of the bilateral shift.

noncomputable def approxEigenVec (μ : 𝕜) (N : ℕ) : ℓ²(ℤ, 𝕜) :=
  ⟨approxEigenFun μ N, memℓp_approxEigenFun N⟩

Uses 1 · Used by 4

Statement usesTruncated approximate eigenfunction of the bilateral shift

Used byEvery point of the unit circle lies in the spectrum of the bilateral shift · Norm of the truncated approximate eigenvector · Residual of the truncated approximate eigenvector · Coordinates of the residual of the truncated approximate eigenvector

TheoremNorm of the truncated approximate eigenvector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(\mu \in \mathbb{K}\) with \(|\mu| = 1\), and let \(N \in \mathbb{N}\). The truncated approximate eigenvector \(v_{\mu,N} \in \ell^2(\mathbb{Z}, \mathbb{K})\), whose \(n\)-th coordinate is \(\bar{\mu}^{\,n}\) for \(-N \le n \le N\) and \(0\) otherwise (\(\bar{\mu}\) the complex conjugate of \(\mu\)), satisfies \(\|v_{\mu,N}\|^2 = 2N + 1\).

theorem norm_sq_approxEigenVec {μ : 𝕜} (hμ : ‖μ‖ = 1) (N : ℕ) :
    ‖approxEigenVec μ N‖ ^ 2 = 2 * (N : ℝ) + 1

Uses 2 · Used by 1

Statement usesTruncated approximate eigenvector of the bilateral shift

Proof usesTruncated approximate eigenfunction of the bilateral shift

Used byEvery point of the unit circle lies in the spectrum of the bilateral shift

TheoremApplying \(\mu I - T\) on \(\ell^2(\mathbb{Z})\)#✓fully proved

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

theorem algebraMap_sub_apply (T : ℓ²(ℤ, 𝕜) →L[𝕜] ℓ²(ℤ, 𝕜)) (μ : 𝕜)
    (x : ℓ²(ℤ, 𝕜)) :
    (algebraMap 𝕜 (ℓ²(ℤ, 𝕜) →L[𝕜] ℓ²(ℤ, 𝕜)) μ - T) x = μ • x - T x

Used by 1

Used byCoordinates of the residual of the truncated approximate eigenvector

TheoremCoordinates of the residual of the truncated approximate eigenvector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be the bilateral shift on \(\ell^2(\mathbb{Z}, \mathbb{K})\), and let \(\mu \in \mathbb{K}\), \(N \in \mathbb{N}\) and \(n \in \mathbb{Z}\). Let \(f_{\mu,N}\) be the truncated approximate eigenfunction and \(v_{\mu,N} \in \ell^2(\mathbb{Z}, \mathbb{K})\) the corresponding truncated approximate eigenvector. Then the \(n\)-th coordinate of \((\mu I - S)v_{\mu,N}\) is \(\mu f_{\mu,N}(n) - f_{\mu,N}(n - 1)\), where \(\mu I\) is \(\mu\) times the identity operator.

theorem residual_apply {μ : 𝕜} (N : ℕ) (n : ℤ) :
    ((algebraMap 𝕜 (ℓ²(ℤ, 𝕜) →L[𝕜] ℓ²(ℤ, 𝕜)) μ - bilateralShiftCLM (𝕜 := 𝕜))
        (approxEigenVec μ N)) n =
      μ * approxEigenFun μ N n - approxEigenFun μ N (n - 1)

Uses 4 · Used by 1

Statement usesBilateral shift operator · Truncated approximate eigenfunction of the bilateral shift · Truncated approximate eigenvector of the bilateral shift

Proof usesApplying \(\mu I - T\) on \(\ell^2(\mathbb{Z})\)

Used byResidual of the truncated approximate eigenvector

TheoremResidual of the truncated approximate eigenvector#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(S\) be the bilateral shift on \(\ell^2(\mathbb{Z}, \mathbb{K})\), let \(\mu \in \mathbb{K}\) with \(|\mu| = 1\), and let \(N \in \mathbb{N}\). The truncated approximate eigenvector \(v_{\mu,N}\) satisfies \(\|(\mu I - S)v_{\mu,N}\|^2 = 2\), where \(\mu I\) is \(\mu\) times the identity operator.

The only nonzero coordinates of \((\mu I - S)v_{\mu,N}\) are those at \(n = -N\) and \(n = N + 1\), each of absolute value \(1\).

theorem norm_sq_residual_approxEigenVec {μ : 𝕜} (hμ : ‖μ‖ = 1) (N : ℕ) :
    ‖(algebraMap 𝕜 (ℓ²(ℤ, 𝕜) →L[𝕜] ℓ²(ℤ, 𝕜)) μ - bilateralShiftCLM (𝕜 := 𝕜))
        (approxEigenVec μ N)‖ ^ 2 = 2

Uses 5 · Used by 1

Statement usesBilateral shift operator · Truncated approximate eigenvector of the bilateral shift

Proof usesTruncated approximate eigenfunction of the bilateral shift · Multiplying a power of the conjugate by a unit scalar · Coordinates of the residual of the truncated approximate eigenvector

Used byEvery point of the unit circle lies in the spectrum of the bilateral shift

TheoremEvery point of the unit circle lies in the spectrum of the bilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(S\) be the bilateral shift on \(\ell^2(\mathbb{Z}, \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{Z}, \mathbb{K})\), that is, \(\mu I - S\) is not invertible there, where \(\mu I\) is \(\mu\) times the identity operator.

If \(\mu I - S\) were invertible it would be bounded below, but the truncated approximate eigenvectors \(v_{\mu,N}\) satisfy \(\|v_{\mu,N}\| = \sqrt{2N + 1}\) and \(\|(\mu I - S)v_{\mu,N}\| = \sqrt{2}\) for every \(N \in \mathbb{N}\).

theorem mem_spectrum_bilateralShiftCLM_of_norm_eq_one {μ : 𝕜} (hμ : ‖μ‖ = 1) :
    μ ∈ spectrum 𝕜 (bilateralShiftCLM (𝕜 := 𝕜))

Uses 4 · Used by 1

Statement usesBilateral shift operator

Proof usesTruncated approximate eigenvector of the bilateral shift · Norm of the truncated approximate eigenvector · Residual of the truncated approximate eigenvector

Used bySpectrum of the bilateral shift

TheoremSpectrum of the bilateral shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\). The spectrum of the bilateral shift, as a bounded operator on \(\ell^2(\mathbb{Z}, \mathbb{K})\), is the set of scalars \(\mu \in \mathbb{K}\) with \(|\mu| = 1\); for \(\mathbb{K} = \mathbb{C}\) this is the unit circle.

theorem spectrum_bilateralShiftCLM :
    spectrum 𝕜 (bilateralShiftCLM (𝕜 := 𝕜)) = Metric.sphere 0 1

Uses 4 · Used by 1

Statement usesBilateral shift operator

Proof usesBilateral backward shift operator · Bilateral backward shift of a sequence · Every point of the unit circle lies in the spectrum of the bilateral shift

Used bySpectrum of the bilateral backward shift

TheoremSpectrum of the bilateral backward shift#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(B\) be the bilateral backward shift on \(\ell^2(\mathbb{Z}, \mathbb{K})\). The spectrum of \(B\) in the algebra of bounded operators on \(\ell^2(\mathbb{Z}, \mathbb{K})\) is the unit circle \(\{\mu \in \mathbb{K} : |\mu| = 1\}\).

theorem spectrum_bilateralBackwardCLM :
    spectrum 𝕜 (bilateralBackwardCLM (𝕜 := 𝕜)) = Metric.sphere 0 1

Uses 4

Statement usesBilateral backward shift operator

Proof usesBilateral backward shift of a sequence · Bilateral shift operator · Spectrum of the bilateral shift

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.