Documentation

TauCeti.Analysis.Fourier.Hardy.Hankel.Basic

Hankel operators and Toeplitz products #

The Hankel operator of a bounded circle symbol is multiplication followed by projection onto the actual orthogonal complement of boundary Hardy space. Together with the Toeplitz compression, it gives the orthogonal decomposition of multiplication on Hardy functions.

The identity toeplitz_comp_sub_toeplitz expresses the defect of multiplicativity of Toeplitz compression as a product of Hankel operators. The Fourier characterization hankel_eq_zero_iff then gives exact multiplication when the right symbol is analytic or the left symbol is coanalytic. This is the algebraic input to compactness of continuous-symbol semicommutators.

The construction uses Mathlib's orthogonal projections and the existing Lp.multiplicationOperator. The conventions and product identity follow Conway, A Course in Functional Analysis, second edition, and E. Park, Toeplitz operators.

source
noncomputable def TauCeti.hankel :
↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle) →L[ℂ] HardySpace →L[ℂ] ↥hardySubmoduleᗮ

The Hankel symbol map H_a = (1 - P) M_a |H², with the orthogonal complement of Hardy space as codomain.

Instances For
    source
    theorem TauCeti.hankel_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) :
    hankel a = hardySubmoduleᗮ.orthogonalProjectionOnto ∘SL MeasureTheory.Lp.multiplicationOperator a ∘SL hardySubmodule.subtypeL

    The Hankel operator projects multiplication onto the negative Fourier modes.

    source
    theorem TauCeti.inner_negativeHardyBasis_hankel_hardyBasis (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (i j : ℕ) :
    inner ℂ (negativeHardyBasis i) ((hankel a) (hardyBasis j)) = fourierCoeff (↑↑a) (-↑i - 1 - ↑j)

    The negative-mode matrix of the orthogonal-complement-valued Hankel operator.

    source
    theorem TauCeti.coe_hankel_apply (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (f : HardySpace) :
    ↑((hankel a) f) = a • ↑f - hardySubmodule.starProjection (a • ↑f)

    The ambient value of a Hankel operator is the complementary Hardy projection.

    source
    theorem TauCeti.coe_toeplitz_add_coe_hankel (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (f : HardySpace) :
    ↑((toeplitz a) f) + ↑((hankel a) f) = a • ↑f

    Multiplication of a Hardy function splits into its Toeplitz and Hankel parts.

    source
    theorem TauCeti.norm_hankel_le (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) :
    ‖hankel a‖ ≤ ‖a‖

    Hankel compression does not increase the norm of the symbol.

    source
    @[simp]
    theorem TauCeti.hankel_const (c : ℂ) :
    hankel ((MeasureTheory.Lp.const ⊤ AddCircle.haarAddCircle) c) = 0

    A constant symbol has zero Hankel operator.

    source
    theorem TauCeti.adjoint_hankel (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) :
    ContinuousLinearMap.adjoint (hankel a) = hardySubmodule.orthogonalProjectionOnto ∘SL MeasureTheory.Lp.multiplicationOperator (star a) ∘SL hardySubmoduleᗮ.subtypeL

    The adjoint of H_a multiplies negative-mode functions by the conjugate symbol and projects back to Hardy space.

    source
    theorem TauCeti.toeplitz_comp_sub_toeplitz (a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) :
    toeplitz a ∘SL toeplitz b - toeplitz (a * b) = -ContinuousLinearMap.adjoint (hankel (star a)) ∘SL hankel b

    Toeplitz semicommutator identity. The defect of multiplication is minus the product of the adjoint Hankel operator of the conjugate left symbol with the right Hankel operator.

    source
    theorem TauCeti.hankel_eq_zero_iff (a : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) :
    hankel a = 0 ↔ ∀ n < 0, fourierCoeff (↑↑a) n = 0

    A Hankel operator vanishes exactly when its symbol has no negative Fourier coefficients.

    source
    theorem TauCeti.toeplitz_comp_of_analytic (a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (hb : ∀ n < 0, fourierCoeff (↑↑b) n = 0) :
    toeplitz a ∘SL toeplitz b = toeplitz (a * b)

    Toeplitz multiplication is exact when the right symbol has no negative Fourier modes.

    source
    theorem TauCeti.toeplitz_comp_of_coanalytic (a b : ↥(MeasureTheory.Lp ℂ ⊤ AddCircle.haarAddCircle)) (ha : ∀ n < 0, fourierCoeff (↑↑(star a)) n = 0) :
    toeplitz a ∘SL toeplitz b = toeplitz (a * b)

    Toeplitz multiplication is exact when the conjugate left symbol is analytic, that is, when the left symbol is coanalytic.