Toeplitz operators

DefinitionDiagonal slice function of a Toeplitz matrix#✓fully proved

The k-th diagonal slice function: shift coordinates by k, killing the coordinates that fall off the end. For k ≥ 0 this is the k-fold forward shift; for k < 0 it is the (-k)-fold backward shift.

def toeplitzSliceFun (k : ℤ) (x : ℕ → 𝕜) (i : ℕ) : 𝕜 :=
  if k ≤ (i : ℤ) then x (((i : ℤ) - k).toNat) else 0

Used by 8

Used byDiagonal slices do not increase norms · Diagonal slices preserve square-summability · Pointwise action of a Toeplitz operator · Pointwise action of the diagonal slice operator · Diagonal slices are powers of the forward or backward shift · Inner product symmetry of opposite diagonal slices · Diagonal slice as a linear map · Pointwise action of the diagonal slice linear map

TheoremDiagonal slices preserve square-summability#✓fully proved

The slice of an ℓ² sequence is in ℓ².

theorem toeplitz_memℓp_sliceFun {k : ℤ} {x : ℓ²(ℕ, 𝕜)} :
    Memℓp (toeplitzSliceFun k (x : ℕ → 𝕜)) 2

Uses 1 · Used by 1

Statement usesDiagonal slice function of a Toeplitz matrix

Used byDiagonal slice as a linear map

DefinitionDiagonal slice as a linear map#✓fully proved

The k-th diagonal slice as a linear map.

noncomputable def toeplitzSliceLinMap (k : ℤ) : ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨toeplitzSliceFun k (x : ℕ → 𝕜), toeplitz_memℓp_sliceFun⟩
  map_add' x y := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_add, Pi.add_apply, toeplitzSliceFun_apply]
    split_ifs with hi <;> simp
  map_smul' c x := by
    apply lp.ext
    funext i
    simp only [lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, toeplitzSliceFun_apply,
      RingHom.id_apply]
    split_ifs with hi <;> simp

Uses 2 · Used by 3

Statement usesDiagonal slice function of a Toeplitz matrix · Diagonal slices preserve square-summability

Used byDiagonal slices do not increase norms · Diagonal slice as a bounded operator · Pointwise action of the diagonal slice linear map

TheoremPointwise action of the diagonal slice linear map#✓fully proved

Pointwise action of the slice linear map.

theorem toeplitzSliceLinMap_apply (k : ℤ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    toeplitzSliceLinMap k x i = toeplitzSliceFun k (x : ℕ → 𝕜) i

Uses 2

Statement usesDiagonal slice function of a Toeplitz matrix · Diagonal slice as a linear map

TheoremDiagonal slices do not increase norms#✓fully proved

A slice does not increase norms.

theorem norm_toeplitzSliceLinMap_apply_le (k : ℤ) (x : ℓ²(ℕ, 𝕜)) :
    ‖toeplitzSliceLinMap k x‖ ≤ ‖x‖

Uses 2 · Used by 2

Statement usesDiagonal slice as a linear map

Proof usesDiagonal slice function of a Toeplitz matrix

Used byOperator norm of a diagonal slice is at most one · Diagonal slice as a bounded operator

DefinitionDiagonal slice as a bounded operator#✓fully proved

The k-th diagonal slice as a bounded operator.

noncomputable def toeplitzSlice (k : ℤ) : ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  (toeplitzSliceLinMap k).mkContinuous 1 (fun x => by
    rw [one_mul]
    exact norm_toeplitzSliceLinMap_apply_le k x)

Uses 2 · Used by 13

Statement usesDiagonal slices do not increase norms · Diagonal slice as a linear map

Used byAdjoint of a Toeplitz operator · Adjoint of a diagonal slice is the opposite slice · Operator norm bound for a Toeplitz operator · Operator norm of a diagonal slice is at most one · Toeplitz operator as the sum of its diagonal slices · Toeplitz operator with absolutely summable symbol · Pointwise action of a Toeplitz operator · Toeplitz operator of a delta symbol is a scaled slice · Toeplitz operator of the zero symbol · Pointwise action of the diagonal slice operator · Diagonal slices are powers of the forward or backward shift · Inner product symmetry of opposite diagonal slices · Summability of weighted diagonal slices

TheoremPointwise action of the diagonal slice operator#✓fully proved

Pointwise action of the slice operator.

theorem toeplitzSlice_apply (k : ℤ) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    toeplitzSlice k x i = toeplitzSliceFun k (x : ℕ → 𝕜) i

Uses 2 · Used by 2

Statement usesDiagonal slice as a bounded operator · Diagonal slice function of a Toeplitz matrix

Used byDiagonal slices are powers of the forward or backward shift · Inner product symmetry of opposite diagonal slices

TheoremDiagonal slices are powers of the forward or backward shift#✓fully proved

Every nonnegative Toeplitz slice is the corresponding power of the canonical unilateral shift, and every negative slice is the corresponding power of the canonical backward shift.

theorem toeplitzSlice_eq_shiftCLM_pow_or_backwardCLM_pow (k : ℤ) :
    toeplitzSlice (𝕜 := 𝕜) k = if 0 ≤ k then
      LpShiftOperator.shiftCLM ^ k.toNat
    else LpShiftOperator.backwardCLM ^ (-k).toNat

Uses 7

Statement usesBackward shift · The unilateral shift operator · Diagonal slice as a bounded operator

Proof usesPointwise action of a power of the backward shift · Pointwise action of a power of the unilateral shift · Diagonal slice function of a Toeplitz matrix · Pointwise action of the diagonal slice operator

TheoremOperator norm of a diagonal slice is at most one#✓fully proved

The operator norm of a slice is at most 1.

theorem norm_toeplitzSlice_le (k : ℤ) : ‖toeplitzSlice (𝕜 := 𝕜) k‖ ≤ 1

Uses 2 · Used by 3

Statement usesDiagonal slice as a bounded operator

Proof usesDiagonal slices do not increase norms

Used byOperator norm bound for a Toeplitz operator · Pointwise action of a Toeplitz operator · Summability of weighted diagonal slices

TheoremInner product symmetry of opposite diagonal slices#✓fully proved

A slice is adjoint to the slice at the negated index: the diagonal symmetry exchanges the two sides of the inner product.

theorem toeplitzSlice_inner_symm (k : ℤ) (x y : ℓ²(ℕ, 𝕜)) :
    ⟪toeplitzSlice k x, y⟫_𝕜 = ⟪x, toeplitzSlice (-k) y⟫_𝕜

Uses 3 · Used by 1

Statement usesDiagonal slice as a bounded operator

Proof usesDiagonal slice function of a Toeplitz matrix · Pointwise action of the diagonal slice operator

Used byAdjoint of a diagonal slice is the opposite slice

TheoremAdjoint of a diagonal slice is the opposite slice#✓fully proved

A slice is adjoint to the slice at the negated index.

theorem adjoint_toeplitzSlice (k : ℤ) :
    (toeplitzSlice (𝕜 := 𝕜) k)† = toeplitzSlice (𝕜 := 𝕜) (-k)

Uses 2 · Used by 1

Statement usesDiagonal slice as a bounded operator

Proof usesInner product symmetry of opposite diagonal slices

Used byAdjoint of a Toeplitz operator

TheoremSummability of weighted diagonal slices#✓fully proved

The slice operators weighted by a are summable in operator norm when a is absolutely summable.

theorem toeplitz_summable_slices {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    Summable fun k => (a k) • toeplitzSlice (𝕜 := 𝕜) k

Uses 2 · Used by 1

Statement usesDiagonal slice as a bounded operator

Proof usesOperator norm of a diagonal slice is at most one

Used byToeplitz operator as the sum of its diagonal slices

DefinitionToeplitz operator with absolutely summable symbol#✓fully proved

The Toeplitz operator with symbol a. Defined as the norm-convergent series ∑' k, a k • toeplitzSlice k over the diagonal slices.

noncomputable def toeplitzOperator (a : ℤ → 𝕜) (_ha : Summable fun k => ‖a k‖) :
    ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  ∑' k, (a k) • toeplitzSlice (𝕜 := 𝕜) k

Uses 1 · Used by 12

Statement usesDiagonal slice as a bounded operator

Used byAdjoint of a Toeplitz operator · A Toeplitz operator is compact iff its symbol is zero · Characterization of self-adjoint Toeplitz operators · Toeplitz operators with self-adjoint symbol are self-adjoint · Operator norm of a Toeplitz operator with delta symbol · Operator norm bound for a Toeplitz operator · Toeplitz operators with nonzero symbol are not compact · Toeplitz operator as the sum of its diagonal slices · Pointwise action of a Toeplitz operator · Toeplitz operator applied to a standard basis vector · Toeplitz operator of a delta symbol is a scaled slice · Toeplitz operator of the zero symbol

TheoremToeplitz operator as the sum of its diagonal slices#✓fully proved

The Toeplitz operator is the sum of its slices.

theorem toeplitz_hasSum_slices {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    HasSum (fun k => (a k) • toeplitzSlice (𝕜 := 𝕜) k) (toeplitzOperator a ha)

Uses 3 · Used by 3

Statement usesToeplitz operator with absolutely summable symbol · Diagonal slice as a bounded operator

Proof usesSummability of weighted diagonal slices

Used byAdjoint of a Toeplitz operator · Operator norm bound for a Toeplitz operator · Pointwise action of a Toeplitz operator

TheoremPointwise action of a Toeplitz operator#✓fully proved

Pointwise action of the Toeplitz operator: (Tₐ x) i = ∑' j, a (i - j) * x j.

theorem toeplitzOperator_apply {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖)
    (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    toeplitzOperator a ha x i = ∑' j : ℕ, a ((i : ℤ) - (j : ℤ)) * x j

Uses 5 · Used by 2

Statement usesToeplitz operator with absolutely summable symbol

Proof usesOperator norm of a diagonal slice is at most one · Diagonal slice as a bounded operator · Diagonal slice function of a Toeplitz matrix · Toeplitz operator as the sum of its diagonal slices

Used byCharacterization of self-adjoint Toeplitz operators · Toeplitz operator applied to a standard basis vector

TheoremToeplitz operator of the zero symbol#✓fully proved

The zero symbol gives the zero operator.

theorem toeplitzOperator_zero : toeplitzOperator (0 : ℤ → 𝕜) (by simp) = 0

Uses 2 · Used by 1

Statement usesToeplitz operator with absolutely summable symbol

Proof usesDiagonal slice as a bounded operator

Used byA Toeplitz operator is compact iff its symbol is zero

TheoremOperator norm bound for a Toeplitz operator#✓fully proved

Operator-norm bound: ‖Tₐ‖ ≤ ∑' k, ‖a k‖.

theorem norm_toeplitzOperator_le {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    ‖toeplitzOperator a ha‖ ≤ ∑' k, ‖a k‖

Uses 4 · Used by 1

Statement usesToeplitz operator with absolutely summable symbol

Proof usesOperator norm of a diagonal slice is at most one · Diagonal slice as a bounded operator · Toeplitz operator as the sum of its diagonal slices

Used byOperator norm of a Toeplitz operator with delta symbol

DefinitionAdjoint symbol of a Toeplitz operator#✓fully proved

The adjoint symbol: a* k = star (a (-k)).

def toeplitzAdjointSymbol (a : ℤ → 𝕜) : ℤ → 𝕜 := fun k => star (a (-k))

Used by 3

Used byAdjoint of a Toeplitz operator · Characterization of self-adjoint Toeplitz operators · Absolute summability of the adjoint symbol

TheoremAbsolute summability of the adjoint symbol#✓fully proved

The adjoint symbol of an absolutely summable symbol is absolutely summable.

theorem summable_norm_toeplitzAdjointSymbol {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    Summable fun k => ‖toeplitzAdjointSymbol a k‖

Uses 1 · Used by 2

Statement usesAdjoint symbol of a Toeplitz operator

Used byAdjoint of a Toeplitz operator · Characterization of self-adjoint Toeplitz operators

TheoremAdjoint of a Toeplitz operator#✓fully proved

Adjoint of a Toeplitz operator: (Tₐ)† = T_{a*}.

theorem adjoint_toeplitzOperator {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    (toeplitzOperator (𝕜 := 𝕜) a ha)† =
      toeplitzOperator (toeplitzAdjointSymbol a)
        (summable_norm_toeplitzAdjointSymbol ha)

Uses 6 · Used by 1

Statement usesAbsolute summability of the adjoint symbol · Adjoint symbol of a Toeplitz operator · Toeplitz operator with absolutely summable symbol

Proof usesAdjoint of a diagonal slice is the opposite slice · Diagonal slice as a bounded operator · Toeplitz operator as the sum of its diagonal slices

Used byCharacterization of self-adjoint Toeplitz operators

TheoremToeplitz operator applied to a standard basis vector#✓fully proved

The Toeplitz operator applied to a standard basis vector.

theorem toeplitzOperator_apply_single {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖)
    (j i : ℕ) :
    toeplitzOperator a ha (lp.single 2 j (1 : 𝕜)) i = a ((i : ℤ) - (j : ℤ))

Uses 2 · Used by 3

Statement usesToeplitz operator with absolutely summable symbol

Proof usesPointwise action of a Toeplitz operator

Used byCharacterization of self-adjoint Toeplitz operators · Operator norm of a Toeplitz operator with delta symbol · Toeplitz operators with nonzero symbol are not compact

TheoremCharacterization of self-adjoint Toeplitz operators#✓fully proved

Self-adjointness of a Toeplitz operator iff the symbol satisfies star (a (-k)) = a k for all k.

theorem isSelfAdjoint_toeplitzOperator_iff {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    IsSelfAdjoint (toeplitzOperator a ha) ↔ ∀ k : ℤ, star (a (-k)) = a k

Uses 6 · Used by 1

Statement usesToeplitz operator with absolutely summable symbol

Proof usesAdjoint of a Toeplitz operator · Absolute summability of the adjoint symbol · Adjoint symbol of a Toeplitz operator · Pointwise action of a Toeplitz operator · Toeplitz operator applied to a standard basis vector

Used byToeplitz operators with self-adjoint symbol are self-adjoint

TheoremToeplitz operators with self-adjoint symbol are self-adjoint#✓fully proved

A Toeplitz operator with a star-fixed adjoint symbol is self-adjoint.

theorem isSelfAdjoint_toeplitzOperator_of_forall_star {a : ℤ → 𝕜}
    (ha : Summable fun k => ‖a k‖) (hstar : ∀ k, star (a (-k)) = a k) :
    IsSelfAdjoint (toeplitzOperator a ha)

Uses 2

Statement usesToeplitz operator with absolutely summable symbol

Proof usesCharacterization of self-adjoint Toeplitz operators

TheoremToeplitz operators with nonzero symbol are not compact#✓fully proved

A Toeplitz operator with a nonzero symbol is not compact: the images of the standard basis vectors converge coordinatewise to 0 but keep a nonzero coordinate.

theorem not_isCompactOperator_toeplitzOperator_of_ne {a : ℤ → 𝕜}
    (ha : Summable fun k => ‖a k‖) {k₀ : ℤ} (hk₀ : a k₀ ≠ 0) :
    ¬ IsCompactOperator (toeplitzOperator a ha)

Uses 2 · Used by 1

Statement usesToeplitz operator with absolutely summable symbol

Proof usesToeplitz operator applied to a standard basis vector

Used byA Toeplitz operator is compact iff its symbol is zero

TheoremA Toeplitz operator is compact iff its symbol is zero#✓fully proved

A Toeplitz operator is compact iff its symbol is zero.

theorem isCompactOperator_toeplitzOperator_iff {a : ℤ → 𝕜} (ha : Summable fun k => ‖a k‖) :
    IsCompactOperator (toeplitzOperator a ha) ↔ a = 0

Uses 3

Statement usesToeplitz operator with absolutely summable symbol

Proof usesToeplitz operators with nonzero symbol are not compact · Toeplitz operator of the zero symbol

DefinitionDelta symbol for Toeplitz operators#✓fully proved

The delta symbol at m with value c.

def toeplitzDelta (m : ℤ) (c : 𝕜) : ℤ → 𝕜 := fun k => if k = m then c else 0

Used by 4

Used byOperator norm of a Toeplitz operator with delta symbol · Absolute summability of a delta symbol · Toeplitz operator of a delta symbol is a scaled slice · \(\ell^1\) norm of a delta symbol

TheoremAbsolute summability of a delta symbol#✓fully proved

A delta symbol is absolutely summable.

theorem summable_norm_toeplitzDelta (m : ℤ) (c : 𝕜) :
    Summable fun k => ‖toeplitzDelta m c k‖

Uses 1 · Used by 2

Statement usesDelta symbol for Toeplitz operators

Used byOperator norm of a Toeplitz operator with delta symbol · Toeplitz operator of a delta symbol is a scaled slice

TheoremToeplitz operator of a delta symbol is a scaled slice#✓fully proved

A Toeplitz operator with a delta symbol is the corresponding scalar multiple of its diagonal slice.

theorem toeplitzOperator_delta_eq_smul_slice (m : ℤ) (c : 𝕜) :
    toeplitzOperator (toeplitzDelta m c) (summable_norm_toeplitzDelta m c) =
      c • toeplitzSlice (𝕜 := 𝕜) m

Uses 4

Statement usesAbsolute summability of a delta symbol · Delta symbol for Toeplitz operators · Toeplitz operator with absolutely summable symbol · Diagonal slice as a bounded operator

Theorem\(\ell^1\) norm of a delta symbol#✓fully proved

The ℓ¹ norm of a delta symbol is ‖c‖.

theorem tsum_norm_toeplitzDelta (m : ℤ) (c : 𝕜) :
    ∑' k, ‖toeplitzDelta m c k‖ = ‖c‖

Uses 1 · Used by 1

Statement usesDelta symbol for Toeplitz operators

Used byOperator norm of a Toeplitz operator with delta symbol

TheoremOperator norm of a Toeplitz operator with delta symbol#✓fully proved

The operator norm of a Toeplitz operator with a delta symbol is ‖c‖.

theorem norm_toeplitzOperator_delta (m : ℤ) (c : 𝕜) :
    ‖toeplitzOperator (toeplitzDelta m c) (summable_norm_toeplitzDelta m c)‖ = ‖c‖

Uses 6

Statement usesAbsolute summability of a delta symbol · Delta symbol for Toeplitz operators · Toeplitz operator with absolutely summable symbol

Proof usesOperator norm bound for a Toeplitz operator · Toeplitz operator applied to a standard basis vector · \(\ell^1\) norm of a delta symbol

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.