The holomorphic disk function of a Hardy function

A boundary Hardy function x, with Fourier coefficients x̂ n, defines the power series F_x w = ∑ n, x̂ n * w ^ n on the open unit disk. Because the coefficients are square summable, they are bounded by ‖x‖, so the series converges on the whole disk.

Main results

• TauCeti.HardySpace.diskFunction: the function F_x.
• TauCeti.HardySpace.hasFPowerSeriesOnBall_diskFunction: F_x is the sum of its Taylor series on the unit disk; in particular it is holomorphic there (TauCeti.HardySpace.differentiableOn_diskFunction) and the partial sums converge locally uniformly (TauCeti.HardySpace.tendstoLocallyUniformlyOn_diskFunction).
• TauCeti.HardySpace.norm_diskFunction_le: the pointwise bound ‖F_x w‖ ≤ ‖x‖ / √(1 - ‖w‖ ^ 2), from the Cauchy–Schwarz inequality in ℓ².
• TauCeti.HardySpace.tendsto_eLpNorm_diskFunction_sub: the circle restrictions t ↦ F_x (r * e (t)) converge to x in L² as r → 1⁻.
• TauCeti.HardySpace.tendsto_circleAverage_norm_sq_diskFunction: the squared circle means of F_x converge to the squared boundary norm as r → 1⁻.

References

• J. B. Conway, A Course in Functional Analysis, second edition.
• P. L. Duren, Theory of Hᵖ Spaces, chapter 1.

noncomputable def TauCeti.HardySpace.diskFunction (x : HardySpace) (w : ℂ) : ℂ

The holomorphic function w ↦ ∑ n, x̂ n * w ^ n on the unit disk determined by a boundary Hardy function x, where x̂ n is its n-th Fourier coefficient. Outside the open unit disk the value is a junk value.

theorem TauCeti.HardySpace.diskFunction_def (x : HardySpace) (w : ℂ) : x.diskFunction w = ∑' (n : ℕ), fourierCoeff ↑↑↑x ↑n * w ^ n

The disk function is the coefficient series ∑' n, x̂ n * w ^ n at every point.

theorem TauCeti.HardySpace.summable_norm_fourierCoeff_mul_pow (x : HardySpace) {w : ℂ} (hw : ‖w‖ < 1) : Summable fun (n : ℕ) => ‖fourierCoeff ↑↑↑x ↑n * w ^ n‖

The Taylor series of the disk function converges absolutely on the open unit disk.

theorem TauCeti.HardySpace.hasSum_diskFunction (x : HardySpace) {w : ℂ} (hw : ‖w‖ < 1) : HasSum (fun (n : ℕ) => fourierCoeff ↑↑↑x ↑n * w ^ n) (x.diskFunction w)

On the open unit disk the disk function is the sum of its Taylor series.

@[simp]

theorem TauCeti.HardySpace.diskFunction_apply_zero (x : HardySpace) : x.diskFunction 0 = fourierCoeff (↑↑↑x) 0

The value of the disk function at the origin is the zeroth Fourier coefficient.

@[simp]

theorem TauCeti.HardySpace.diskFunction_hardyBasis (n : ℕ) (w : ℂ) : (hardyBasis n).diskFunction w = w ^ n

The disk function of the n-th Hardy basis vector is the monomial w ^ n.

@[simp]

theorem TauCeti.HardySpace.diskFunction_zero (w : ℂ) : diskFunction 0 w = 0

The disk function of the zero Hardy function vanishes identically.

theorem TauCeti.HardySpace.diskFunction_add (x : HardySpace) {w : ℂ} (y : HardySpace) (hw : ‖w‖ < 1) : (x + y).diskFunction w = x.diskFunction w + y.diskFunction w

On the open unit disk the disk function depends additively on the Hardy function.

theorem TauCeti.HardySpace.diskFunction_smul (x : HardySpace) {w : ℂ} (c : ℂ) : (c • x).diskFunction w = c * x.diskFunction w

The disk function commutes with scalar multiplication at every point.

theorem TauCeti.HardySpace.hasFPowerSeriesOnBall_diskFunction (x : HardySpace) : HasFPowerSeriesOnBall x.diskFunction (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => fourierCoeff ↑↑↑x ↑n) 0 1

The disk function is the sum of its Taylor series on the open unit disk.

theorem TauCeti.HardySpace.analyticOnNhd_diskFunction (x : HardySpace) : AnalyticOnNhd ℂ x.diskFunction (Metric.ball 0 1)

The disk function is analytic on the open unit disk.

theorem TauCeti.HardySpace.differentiableOn_diskFunction (x : HardySpace) : DifferentiableOn ℂ x.diskFunction (Metric.ball 0 1)

The disk function is holomorphic on the open unit disk.

theorem TauCeti.HardySpace.tendstoLocallyUniformlyOn_diskFunction (x : HardySpace) : TendstoLocallyUniformlyOn (fun (N : ℕ) (w : ℂ) => ∑ n ∈ Finset.range N, fourierCoeff ↑↑↑x ↑n * w ^ n) x.diskFunction Filter.atTop (Metric.ball 0 1)

The partial sums of the Taylor series converge to the disk function locally uniformly on the open unit disk.

theorem TauCeti.HardySpace.norm_diskFunction_le (x : HardySpace) {w : ℂ} (hw : ‖w‖ < 1) : ‖x.diskFunction w‖ ≤ ‖x‖ / √(1 - ‖w‖ ^ 2)

The pointwise bound ‖F_x w‖ ≤ ‖x‖ / √(1 - ‖w‖ ^ 2) on the open unit disk, obtained by pairing the coefficient sequence of x with the square-summable sequence (conj w ^ n) in ℓ².

Radial approximation in L²

theorem TauCeti.HardySpace.tendsto_eLpNorm_diskFunction_sub (x : HardySpace) : Filter.Tendsto (fun (r : ℝ) => MeasureTheory.eLpNorm (fun (t : AddCircle 1) => x.diskFunction (↑r * ↑t.toCircle) - ↑↑↑x t) 2 AddCircle.haarAddCircle) (nhdsWithin 1 (Set.Iio 1)) (nhds 0)

The circle restrictions t ↦ F_x (r * e (t)) of the disk function converge to the boundary function x in L² as r → 1⁻.

theorem TauCeti.HardySpace.tendsto_circleAverage_norm_sq_diskFunction (x : HardySpace) : Filter.Tendsto (fun (r : ℝ) => Real.circleAverage (fun (w : ℂ) => ‖x.diskFunction w‖ ^ 2) 0 r) (nhdsWithin 1 (Set.Iio 1)) (nhds (‖x‖ ^ 2))

The squared circle means of the disk function converge to the squared boundary Hardy norm as the radius tends to one from below.

theorem TauCeti.HardySpace.eqOn_diskFunction_zero_iff (x : HardySpace) : Set.EqOn x.diskFunction 0 (Metric.ball 0 1) ↔ x = 0

A Hardy function is determined by its disk function: F_x vanishes on the open unit disk exactly when x = 0.