Bergman space

TheoremSquare of the complex geometric series#✓fully proved

The Cauchy product of the geometric series with itself: the series ∑' n, (n + 1) * qⁿ sums to (1 - q)⁻¹ ^ 2.

theorem hasSum_succ_mul_pow_complex {q : ℂ} (hq : ‖q‖ < 1) :
    HasSum (fun n : ℕ => ((n : ℂ) + 1) * q ^ n) ((1 - q)⁻¹ ^ 2)

Used by 1

Used byInner product of two Bergman kernels

TheoremSquare of the real geometric series#✓fully proved

The real form of the Cauchy product above.

theorem hasSum_succ_mul_pow_real {r : ℝ} (h0 : 0 ≤ r) (h1 : r < 1) :
    HasSum (fun n : ℕ => ((n : ℝ) + 1) * r ^ n) ((1 - r)⁻¹ ^ 2)

Used by 2

Used byBergman kernel coefficients are square-summable · Squared norm of the Bergman kernel

TheoremSquared norms of the Bergman kernel coefficients#✓fully proved

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

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

Used by 2

Used byBergman kernel coefficients are square-summable · Squared norm of the Bergman kernel

TheoremBergman kernel coefficients are square-summable#✓fully proved

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

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

Uses 2 · Used by 1

Proof usesSquare of the real geometric series · Squared norms of the Bergman kernel coefficients

Used byBergman kernel

DefinitionBergman kernel#✓fully proved

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

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

Uses 1 · Used by 13

Statement usesBergman kernel coefficients are square-summable

Used byPoint evaluation on the Bergman space · Bergman kernel evaluated at its own point · Bounded point-evaluation functional on the Bergman space · Bergman point evaluation as a Taylor series · Bergman evaluation of a monomial · Bergman evaluation at the origin · Bergman kernel at the origin · Inner product of two Bergman kernels · Reproducing property of the Bergman kernel, conjugate form · Operator norm of Bergman point evaluation · Norm of the Bergman kernel · Squared norm of the Bergman kernel · Convergence of the Taylor series of a Bergman space function

TheoremBergman kernel at the origin#✓fully proved

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

theorem bergmanKernel_zero (hz : ‖(0 : ℂ)‖ < 1) :
    bergmanKernel 0 hz = lp.single 2 0 (1 : ℂ)

Uses 1 · Used by 1

Statement usesBergman kernel

Used byBergman evaluation at the origin

TheoremSquared norm of the Bergman kernel#✓fully proved

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

theorem norm_sq_bergmanKernel (z : ℂ) (hz : ‖z‖ < 1) :
    ‖bergmanKernel z hz‖ ^ 2 = 1 / (1 - ‖z‖ ^ 2) ^ 2

Uses 3 · Used by 1

Statement usesBergman kernel

Proof usesSquare of the real geometric series · Squared norms of the Bergman kernel coefficients

Used byNorm of the Bergman kernel

TheoremNorm of the Bergman kernel#✓fully proved

The norm of the Bergman kernel is 1 / (1 - ‖z‖²).

theorem norm_bergmanKernel (z : ℂ) (hz : ‖z‖ < 1) :
    ‖bergmanKernel z hz‖ = 1 / (1 - ‖z‖ ^ 2)

Uses 2 · Used by 1

Statement usesBergman kernel

Proof usesSquared norm of the Bergman kernel

Used byOperator norm of Bergman point evaluation

DefinitionPoint evaluation on the Bergman space#✓fully proved

Point evaluation on A²(𝔻): the inner product with the Bergman kernel.

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

Uses 1 · Used by 7

Statement usesBergman kernel

Used byBergman kernel evaluated at its own point · Bergman point evaluation is the inner product with the kernel · Bergman point evaluation as a Taylor series · Bergman evaluation of a monomial · Bergman evaluation at the origin · Reproducing property of the Bergman kernel, conjugate form · Pointwise bound for Bergman space functions

TheoremBergman point evaluation as a Taylor series#✓fully proved

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

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

Uses 2

Statement usesPoint evaluation on the Bergman space

Proof usesBergman kernel

TheoremConvergence of the Taylor series of a Bergman space function#✓fully proved

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

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

Uses 1

Proof usesBergman kernel

DefinitionBounded point-evaluation functional on the Bergman space#✓fully proved

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

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

Uses 1 · Used by 3

Statement usesBergman kernel

Used byBergman point evaluation is the inner product with the kernel · Operator norm of Bergman point evaluation · Pointwise bound for Bergman space functions

TheoremBergman point evaluation is the inner product with the kernel#✓fully proved

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

theorem bergmanEvalCLM_apply (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    bergmanEvalCLM z hz a = bergmanEval z hz a

Uses 2 · Used by 1

Statement usesPoint evaluation on the Bergman space · Bounded point-evaluation functional on the Bergman space

Used byPointwise bound for Bergman space functions

TheoremOperator norm of Bergman point evaluation#✓fully proved

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

theorem norm_bergmanEvalCLM (z : ℂ) (hz : ‖z‖ < 1) :
    ‖bergmanEvalCLM z hz‖ = 1 / (1 - ‖z‖ ^ 2)

Uses 3 · Used by 1

Statement usesBounded point-evaluation functional on the Bergman space

Proof usesBergman kernel · Norm of the Bergman kernel

Used byPointwise bound for Bergman space functions

TheoremPointwise bound for Bergman space functions#✓fully proved

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

theorem norm_bergmanEval_le (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    ‖bergmanEval z hz a‖ ≤ ‖a‖ / (1 - ‖z‖ ^ 2)

Uses 4

Statement usesPoint evaluation on the Bergman space

Proof usesBounded point-evaluation functional on the Bergman space · Bergman point evaluation is the inner product with the kernel · Operator norm of Bergman point evaluation

TheoremBergman evaluation at the origin#✓fully proved

Evaluation at 0 is the constant Taylor coefficient.

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

Uses 3

Statement usesPoint evaluation on the Bergman space

Proof usesBergman kernel · Bergman kernel at the origin

TheoremBergman evaluation of a monomial#✓fully proved

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

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

Uses 2

Statement usesPoint evaluation on the Bergman space

Proof usesBergman kernel

TheoremReproducing property of the Bergman kernel, conjugate form#✓fully proved

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

theorem inner_bergmanKernel_right (z : ℂ) (hz : ‖z‖ < 1) (a : ℓ²(ℕ, ℂ)) :
    ⟪a, bergmanKernel z hz⟫ = (starRingEnd ℂ) (bergmanEval z hz a)

Uses 2

Statement usesPoint evaluation on the Bergman space · Bergman kernel

TheoremInner product of two Bergman kernels#✓fully proved

The inner product of two Bergman kernels is the Bergman kernel function (1 - z * conj w)⁻¹ ^ 2.

theorem inner_bergmanKernel_bergmanKernel (z : ℂ) (hz : ‖z‖ < 1) (w : ℂ)
    (hw : ‖w‖ < 1) :
    ⟪bergmanKernel z hz, bergmanKernel w hw⟫ = (1 - z * (starRingEnd ℂ w))⁻¹ ^ 2

Uses 2 · Used by 1

Statement usesBergman kernel

Proof usesSquare of the complex geometric series

Used byBergman kernel evaluated at its own point

TheoremBergman kernel evaluated at its own point#✓fully proved

Evaluation of the kernel at its own point: f_z(k_z) = (1 - ‖z‖²)⁻¹ ^ 2, so the pointwise bound is sharp.

theorem bergmanEval_bergmanKernel (z : ℂ) (hz : ‖z‖ < 1) :
    bergmanEval z hz (bergmanKernel z hz) = ((1 - ‖z‖ ^ 2 : ℝ) : ℂ)⁻¹ ^ 2

Uses 3

Statement usesPoint evaluation on the Bergman space · Bergman kernel

Proof usesInner product of two Bergman kernels

DefinitionRescaled Bergman monomial#✓fully proved

The rescaled monomial eₙ(z) = √(n + 1) zⁿ for normalized area measure dA / π, represented by the nth standard basis vector in the coefficient model.

noncomputable def bergmanMonomial (n : ℕ) : ℓ²(ℕ, ℂ) :=
  lp.single 2 n (1 : ℂ)

Used by 1

Used byRescaled Bergman monomials are orthonormal

TheoremInner products of rescaled Bergman monomials are Kronecker deltas#✓fully proved

The coordinate inner products of the rescaled monomials equal the Kronecker delta.

theorem bergmanMonomial_orthonormal (m n : ℕ) :
    ⟪(lp.single 2 m (1 : ℂ) : ℓ²(ℕ, ℂ)), (lp.single 2 n (1 : ℂ) : ℓ²(ℕ, ℂ))⟫_ℂ =
      if m = n then (1 : ℂ) else 0

Used by 1

Used byRescaled Bergman monomials are orthonormal

TheoremRescaled Bergman monomials are orthonormal#✓fully proved

The rescaled monomial family satisfies Mathlib's standard orthonormal predicate.

theorem orthonormal_bergmanMonomial : Orthonormal ℂ bergmanMonomial

Uses 2

Statement usesRescaled Bergman monomial

Proof usesInner products of rescaled Bergman monomials are Kronecker deltas

TheoremBergman coefficients as inner products with monomials#✓fully proved

The coefficient of a at n is the inner product with eₙ.

theorem bergmanCoeff_eq_inner (a : ℓ²(ℕ, ℂ)) (n : ℕ) :
    a n = ⟪lp.single 2 n (1 : ℂ), a⟫

DefinitionThe open unit disc#✓fully proved

The set \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\).

def Disc : Set ℂ := {z | ‖z‖ < 1}

Used by 3

Used byBergman space \(A^2\) of the unit disc · Bergman cyclicity conjecture · Density of polynomial multiples in \(A^2\)

DefinitionBergman space \(A^2\) of the unit disc#✓fully proved

A function \(f : \mathbb{C} \to \mathbb{C}\) belongs to the Bergman space \(A^2\) when it is analytic on the open unit disc \(\mathbb{D} = \{z \in \mathbb{C} : |z| < 1\}\) and square-integrable on \(\mathbb{D}\) with respect to Lebesgue area measure \(dA\): \(f\) is almost everywhere strongly measurable on \(\mathbb{D}\) and \(\int_{\mathbb{D}} |f|^2 \, dA < \infty\).

def Bergman (f : ℂ → ℂ) : Prop :=
  AnalyticOn ℂ f Disc ∧ MemLp f 2 (volume.restrict Disc)

Uses 1 · Used by 2

Statement usesThe open unit disc

Used byBergman cyclicity conjecture · Density of polynomial multiples in \(A^2\)

DefinitionPointwise reciprocal#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\), the function \(z \mapsto f(z)^{-1}\), with the convention \(0^{-1} = 0\) at the zeros of \(f\).

noncomputable def Inv (f : ℂ → ℂ) : ℂ → ℂ := fun z => (f z)⁻¹

Used by 1

Used byBergman cyclicity conjecture

DefinitionDensity of polynomial multiples in \(A^2\)#✓fully proved

Write \(\mathbb{D}\) for the open unit disc and \(dA\) for Lebesgue area measure on it. For a function \(f : \mathbb{C} \to \mathbb{C}\), the statement that the polynomial multiples of \(f\) are dense in the Bergman space \(A^2\): for every \(g \in A^2\) and every \(\varepsilon > 0\) there is a complex polynomial \(p\) with \(\left(\int_{\mathbb{D}} |p f - g|^2 \, dA\right)^{1/2} < \varepsilon\).

def Dense (f : ℂ → ℂ) : Prop :=
  ∀ g : ℂ → ℂ, Bergman g → ∀ ε : ENNReal, 0 < ε →
    ∃ p : Polynomial ℂ, eLpNorm (fun z => p.eval z * f z - g z) 2 (volume.restrict Disc) < ε

Uses 2 · Used by 1

Statement usesBergman space \(A^2\) of the unit disc · The open unit disc

Used byBergman cyclicity conjecture

DefinitionBergman cyclicity conjecture#✓fully proved

Write \(\mathbb{D}\) for the open unit disc and \(dA\) for Lebesgue area measure on it. The statement that for every function \(f : \mathbb{C} \to \mathbb{C}\) with no zeros in \(\mathbb{D}\) such that \(f\) and its pointwise reciprocal \(1/f\) both belong to the Bergman space \(A^2\), the polynomial multiples of \(f\) are dense in \(A^2\): for every \(g \in A^2\) and every \(\varepsilon > 0\) there is a complex polynomial \(p\) with \(\left(\int_{\mathbb{D}} |p f - g|^2 \, dA\right)^{1/2} < \varepsilon\).

def conjecture : Prop :=
  ∀ f : ℂ → ℂ, Bergman f → Bergman (Inv f) →
    (∀ z ∈ Disc, f z ≠ 0) → Dense f

Sources

• record AMR-022-8010; the record's generalization to other spaces is not part of this statement.

Uses 4 · Used by 1

Statement usesBergman space \(A^2\) of the unit disc · Density of polynomial multiples in \(A^2\) · The open unit disc · Pointwise reciprocal

Used byInvertible non-cyclic functions in the Bergman space \(A^2\)

TheoremInvertible non-cyclic functions in the Bergman space \(A^2\)#●ready to prove

Write \(\mathbb{D}\) for the open unit disc and \(dA\) for Lebesgue area measure on it. There is a function \(f : \mathbb{C} \to \mathbb{C}\) with no zeros in \(\mathbb{D}\) such that \(f\) and its pointwise reciprocal \(1/f\) both belong to the Bergman space \(A^2\), but the polynomial multiples of \(f\) are not dense in \(A^2\): there are \(g \in A^2\) and \(\varepsilon > 0\) with \(\left(\int_{\mathbb{D}} |p f - g|^2 \, dA\right)^{1/2} \ge \varepsilon\) for every complex polynomial \(p\). That is, the Bergman cyclicity conjecture is false.

Borichev and Hedenmalm (J. Amer. Math. Soc. 10 (1997) 761-796) constructed invertible but non-cyclic functions in the unweighted Bergman spaces \(B^p(\mathbb{D})\), \(0 < p < \infty\); the case \(p = 2\) gives such an \(f\), as stated in Borichev-Hedenmalm-Volberg (arXiv:math/0304318).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Alexander Borichev, Haakan Hedenmalm and Alexander Volberg, Large Bergman spaces: invertibility, cyclicity, and subspaces of arbitrary index, arXiv:math/0304318 (2003), https://arxiv.org/abs/math/0304318.

Uses 1

Statement usesBergman cyclicity conjecture

29 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.