Boundary uniqueness for the Hardy space

A nonzero boundary Hardy function x ∈ H² is nonzero almost everywhere on the circle. This is the boundary uniqueness behind Coburn's alternative for Toeplitz operators: the product of two nonzero Hardy functions is nonzero almost everywhere, so a symbol a with a * f * conj g = 0 almost everywhere for nonzero Hardy functions f and g vanishes almost everywhere.

Implementation notes

The circle restrictions t ↦ F_x (r * e (t)) of the disk function converge to x in L² as r → 1⁻, so along a sequence of radii they converge to x almost everywhere. On these circles the averages of log⁺ ‖F_x‖ are bounded by the averages of ‖F_x‖ ^ 2, which converge to ‖x‖ ^ 2. If x vanished on a set of positive measure, the sequential form of the F. and M. Riesz uniqueness theorem, which combines Jensen's inequality with Fatou's lemma, would make F_x vanish on the disk, and hence x = 0.

Main results

• TauCeti.HardySpace.ae_ne_zero: a nonzero Hardy function is nonzero almost everywhere.
• TauCeti.HardySpace.ae_ne_zero_iff: a Hardy function is nonzero almost everywhere exactly when it is nonzero.

References

• P. L. Duren, Theory of Hᵖ Spaces, Chapter 2.
• E. Park, Toeplitz operators, for the use of boundary uniqueness in Coburn's alternative.

theorem TauCeti.HardySpace.ae_ne_zero {x : HardySpace} (hx : x ≠ 0) : ∀ᵐ (t : AddCircle 1) ∂AddCircle.haarAddCircle, ↑↑↑x t ≠ 0

Boundary uniqueness for the Hardy space. A nonzero Hardy function is nonzero almost everywhere on the circle.

theorem TauCeti.HardySpace.ae_ne_zero_iff {x : HardySpace} : (∀ᵐ (t : AddCircle 1) ∂AddCircle.haarAddCircle, ↑↑↑x t ≠ 0) ↔ x ≠ 0

A Hardy function is nonzero almost everywhere on the circle exactly when it is nonzero.