Toeplitz operators on boundary Hardy space

For an essentially bounded symbol a on UnitAddCircle, the Toeplitz operator T_a is the compression P M_a |H² of the multiplication operator M_a on circle L² to the boundary Hardy space H², where P is the orthogonal projection onto H². This file bundles the symbol map a ↦ T_a as a bounded complex-linear map TauCeti.toeplitz and proves its basic properties:

• TauCeti.toeplitz_apply_eq_zero_iff: T_a f = 0 exactly when a f lies in the orthogonal complement of Hardy space;
• TauCeti.inner_hardyBasis_toeplitz_hardyBasis: in the Hardy basis e₀, e₁, … the matrix entry (i, j) of T_a is the Fourier coefficient â(i - j);
• TauCeti.adjoint_toeplitz: the adjoint of T_a is the Toeplitz operator of the complex conjugate symbol;
• TauCeti.toeplitz_const: a constant symbol acts by scalar multiplication;
• TauCeti.toeplitz_fourierLp_natCast_hardyBasis, TauCeti.toeplitz_fourierLp_one_hardyBasis: the Toeplitz operator of e_m, m ≥ 0, raises the Hardy basis by m; in particular the forward shift S = T_z sends eₙ to eₙ₊₁;
• TauCeti.coe_toeplitz_fourierLp_natCast_apply, TauCeti.isometry_toeplitz_fourierLp_natCast, TauCeti.toeplitz_fourierLp_natCast: for m ≥ 0, the Toeplitz operator of e_m is multiplication by e_m, an isometry, and the mth power of the forward shift;
• TauCeti.toeplitz_fourierLp_neg: the Toeplitz operator of e_(-k) is the adjoint of that of e_k;
• TauCeti.norm_toeplitz: the operator norm of T_a is exactly ‖a‖∞, so the symbol map is an isometry (TauCeti.isometry_toeplitz) and in particular injective (TauCeti.toeplitz_injective).

The inequality ‖T_a‖ ≤ ‖a‖∞ is immediate from the compression. For the reverse inequality, multiplication by a Fourier monomial e_N is unitary on circle L² and commutes with M_a, and for N large it moves any two trigonometric polynomials f, g into H². Hence |⟪f, a g⟫| = |⟪e_N f, T_a (e_N g)⟫| ≤ ‖T_a‖ ‖f‖ ‖g‖, which extends by density to all of L² and gives ‖M_a‖ ≤ ‖T_a‖; the operator norm of M_a is ‖a‖∞. This norm-equality argument follows Böttcher–Silbermann, Analysis of Toeplitz Operators, §2.

The conventions are those of Conway, A Course in Functional Analysis, second edition, and of E. Park, Toeplitz operators: normalized Haar measure, the modes exp (2πint) and inner products conjugate linear in the first variable.

noncomputable def TauCeti.toeplitz : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle) →L[ℂ] HardySpace →L[ℂ] HardySpace

The Toeplitz operator map, sending an essentially bounded symbol a on the unit circle to the compression T_a = P M_a |H² of multiplication by a to boundary Hardy space.

theorem TauCeti.toeplitz_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : toeplitz a = hardySubmodule.orthogonalProjectionOnto ∘SL MeasureTheory.Lp.multiplicationOperator a ∘SL hardySubmodule.subtypeL

The Toeplitz operator of a compresses the multiplication operator of a to Hardy space.

theorem TauCeti.coe_toeplitz_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (f : HardySpace) : ↑((toeplitz a) f) = hardySubmodule.starProjection (a • ↑f)

The ambient value of T_a f is the Hardy projection of the product a f.

theorem TauCeti.toeplitz_apply_eq_zero_iff (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (f : HardySpace) : (toeplitz a) f = 0 ↔ a • ↑f ∈ hardySubmoduleᗮ

A Hardy function f lies in the kernel of the Toeplitz operator T_a exactly when the product a f lies in the orthogonal complement of Hardy space, that is, when a f has only negative Fourier modes.

theorem TauCeti.inner_toeplitz_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (f g : HardySpace) : inner ℂ f ((toeplitz a) g) = inner ℂ (↑f) (a • ↑g)

Compressing to Hardy space does not change inner products against Hardy functions.

@[simp]

theorem TauCeti.hardyBasis_repr_toeplitz_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (f : HardySpace) (i : ℕ) : ↑(hardyBasis.repr ((toeplitz a) f)) i = fourierCoeff ↑↑(a • ↑f) ↑i

The Hardy coordinates of T_a f are the nonnegative Fourier coefficients of a f.

theorem TauCeti.inner_hardyBasis_toeplitz_hardyBasis (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (i j : ℕ) : inner ℂ (hardyBasis i) ((toeplitz a) (hardyBasis j)) = fourierCoeff (↑↑a) (↑i - ↑j)

Matrix formula. In the Hardy basis e₀, e₁, …, the (i, j) entry of the Toeplitz operator T_a is the Fourier coefficient â(i - j).

@[simp]

theorem TauCeti.adjoint_toeplitz (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : ContinuousLinearMap.adjoint (toeplitz a) = toeplitz (star a)

The adjoint of the Toeplitz operator T_a is the Toeplitz operator of the complex conjugate symbol.

@[simp]

theorem TauCeti.toeplitz_const (c : ℂ) : toeplitz ((MeasureTheory.Lp.const ⊤ AddCircle.haarAddCircle) c) = c • ContinuousLinearMap.id ℂ HardySpace

A constant symbol acts on Hardy space by scalar multiplication.

@[simp]

theorem TauCeti.toeplitz_algebraMap (c : ℂ) : toeplitz ((algebraMap ℂ ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) c) = c • ContinuousLinearMap.id ℂ HardySpace

A symbol in the scalar embedding acts on Hardy space by scalar multiplication.

@[simp]

theorem TauCeti.toeplitz_fourierLp_natCast_hardyBasis (m n : ℕ) : (toeplitz (fourierLp ⊤ ↑m)) (hardyBasis n) = hardyBasis (m + n)

The Toeplitz operator of the Fourier monomial e_m, m ≥ 0, raises the Hardy basis by m.

@[simp]

theorem TauCeti.toeplitz_fourierLp_one_hardyBasis (n : ℕ) : (toeplitz (fourierLp ⊤ 1)) (hardyBasis n) = hardyBasis (n + 1)

The forward shift S = T_z on Hardy space sends eₙ to eₙ₊₁.

theorem TauCeti.coe_toeplitz_fourierLp_natCast_apply (m : ℕ) (f : HardySpace) : ↑((toeplitz (fourierLp ⊤ ↑m)) f) = fourierLp ⊤ ↑m • ↑f

For m ≥ 0, the Toeplitz operator of the Fourier monomial e_m is multiplication by e_m.

theorem TauCeti.coe_toeplitz_fourierLp_one_apply (f : HardySpace) : ↑((toeplitz (fourierLp ⊤ 1)) f) = fourierLp ⊤ 1 • ↑f

The forward shift S = T_{e_1} is multiplication by e_1.

@[simp]

theorem TauCeti.norm_toeplitz_fourierLp_natCast_apply (m : ℕ) (f : HardySpace) : ‖↑((toeplitz (fourierLp ⊤ ↑m)) f)‖ = ‖↑f‖

For m ≥ 0, the Toeplitz operator of the Fourier monomial e_m preserves norms. The norms are taken in L², the simp normal form of norms of Hardy functions.

theorem TauCeti.isometry_toeplitz_fourierLp_natCast (m : ℕ) : Isometry ⇑(toeplitz (fourierLp ⊤ ↑m))

For m ≥ 0, the Toeplitz operator of the Fourier monomial e_m is an isometry of Hardy space.

theorem TauCeti.toeplitz_fourierLp_natCast (m : ℕ) : toeplitz (fourierLp ⊤ ↑m) = toeplitz (fourierLp ⊤ 1) ^ m

The Toeplitz operator of the Fourier monomial e_m, m ≥ 0, is the mth power of the forward shift S = T_{e_1}.

theorem TauCeti.toeplitz_fourierLp_neg (k : ℤ) : toeplitz (fourierLp ⊤ (-k)) = ContinuousLinearMap.adjoint (toeplitz (fourierLp ⊤ k))

The Toeplitz operator of the Fourier monomial e_(-k) is the adjoint of that of e_k.

theorem TauCeti.norm_toeplitz_le (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : ‖toeplitz a‖ ≤ ‖a‖

The operator norm of the Toeplitz operator T_a is at most the L∞ norm of its symbol.

@[simp]

theorem TauCeti.norm_toeplitz (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : ‖toeplitz a‖ = ‖a‖

Symbol norm. The operator norm of the Toeplitz operator T_a is the L∞ norm of its symbol.

theorem TauCeti.isometry_toeplitz : Isometry ⇑toeplitz

The Toeplitz symbol map a ↦ T_a is an isometry.

theorem TauCeti.toeplitz_injective : Function.Injective ⇑toeplitz

A symbol is determined by its Toeplitz operator.