The boundary Hardy Hilbert space

The boundary Hardy space is the closed complex subspace of the native L² space on UnitAddCircle generated by the nonnegative Fourier modes. Its elements are exactly the functions with vanishing negative Fourier coefficients. The nonnegative modes form a Hilbert basis, whose representation identifies the space isometrically with native lp sequences. The negative modes form the basis negativeHardyBasis of the orthogonal complement; the unitary hardyFlip sends e₋ₙ₋₁ to eₙ. The ambient orthogonal projection and complementary negative modes provide the boundary decomposition used to compress multiplication operators to Hardy space. Multiplication by a sufficiently high Fourier mode moves every trigonometric polynomial into Hardy space (TauCeti.eventually_fourierLp_smul_mem_hardySubmodule).

The conventions are those of Conway, A Course in Functional Analysis, second edition: normalized Haar measure and the modes exp (2πint). The formal construction uses Mathlib's fourierBasis and HilbertBasis.mkOfOrthogonalEqBot.

noncomputable def TauCeti.hardySubmodule : Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

The closed subspace of circle L² generated by the nonnegative Fourier modes.

@[reducible, inline]

abbrev TauCeti.HardySpace : Type

The boundary Hardy space, with the norm and inner product inherited from circle L².

theorem TauCeti.hardySubmodule_def : hardySubmodule = (Submodule.span ℂ (Set.range fun (n : ℕ) => fourierBasis ↑n)).topologicalClosure

The Hardy submodule is the closed span of the nonnegative Fourier modes.

theorem TauCeti.isClosed_hardySubmodule : IsClosed ↑hardySubmodule

The boundary Hardy subspace is closed in native circle L².

instance TauCeti.instCompleteSpaceHardySpace : CompleteSpace HardySpace

Boundary Hardy space is a Hilbert space.

theorem TauCeti.fourierBasis_mem_hardySubmodule (n : ℕ) : fourierBasis ↑n ∈ hardySubmodule

Every nonnegative Fourier mode belongs to the boundary Hardy space.

theorem TauCeti.eventually_fourierLp_smul_mem_hardySubmodule {g : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)} (hg : g ∈ Submodule.span ℂ (Set.range ⇑fourierBasis)) : ∀ᶠ (N : ℤ) in Filter.atTop, fourierLp ⊤ N • g ∈ hardySubmodule

Multiplying a trigonometric polynomial by a sufficiently high Fourier mode lands in Hardy space.

theorem TauCeti.mem_hardySubmodule_iff (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : f ∈ hardySubmodule ↔ ∀ n < 0, fourierCoeff (↑↑f) n = 0

A circle L² function is in the Hardy space exactly when its negative coefficients vanish.

theorem TauCeti.fourierLp_natCast_smul_mem_hardySubmodule (m : ℕ) {f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)} (hf : f ∈ hardySubmodule) : fourierLp ⊤ ↑m • f ∈ hardySubmodule

Multiplication by a Fourier monomial e_m with m ≥ 0 preserves Hardy space.

noncomputable def TauCeti.hardyBasis : HilbertBasis ℕ ℂ HardySpace

The natural-number-indexed Fourier Hilbert basis of boundary Hardy space.

@[simp]

theorem TauCeti.coe_hardyBasis (n : ℕ) : ↑(hardyBasis n) = fourierBasis ↑n

Hardy basis vectors are precisely the nonnegative ambient Fourier modes.

theorem TauCeti.hardyBasis_repr (f : HardySpace) (n : ℕ) : ↑(hardyBasis.repr f) n = fourierCoeff ↑↑↑f ↑n

Hardy coordinates are the ordinary nonnegative Fourier coefficients.

theorem TauCeti.HardySpace.fourierCoeff_eq_zero (f : HardySpace) {n : ℤ} (hn : n < 0) : fourierCoeff (↑↑↑f) n = 0

Hardy functions have no negative Fourier coefficients.

theorem TauCeti.HardySpace.norm_fourierCoeff_le (x : HardySpace) (n : ℕ) : ‖fourierCoeff ↑↑↑x ↑n‖ ≤ ‖x‖

Each Hardy coefficient is bounded by the norm of the Hardy function.

theorem TauCeti.hardyBasis_repr_orthogonalProjectionOnto (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℕ) : ↑(hardyBasis.repr (hardySubmodule.orthogonalProjectionOnto f)) n = fourierCoeff ↑↑f ↑n

Projection retains every nonnegative Fourier coefficient.

@[simp]

theorem TauCeti.fourierCoeff_hardySubmodule_starProjection (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℤ) : fourierCoeff (↑↑(hardySubmodule.starProjection f)) n = if 0 ≤ n then fourierCoeff (↑↑f) n else 0

Orthogonal Hardy projection deletes precisely the negative Fourier coefficients.

theorem TauCeti.mem_hardySubmodule_orthogonal_iff (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) : f ∈ hardySubmoduleᗮ ↔ ∀ (n : ℕ), fourierCoeff ↑↑f ↑n = 0

The orthogonal complement of Hardy space consists of functions with only negative modes.

theorem TauCeti.hardySubmodule_orthogonal_eq : hardySubmoduleᗮ = (Submodule.span ℂ (Set.range fun (n : ℕ) => fourierBasis (-↑n - 1))).topologicalClosure

The negative Fourier modes span exactly the orthogonal complement of Hardy space. Together with Submodule.isCompl_orthogonal, this gives the orthogonal splitting of circle L² into its nonnegative and negative modes.

theorem TauCeti.fourierBasis_mem_hardySubmodule_orthogonal (n : ℕ) : fourierBasis (-↑n - 1) ∈ hardySubmoduleᗮ

Every strictly negative Fourier mode belongs to the orthogonal complement of Hardy space.

noncomputable def TauCeti.negativeHardyBasis : HilbertBasis ℕ ℂ ↥hardySubmoduleᗮ

The negative Fourier basis of the orthogonal complement of Hardy space, ordered e₋₁, e₋₂, ….

@[simp]

theorem TauCeti.coe_negativeHardyBasis (n : ℕ) : ↑(negativeHardyBasis n) = fourierBasis (-↑n - 1)

Negative Hardy basis vectors are the corresponding ambient Fourier modes.

theorem TauCeti.negativeHardyBasis_repr (f : ↥hardySubmoduleᗮ) (n : ℕ) : ↑(negativeHardyBasis.repr f) n = fourierCoeff (↑↑↑f) (-↑n - 1)

Coordinates in the negative Hardy basis are the strictly negative Fourier coefficients.

noncomputable def TauCeti.hardyFlip : ↥hardySubmoduleᗮ ≃ₗᵢ[ℂ] HardySpace

The unitary flip from negative modes to Hardy space, sending e₋ₙ₋₁ to eₙ.

@[simp]

theorem TauCeti.hardyBasis_repr_hardyFlip (f : ↥hardySubmoduleᗮ) : hardyBasis.repr (hardyFlip f) = negativeHardyBasis.repr f

The flip preserves coordinates in the negative and nonnegative Hardy bases.

@[simp]

theorem TauCeti.negativeHardyBasis_repr_hardyFlip_symm (f : HardySpace) : negativeHardyBasis.repr (hardyFlip.symm f) = hardyBasis.repr f

The inverse flip preserves the same coordinates.

@[simp]

theorem TauCeti.hardyFlip_negativeHardyBasis (n : ℕ) : hardyFlip (negativeHardyBasis n) = hardyBasis n

The flip sends the nth negative mode to the nth nonnegative mode.

@[simp]

theorem TauCeti.hardyFlip_symm_hardyBasis (n : ℕ) : hardyFlip.symm (hardyBasis n) = negativeHardyBasis n

The inverse flip sends the nth nonnegative mode to the nth negative mode.