The classical Hankel matrix and the negative-mode flip

The unitary hardyFlip from Hardy.Basic sends the negative Fourier mode e₋ₙ₋₁ to eₙ. Composing it with the existing, orthogonal-complement-valued Hankel operator of the reflected symbol gives classicalHankel a, whose matrix is â(i + j + 1).

This comparison fixes the reflection convention in products of classical Hankel matrices. In particular, the Toeplitz product defect is the negative of classicalHankel a ∘ classicalHankel (b ∘ Neg.neg). These are the Hankel operators used in finite Toeplitz product identities.

References

• A. Böttcher and B. Silbermann, Introduction to Large Truncated Toeplitz Matrices, for the classical Hankel convention and its role in finite-section products.

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

The classical Hankel symbol map. Its matrix in the Hardy basis is â(i + j + 1); the reflection distinguishes it from the negative-mode Hankel compression.

theorem TauCeti.classicalHankel_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : classicalHankel a = hardyFlip.toLinearIsometry.toContinuousLinearMap ∘SL hankel ((MeasureTheory.Lp.compMeasurePreserving (fun (t : AddCircle 1) => -t) ⋯) a)

Classical Hankel operators are flipped Hankel compressions of the reflected symbol.

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

The classical Hankel operator is bounded by the essential supremum of its symbol.

theorem TauCeti.inner_hardyBasis_classicalHankel_hardyBasis (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (i j : ℕ) : inner ℂ (hardyBasis i) ((classicalHankel a) (hardyBasis j)) = fourierCoeff (↑↑a) (↑i + ↑j + 1)

The classical Hankel matrix has constant anti-diagonals â(i + j + 1).

@[simp]

theorem TauCeti.adjoint_classicalHankel (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : ContinuousLinearMap.adjoint (classicalHankel a) = classicalHankel ((MeasureTheory.Lp.compMeasurePreserving (fun (t : AddCircle 1) => -t) ⋯) (star a))

Taking the adjoint conjugates and reflects the classical Hankel symbol.

theorem TauCeti.hardyFlip_comp_hankel (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : hardyFlip.toLinearIsometry.toContinuousLinearMap ∘SL hankel a = classicalHankel ((MeasureTheory.Lp.compMeasurePreserving (fun (t : AddCircle 1) => -t) ⋯) a)

Flipping the negative-mode Hankel compression reflects the classical symbol.

theorem TauCeti.adjoint_hankel_comp_hardyFlip_symm (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : ContinuousLinearMap.adjoint (hankel (star a)) ∘SL hardyFlip.symm.toLinearIsometry.toContinuousLinearMap = classicalHankel a

The adjoint Hankel factor in a Toeplitz product becomes the classical Hankel matrix.

theorem TauCeti.toeplitz_comp_sub_toeplitz_eq_neg_classicalHankel_comp_classicalHankel (a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) : toeplitz a ∘SL toeplitz b - toeplitz (a * b) = -classicalHankel a ∘SL classicalHankel ((MeasureTheory.Lp.compMeasurePreserving (fun (t : AddCircle 1) => -t) ⋯) b)

Classical Toeplitz product identity. The product defect is minus the product of the classical Hankel operator of the left symbol and that of the reflected right symbol.