Hardy space

TheoremSquared norms of the Szegő kernel coefficients#✓fully proved

The squared norms of the Szegő kernel coefficients form a geometric progression with ratio ‖z‖².

theorem norm_sq_szego_coeff (z : ℂ) (n : ℕ) :
    ‖(starRingEnd ℂ z) ^ n‖ ^ (2 : ℝ) = (‖z‖ ^ 2) ^ n

Used by 2

Used bySzegő kernel coefficients lie in ℓ² · Squared norm of the Szegő kernel

TheoremSzegő kernel coefficients lie in ℓ²#✓fully proved

The Szegő kernel coefficients are in ℓ² when z is in the disc.

theorem memℓp_szegoKernel (z : ℂ) (hz : ‖z‖ < 1) :
    Memℓp (fun n => (starRingEnd ℂ z) ^ n) 2

Uses 1 · Used by 1

Proof usesSquared norms of the Szegő kernel coefficients

Used bySzegő kernel of the Hardy space

DefinitionSzegő kernel of the Hardy space#✓fully proved

The Szegő kernel at z: the ℓ²(ℕ, ℂ) sequence with coefficients (conj z)ⁿ.

noncomputable def szegoKernel (z : ℂ) (hz : ‖z‖ < 1) : ℓ²(ℕ, ℂ) :=
  ⟨fun n => (starRingEnd ℂ z) ^ n, memℓp_szegoKernel z hz⟩

Uses 1 · Used by 12

Statement usesSzegő kernel coefficients lie in ℓ²

Used byPoint evaluation on the Hardy space · Point evaluation as a bounded functional on the Hardy space · Hardy-space point evaluation as a Taylor series · Hardy-space evaluation of a single monomial · Hardy-space evaluation at the origin is the constant coefficient · Conjugate reproducing property of the Szegő kernel · Inner product of two Szegő kernels · Norm of Hardy-space point evaluation · Squared norm of the Szegő kernel · Norm of the Szegő kernel · Absolute convergence of Taylor series in the Hardy space · Szegő kernel at the origin is the first basis vector

TheoremSzegő kernel at the origin is the first basis vector#✓fully proved

The Szegő kernel at 0 is the first standard basis vector.

theorem szegoKernel_zero (hz : ‖(0 : ℂ)‖ < 1) :
    szegoKernel 0 hz = lp.single 2 0 (1 : ℂ)

Uses 1 · Used by 1

Statement usesSzegő kernel of the Hardy space

Used byHardy-space evaluation at the origin is the constant coefficient

TheoremSquared norm of the Szegő kernel#✓fully proved

The squared norm of the Szegő kernel is 1 / (1 - ‖z‖²).

theorem norm_sq_szegoKernel (z : ℂ) (hz : ‖z‖ < 1) :
    ‖szegoKernel z hz‖ ^ 2 = 1 / (1 - ‖z‖ ^ 2)

Uses 2 · Used by 1

Statement usesSzegő kernel of the Hardy space

Proof usesSquared norms of the Szegő kernel coefficients

Used byNorm of the Szegő kernel

TheoremNorm of the Szegő kernel#✓fully proved

The norm of the Szegő kernel is 1 / √(1 - ‖z‖²).

theorem norm_szegoKernel (z : ℂ) (hz : ‖z‖ < 1) :
    ‖szegoKernel z hz‖ = 1 / Real.sqrt (1 - ‖z‖ ^ 2)

Uses 2 · Used by 1

Statement usesSzegő kernel of the Hardy space

Proof usesSquared norm of the Szegő kernel

Used byNorm of Hardy-space point evaluation

DefinitionPoint evaluation on the Hardy space#✓fully proved

Point evaluation on H²(𝔻): the inner product with the Szegő kernel.

noncomputable def hardyEval (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) : ℂ :=
  ⟪szegoKernel z hz, a⟫

Uses 1 · Used by 6

Statement usesSzegő kernel of the Hardy space

Used byReproducing property of the Szegő kernel · Hardy-space point evaluation as a Taylor series · Hardy-space evaluation of a single monomial · Hardy-space evaluation at the origin is the constant coefficient · Conjugate reproducing property of the Szegő kernel · Pointwise bound for Hardy-space functions

TheoremHardy-space point evaluation as a Taylor series#✓fully proved

Point evaluation is the Taylor series ∑' n, a n * zⁿ.

theorem hardyEval_eq_tsum (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    hardyEval z hz a = ∑' n, a n * z ^ n

Uses 2

Statement usesPoint evaluation on the Hardy space

Proof usesSzegő kernel of the Hardy space

TheoremAbsolute convergence of Taylor series in the Hardy space#✓fully proved

The Taylor series of an H² function converges absolutely at every point of the disc.

theorem summable_hardyEval_terms (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    Summable (fun n => a n * z ^ n)

Uses 1

Proof usesSzegő kernel of the Hardy space

DefinitionPoint evaluation as a bounded functional on the Hardy space#✓fully proved

Point evaluation as a bounded linear functional on H²(𝔻).

noncomputable def hardyEvalCLM (z : ℂ) (hz : ‖z‖ < 1) : ℓ²(ℕ, ℂ) →L[ℂ] ℂ :=
  innerSL ℂ (szegoKernel z hz)

Uses 1 · Used by 3

Statement usesSzegő kernel of the Hardy space

Used byReproducing property of the Szegő kernel · Norm of Hardy-space point evaluation · Pointwise bound for Hardy-space functions

TheoremReproducing property of the Szegő kernel#✓fully proved

The bounded point-evaluation functional acts by the inner product with the Szegő kernel.

theorem hardyEvalCLM_apply (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    hardyEvalCLM z hz a = hardyEval z hz a

Uses 2 · Used by 1

Statement usesPoint evaluation on the Hardy space · Point evaluation as a bounded functional on the Hardy space

Used byPointwise bound for Hardy-space functions

TheoremNorm of Hardy-space point evaluation#✓fully proved

The operator norm of point evaluation is 1 / √(1 - ‖z‖²).

theorem norm_hardyEvalCLM (z : ℂ) (hz : ‖z‖ < 1) :
    ‖hardyEvalCLM z hz‖ = 1 / Real.sqrt (1 - ‖z‖ ^ 2)

Uses 3 · Used by 1

Statement usesPoint evaluation as a bounded functional on the Hardy space

Proof usesNorm of the Szegő kernel · Szegő kernel of the Hardy space

Used byPointwise bound for Hardy-space functions

TheoremPointwise bound for Hardy-space functions#✓fully proved

The pointwise bound for H² functions: ‖f(z)‖ ≤ ‖f‖ / √(1 - ‖z‖²).

theorem norm_hardyEval_le (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    ‖hardyEval z hz a‖ ≤ ‖a‖ / Real.sqrt (1 - ‖z‖ ^ 2)

Uses 4

Statement usesPoint evaluation on the Hardy space

Proof usesPoint evaluation as a bounded functional on the Hardy space · Reproducing property of the Szegő kernel · Norm of Hardy-space point evaluation

TheoremHardy-space evaluation at the origin is the constant coefficient#✓fully proved

Evaluation at 0 is the constant Taylor coefficient.

theorem hardyEval_zero (a : ℓ²(ℕ, ℂ)) (hz : ‖(0 : ℂ)‖ < 1) :
    hardyEval 0 hz a = a 0

Uses 3

Statement usesPoint evaluation on the Hardy space

Proof usesSzegő kernel of the Hardy space · Szegő kernel at the origin is the first basis vector

TheoremHardy-space evaluation of a single monomial#✓fully proved

Evaluation of a monomial c * zⁿ (a single Taylor coefficient).

theorem hardyEval_single (z : ℂ) (hz : ‖z‖ < 1) (n : ℕ) (c : ℂ) :
    hardyEval z hz (lp.single 2 n c) = c * z ^ n

Uses 2

Statement usesPoint evaluation on the Hardy space

Proof usesSzegő kernel of the Hardy space

TheoremConjugate reproducing property of the Szegő kernel#✓fully proved

The reproducing property in the other order: ⟪a, k_z⟫ = conj (f(z)).

theorem inner_szegoKernel_right (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    ⟪a, szegoKernel z hz⟫ = (starRingEnd ℂ) (hardyEval z hz a)

Uses 2

Statement usesPoint evaluation on the Hardy space · Szegő kernel of the Hardy space

TheoremInner product of two Szegő kernels#✓fully proved

The inner product of two Szegő kernels is the Szegő kernel function 1 / (1 - z * conj w).

theorem inner_szegoKernel_szegoKernel (z : ℂ) (hz : ‖z‖ < 1) (w : ℂ)
    (hw : ‖w‖ < 1) :
    ⟪szegoKernel z hz, szegoKernel w hw⟫ = (1 - z * (starRingEnd ℂ w))⁻¹

Uses 1

Statement usesSzegő kernel of the Hardy space

TheoremTaylor coefficients of a Hardy-space function are bounded by its norm#✓fully proved

Taylor coefficients of an H² function are bounded by its norm: a single squared coefficient is at most the sum of all of them.

theorem abs_coeff_le_norm (a : ℓ²(ℕ, ℂ)) (n : ℕ) : ‖a n‖ ≤ ‖a‖

DefinitionThe boundary Hardy space H¹#✓fully proved

Let \(\mathbb{T} = \mathbb{R}/\mathbb{Z}\) carry its Haar measure normalized to total mass \(1\). The Hardy space \(H^1\) is the complex linear subspace of \(L^1(\mathbb{T})\) consisting of those \(f\) whose Fourier coefficients \(\hat f(n) = \int_{\mathbb{T}} f(t) e^{-2\pi i n t} dt\) vanish for all integers \(n < 0\).

def H1 : Submodule ℂ (Lp ℂ 1 (AddCircle.haarAddCircle (T := 1))) where
  carrier := {f | ∀ n : ℤ, n < 0 → fourierCoeff f n = 0}
  zero_mem' := by simp [fourierCoeff]
  add_mem' := by
    intro f g hf hg n hn
    rw [fourierCoeff_congr_ae (Lp.coeFn_add f g),
      fourierCoeff.add (L1.integrable_coeFn f) (L1.integrable_coeFn g)]
    simp_all
  smul_mem' := by
    intro c f n hn
    rw [fourierCoeff_congr_ae (Lp.coeFn_smul c f), fourierCoeff.const_smul]
    simp_all

Used by 1

Used byNewman's theorem: no bounded projection onto the Hardy space

TheoremNewman's theorem: no bounded projection onto the Hardy space#●ready to prove

Let \(L^1(\mathbb{T})\) be the space of integrable complex functions on the circle \(\mathbb{T} = \mathbb{R}/\mathbb{Z}\) with its normalized Haar measure, and let \(H^1 \subseteq L^1(\mathbb{T})\) be the boundary Hardy space. There is no continuous \(\mathbb{C}\)-linear map \(\pi : L^1(\mathbb{T}) \to H^1\) with \(\pi(f) = f\) for every \(f \in H^1\).

public theorem_wanted H1_not_closedComplemented :
    ¬ H1.ClosedComplemented

Sources

• D. J. Newman, 'The nonexistence of projections from L^1 to H^1', Proc. Amer. Math. Soc.; W. Rudin, Fourier Analysis on Groups; Yongxi Lin, Hardy Space and Hartogs Triangle, Theorem 2.8. Problem H1_not_closedComplemented of the lean-eval benchmark.

Uses 1

Statement usesThe boundary Hardy space H¹

19 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.