Dirichlet space

TheoremClosed form of \(\sum r^n/(n+1)\) for real \(0<r<1\)#✓fully proved

Closed form of \(\sum r^n/(n+1)\) for real \(0\lt r<1\). The power series ∑' n, rⁿ / (n + 1) sums to -log (1 - r) / r for 0 < r < 1: factor 1 / r out of the logarithm series.

theorem hasSum_div_succ_pow_real {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    HasSum (fun n : ℕ => r ^ n / ((n : ℝ) + 1)) (-Real.log (1 - r) / r)

Used by 1

Used bySquared norm of the Dirichlet kernel away from the origin

TheoremClosed form of \(\sum u^n/(n+1)\) for complex \(u\) in the unit disc#✓fully proved

The complex form: ∑' n, uⁿ / (n + 1) sums to -log (1 - u) / u for u ≠ 0 in the unit disc.

theorem hasSum_div_succ_pow_complex {u : ℂ} (h0 : u ≠ 0) (h1 : ‖u‖ < 1) :
    HasSum (fun n : ℕ => u ^ n / ((n : ℂ) + 1)) (-Complex.log (1 - u) / u)

Used by 1

Used byLogarithmic formula for the inner product of Dirichlet kernels

TheoremSquared norms of the Dirichlet kernel coefficients#✓fully proved

The squared norms of the Dirichlet kernel coefficients are ‖z‖ ^ (2 * n) / (n + 1).

theorem norm_sq_dirichlet_coeff (z : ℂ) (n : ℕ) :
    ‖(starRingEnd ℂ z) ^ n / (Real.sqrt ((n : ℝ) + 1) : ℂ)‖ ^ (2 : ℝ) =
      (‖z‖ ^ 2) ^ n / ((n : ℝ) + 1)

Used by 2

Used byDirichlet kernel coefficients lie in ℓ² · Squared norm of the Dirichlet kernel away from the origin

TheoremSquare-summability of the Dirichlet kernel coefficients#✓fully proved

The Dirichlet kernel coefficients are summable in the ℓ² sense: ∑' n, (‖z‖²)ⁿ / (n + 1) converges, by comparison with the geometric series.

theorem summable_dirichletKernel_terms (z : ℂ) (hz : ‖z‖ < 1) :
    Summable (fun n : ℕ => (‖z‖ ^ 2) ^ n / ((n : ℝ) + 1))

Used by 1

Used byDirichlet kernel coefficients lie in ℓ²

TheoremDirichlet kernel coefficients lie in ℓ²#✓fully proved

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

theorem memℓp_dirichletKernel (z : ℂ) (hz : ‖z‖ < 1) :
    Memℓp (fun n : ℕ => (starRingEnd ℂ z) ^ n / (Real.sqrt ((n : ℝ) + 1) : ℂ)) 2

Uses 2 · Used by 1

Proof usesSquared norms of the Dirichlet kernel coefficients · Square-summability of the Dirichlet kernel coefficients

Used byReproducing kernel of the Dirichlet space

DefinitionReproducing kernel of the Dirichlet space#✓fully proved

The Dirichlet kernel at z: the ℓ²(ℕ, ℂ) sequence with coefficients (conj z)ⁿ / √(n + 1).

noncomputable def dirichletKernel (z : ℂ) (hz : ‖z‖ < 1) : ℓ²(ℕ, ℂ) :=
  ⟨fun n => (starRingEnd ℂ z) ^ n / (Real.sqrt ((n : ℝ) + 1) : ℂ),
    memℓp_dirichletKernel z hz⟩

Uses 1 · Used by 21

Statement usesDirichlet kernel coefficients lie in ℓ²

Used byPoint evaluation on the Dirichlet space · Point evaluation as a bounded functional on the Dirichlet space · Dirichlet kernel evaluated at its own point · Sharpness of the Dirichlet-space pointwise bound · Dirichlet-space point evaluation as a Taylor series · Dirichlet-space evaluation of a single monomial · Dirichlet-space evaluation at the origin is the constant coefficient · Dirichlet kernel at the origin is the first basis vector · Inner product of two Dirichlet kernels as a power series · Logarithmic formula for the inner product of Dirichlet kernels · Conjugate reproducing property of the Dirichlet kernel · Norm of Dirichlet-space point evaluation equals the kernel norm · Closed-form norm of Dirichlet-space point evaluation · Norm of Dirichlet-space point evaluation at the origin · Pointwise bound for Dirichlet-space functions · Norm of the Dirichlet kernel away from the origin · Norm of the Dirichlet kernel at the origin · Dirichlet kernel norm is bounded by the Szegő kernel norm · Squared norm of the Dirichlet kernel away from the origin · Squared norm of the Dirichlet kernel at the origin · Absolute convergence of Taylor series in the Dirichlet space

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

The Dirichlet kernel at 0 is the first standard basis vector.

theorem dirichletKernel_zero (hz : ‖(0 : ℂ)‖ < 1) :
    dirichletKernel 0 hz = lp.single 2 0 (1 : ℂ)

Uses 1 · Used by 3

Statement usesReproducing kernel of the Dirichlet space

Used byDirichlet-space evaluation at the origin is the constant coefficient · Norm of the Dirichlet kernel at the origin · Squared norm of the Dirichlet kernel at the origin

TheoremSquared norm of the Dirichlet kernel away from the origin#✓fully proved

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

theorem norm_sq_dirichletKernel_of_ne_zero (z : ℂ) (hz : ‖z‖ < 1) (h0 : z ≠ 0) :
    ‖dirichletKernel z hz‖ ^ 2 = -Real.log (1 - ‖z‖ ^ 2) / ‖z‖ ^ 2

Uses 3 · Used by 3

Statement usesReproducing kernel of the Dirichlet space

Proof usesClosed form of \(\sum r^n/(n+1)\) for real \(0<r<1\) · Squared norms of the Dirichlet kernel coefficients

Used bySharpness of the Dirichlet-space pointwise bound · Norm of the Dirichlet kernel away from the origin · Dirichlet kernel norm is bounded by the Szegő kernel norm

TheoremSquared norm of the Dirichlet kernel at the origin#✓fully proved

The squared norm of the Dirichlet kernel at 0 is 1.

theorem norm_sq_dirichletKernel_zero (hz : ‖(0 : ℂ)‖ < 1) :
    ‖dirichletKernel 0 hz‖ ^ 2 = 1

Uses 2 · Used by 1

Statement usesReproducing kernel of the Dirichlet space

Proof usesDirichlet kernel at the origin is the first basis vector

Used byDirichlet kernel norm is bounded by the Szegő kernel norm

TheoremNorm of the Dirichlet kernel away from the origin#✓fully proved

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

theorem norm_dirichletKernel_of_ne_zero (z : ℂ) (hz : ‖z‖ < 1) (h0 : z ≠ 0) :
    ‖dirichletKernel z hz‖ = Real.sqrt (-Real.log (1 - ‖z‖ ^ 2) / ‖z‖ ^ 2)

Uses 2 · Used by 1

Statement usesReproducing kernel of the Dirichlet space

Proof usesSquared norm of the Dirichlet kernel away from the origin

Used byClosed-form norm of Dirichlet-space point evaluation

TheoremNorm of the Dirichlet kernel at the origin#✓fully proved

The norm of the Dirichlet kernel at 0 is 1.

theorem norm_dirichletKernel_zero (hz : ‖(0 : ℂ)‖ < 1) :
    ‖dirichletKernel 0 hz‖ = 1

Uses 2 · Used by 1

Statement usesReproducing kernel of the Dirichlet space

Proof usesDirichlet kernel at the origin is the first basis vector

Used byNorm of Dirichlet-space point evaluation at the origin

TheoremDirichlet kernel norm is bounded by the Szegő kernel norm#✓fully proved

The Dirichlet kernel norm is bounded by the Hardy kernel norm: ‖k_z‖² ≤ 1 / (1 - ‖z‖²), via log x ≤ x - 1 at x = (1 - ‖z‖²)⁻¹.

theorem norm_sq_dirichletKernel_le_inv (z : ℂ) (hz : ‖z‖ < 1) :
    ‖dirichletKernel z hz‖ ^ 2 ≤ 1 / (1 - ‖z‖ ^ 2)

Uses 3

Statement usesReproducing kernel of the Dirichlet space

Proof usesSquared norm of the Dirichlet kernel away from the origin · Squared norm of the Dirichlet kernel at the origin

DefinitionPoint evaluation on the Dirichlet space#✓fully proved

Point evaluation on 𝒟(𝔻): the inner product with the Dirichlet kernel.

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

Uses 1 · Used by 8

Statement usesReproducing kernel of the Dirichlet space

Used byReproducing property of the Dirichlet kernel · Dirichlet kernel evaluated at its own point · Sharpness of the Dirichlet-space pointwise bound · Dirichlet-space point evaluation as a Taylor series · Dirichlet-space evaluation of a single monomial · Dirichlet-space evaluation at the origin is the constant coefficient · Conjugate reproducing property of the Dirichlet kernel · Pointwise bound for Dirichlet-space functions

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

Point evaluation is the Taylor series ∑' n, a n * zⁿ / √(n + 1).

theorem dirichletEval_eq_tsum (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    dirichletEval z hz a = ∑' n, a n * z ^ n / (Real.sqrt ((n : ℝ) + 1) : ℂ)

Uses 2

Statement usesPoint evaluation on the Dirichlet space

Proof usesReproducing kernel of the Dirichlet space

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

The Taylor series of a 𝒟 function converges absolutely at every point of the disc.

theorem summable_dirichletEval_terms (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    Summable (fun n => a n * z ^ n / (Real.sqrt ((n : ℝ) + 1) : ℂ))

Uses 1

Proof usesReproducing kernel of the Dirichlet space

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

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

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

Uses 1 · Used by 5

Statement usesReproducing kernel of the Dirichlet space

Used byReproducing property of the Dirichlet kernel · Norm of Dirichlet-space point evaluation equals the kernel norm · Closed-form norm of Dirichlet-space point evaluation · Norm of Dirichlet-space point evaluation at the origin · Pointwise bound for Dirichlet-space functions

TheoremReproducing property of the Dirichlet kernel#✓fully proved

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

theorem dirichletEvalCLM_apply (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    dirichletEvalCLM z hz a = dirichletEval z hz a

Uses 2 · Used by 1

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

Used byPointwise bound for Dirichlet-space functions

TheoremNorm of Dirichlet-space point evaluation equals the kernel norm#✓fully proved

The operator norm of point evaluation is the norm of the kernel.

theorem norm_dirichletEvalCLM (z : ℂ) (hz : ‖z‖ < 1) :
    ‖dirichletEvalCLM z hz‖ = ‖dirichletKernel z hz‖

Uses 2 · Used by 3

Statement usesPoint evaluation as a bounded functional on the Dirichlet space · Reproducing kernel of the Dirichlet space

Used byClosed-form norm of Dirichlet-space point evaluation · Norm of Dirichlet-space point evaluation at the origin · Pointwise bound for Dirichlet-space functions

TheoremClosed-form norm of Dirichlet-space point evaluation#✓fully proved

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

theorem norm_dirichletEvalCLM_of_ne_zero (z : ℂ) (hz : ‖z‖ < 1) (h0 : z ≠ 0) :
    ‖dirichletEvalCLM z hz‖ = Real.sqrt (-Real.log (1 - ‖z‖ ^ 2) / ‖z‖ ^ 2)

Uses 4

Statement usesPoint evaluation as a bounded functional on the Dirichlet space

Proof usesReproducing kernel of the Dirichlet space · Norm of Dirichlet-space point evaluation equals the kernel norm · Norm of the Dirichlet kernel away from the origin

TheoremNorm of Dirichlet-space point evaluation at the origin#✓fully proved

The operator norm of point evaluation at 0 is 1.

theorem norm_dirichletEvalCLM_zero (hz : ‖(0 : ℂ)‖ < 1) :
    ‖dirichletEvalCLM 0 hz‖ = 1

Uses 4

Statement usesPoint evaluation as a bounded functional on the Dirichlet space

Proof usesReproducing kernel of the Dirichlet space · Norm of Dirichlet-space point evaluation equals the kernel norm · Norm of the Dirichlet kernel at the origin

TheoremPointwise bound for Dirichlet-space functions#✓fully proved

The pointwise bound for 𝒟 functions: ‖f(z)‖ ≤ ‖f‖ * ‖k_z‖.

theorem norm_dirichletEval_le (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    ‖dirichletEval z hz a‖ ≤ ‖a‖ * ‖dirichletKernel z hz‖

Uses 5

Statement usesPoint evaluation on the Dirichlet space · Reproducing kernel of the Dirichlet space

Proof usesPoint evaluation as a bounded functional on the Dirichlet space · Reproducing property of the Dirichlet kernel · Norm of Dirichlet-space point evaluation equals the kernel norm

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

Evaluation at 0 is the constant Taylor coefficient.

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

Uses 3

Statement usesPoint evaluation on the Dirichlet space

Proof usesReproducing kernel of the Dirichlet space · Dirichlet kernel at the origin is the first basis vector

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

Evaluation of a monomial c * zⁿ / √(n + 1) (a single coefficient).

theorem dirichletEval_single (z : ℂ) (hz : ‖z‖ < 1) (n : ℕ) (c : ℂ) :
    dirichletEval z hz (lp.single 2 n c) =
      c * z ^ n / (Real.sqrt ((n : ℝ) + 1) : ℂ)

Uses 2

Statement usesPoint evaluation on the Dirichlet space

Proof usesReproducing kernel of the Dirichlet space

TheoremConjugate reproducing property of the Dirichlet kernel#✓fully proved

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

theorem inner_dirichletKernel_right (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    ⟪a, dirichletKernel z hz⟫ = (starRingEnd ℂ) (dirichletEval z hz a)

Uses 2

Statement usesPoint evaluation on the Dirichlet space · Reproducing kernel of the Dirichlet space

TheoremInner product of two Dirichlet kernels as a power series#✓fully proved

The inner product of two Dirichlet kernels is the power series ∑' n, (z * conj w)ⁿ / (n + 1).

theorem inner_dirichletKernel_dirichletKernel (z : ℂ) (hz : ‖z‖ < 1) (w : ℂ)
    (hw : ‖w‖ < 1) :
    ⟪dirichletKernel z hz, dirichletKernel w hw⟫ =
      ∑' (n : ℕ), (z * (starRingEnd ℂ w)) ^ n / ((n : ℂ) + 1)

Uses 1 · Used by 1

Statement usesReproducing kernel of the Dirichlet space

Used byLogarithmic formula for the inner product of Dirichlet kernels

TheoremLogarithmic formula for the inner product of Dirichlet kernels#✓fully proved

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

theorem inner_dirichletKernel_dirichletKernel_eq_log (z : ℂ) (hz : ‖z‖ < 1) (w : ℂ)
    (hw : ‖w‖ < 1) (h0 : z * (starRingEnd ℂ w) ≠ 0) :
    ⟪dirichletKernel z hz, dirichletKernel w hw⟫ =
      -Complex.log (1 - z * (starRingEnd ℂ w)) / (z * (starRingEnd ℂ w))

Uses 3

Statement usesReproducing kernel of the Dirichlet space

Proof usesClosed form of \(\sum u^n/(n+1)\) for complex \(u\) in the unit disc · Inner product of two Dirichlet kernels as a power series

TheoremDirichlet kernel evaluated at its own point#✓fully proved

Evaluation of the kernel at its own point: f_z(k_z) = ‖k_z‖².

theorem dirichletEval_dirichletKernel (z : ℂ) (hz : ‖z‖ < 1) :
    dirichletEval z hz (dirichletKernel z hz) =
      ((‖dirichletKernel z hz‖ ^ 2 : ℝ) : ℂ)

Uses 2 · Used by 1

Statement usesPoint evaluation on the Dirichlet space · Reproducing kernel of the Dirichlet space

Used bySharpness of the Dirichlet-space pointwise bound

TheoremSharpness of the Dirichlet-space pointwise bound#✓fully proved

Evaluation of the kernel at its own point, in closed form: f_z(k_z) = -log (1 - ‖z‖²) / ‖z‖², so the pointwise bound is sharp.

theorem dirichletEval_dirichletKernel_of_ne_zero (z : ℂ) (hz : ‖z‖ < 1) (h0 : z ≠ 0) :
    dirichletEval z hz (dirichletKernel z hz) =
      ((-Real.log (1 - ‖z‖ ^ 2) / ‖z‖ ^ 2 : ℝ) : ℂ)

Uses 4

Statement usesPoint evaluation on the Dirichlet space · Reproducing kernel of the Dirichlet space

Proof usesDirichlet kernel evaluated at its own point · Squared norm of the Dirichlet kernel away from the origin

AbbreviationThe Dirichlet space#✓fully proved

The Dirichlet space \(\mathcal{D}\) consists of the functions \(f : \mathbb{C} \to \mathbb{C}\) that are analytic on the open unit disc \(\{z : |z| < 1\}\) and have finite Dirichlet integral: \(|f'|^2\) is integrable on the disc with respect to Lebesgue (area) measure. The values of \(f\) outside the disc are unconstrained.

abbrev DirichletSpace := { f : ℂ → ℂ // AnalyticOn ℂ f (Metric.ball (0 : ℂ) 1) ∧ MeasureTheory.IntegrableOn (fun z => ‖deriv f z‖ ^ 2) (Metric.ball (0 : ℂ) 1) MeasureTheory.volume }

Sources

• AMR-022-8011 (Hayman, Research Problems in Function Theory (2018), Problem 8.11, https://arxiv.org/abs/1809.07200).

Used by 3

Used byHayman's Problem 8.11: polynomial density under domination · Density in the Dirichlet norm · Polynomial multiples of a function in the Dirichlet space

DefinitionPolynomial multiples of a function in the Dirichlet space#✓fully proved

For \(g\) in the Dirichlet space \(\mathcal{D}\), the set \(Pg\) consists of the functions \(h \in \mathcal{D}\) for which there is a polynomial \(p\) with complex coefficients such that \(h(z) = p(z) g(z)\) for all \(|z| < 1\); only values on the open unit disc are compared.

def polyTimes (g : DirichletSpace) : Set DirichletSpace :=
  { h | ∃ p : Polynomial ℂ, ∀ z : ℂ, ‖z‖ < 1 → h.val z = p.eval z * g.val z }

Sources

• AMR-022-8011 (Hayman, Research Problems in Function Theory (2018), Problem 8.11, with \(Pg\) as defined in Problem 8.10), https://arxiv.org/abs/1809.07200.

Uses 1 · Used by 1

Statement usesThe Dirichlet space

Used byHayman's Problem 8.11: polynomial density under domination

DefinitionDensity in the Dirichlet norm#✓fully proved

A set \(S\) of elements of the Dirichlet space \(\mathcal{D}\) is dense in the Dirichlet norm when for every \(u \in \mathcal{D}\) and every real \(\varepsilon > 0\) there is \(h \in S\) with

\[|h(0) - u(0)|^2 + \int_{|z| < 1} |h'(z) - u'(z)|^2 \, dA(z) < \varepsilon,\]

where \(A\) is Lebesgue (area) measure on \(\mathbb{C}\).

def IsDirichletDense (S : Set DirichletSpace) : Prop :=
  ∀ u : DirichletSpace, ∀ ε : ℝ, 0 < ε →
    ∃ h ∈ S, ‖h.val 0 - u.val 0‖ ^ 2 +
      (∫ z in Metric.ball (0 : ℂ) 1, ‖deriv h.val z - deriv u.val z‖ ^ 2
        ∂MeasureTheory.volume) < ε

Uses 1 · Used by 1

Statement usesThe Dirichlet space

Used byHayman's Problem 8.11: polynomial density under domination

DefinitionHayman's Problem 8.11: polynomial density under domination#✓fully proved

The statement that for all \(f\) and \(g\) in the Dirichlet space \(\mathcal{D}\): if the polynomial multiples \(Pg\) are dense in \(\mathcal{D}\) in the Dirichlet norm and \(|g(z)| \le |f(z)|\) for all \(|z| < 1\), then the polynomial multiples \(Pf\) are also dense in \(\mathcal{D}\) in the Dirichlet norm.

def conjecture : Prop :=
  ∀ (g f : DirichletSpace), IsDirichletDense (polyTimes g) → (∀ z : ℂ, ‖z‖ < 1 → ‖g.val z‖ ≤ ‖f.val z‖) → IsDirichletDense (polyTimes f)

Sources

• the open question of AMR-022-8011 (Hayman, Research Problems in Function Theory (2018), Problem 8.11, https://arxiv.org/abs/1809.07200).

Uses 3 · Used by 1

Statement usesThe Dirichlet space · Density in the Dirichlet norm · Polynomial multiples of a function in the Dirichlet space

Used byPolynomial density passes to dominating functions in the Dirichlet space

TheoremPolynomial density passes to dominating functions in the Dirichlet space#●ready to prove

For all \(f\) and \(g\) in the Dirichlet space \(\mathcal{D}\): if the polynomial multiples \(Pg\) are dense in \(\mathcal{D}\) in the Dirichlet norm and \(|g(z)| \le |f(z)|\) for all \(|z| < 1\), then the polynomial multiples \(Pf\) are dense in \(\mathcal{D}\) in the Dirichlet norm. This answers Hayman's Problem 8.11 positively.

Resolved true: Richter and Sundberg (Michigan Math. J. 38 (1991) 355-379), and independently Aleman, proved that in Dirichlet-type spaces \(\mathcal{D}(\mu)\), including the classical Dirichlet space, \(|g| \le |f|\) with \(g\) cyclic implies \(f\) cyclic, where \(g\) is cyclic when \(Pg\) is dense (restated in arXiv:2406.06182, Thm 5.12).

public theorem_wanted conjecture_holds : conjecture

Sources

• Emmanuel Fricain and Romain Lebreton, Cyclicity of the shift operator through Bezout identities, arXiv:2406.06182 (2024), https://arxiv.org/abs/2406.06182.

Uses 1

Statement usesHayman's Problem 8.11: polynomial density under domination

32 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.