Documentation

TauCeti.Analysis.Sobolev.Circle.HardyGraph

The nonlinear Hardy graph of a plumbing node #

Let 0 < |a| < 1. The neck of the plumbing xy = a is the annulus |a| ≤ |x| ≤ 1 in the first branch coordinate, with outer boundary circles |x| = 1 and |y| = 1. A holomorphic embedding of the neck into the node zw = b is x ↦ (f(x), b / f(x)) for a nonvanishing holomorphic f of winding number one on the annulus. Its boundary values are ξ = f on |x| = 1 and η(y) = b / f(a / y) on |y| = 1, so they satisfy the node equation ξ(x) η(a / x) = b. The nonlinear Hardy graph theorem says that, near the identity pair (ξ, η) = (x, y), the positive Fourier coefficients of ξ and η are free parameters, and the nonpositive coefficients and b are determined by them, holomorphically in a and the parameters, including at the node a = 0.

This file proves this in exponential coordinates ξ = x e^F, η = y e^G, with F and G in the circle Sobolev space H^s, s > 1/2. In these coordinates the node equation becomes the linear equation F(x) + G(a / x) = F₀ + G₀, with b = a e^{F₀ + G₀}. In Fourier coefficients this says that (F, G) lies in the neck graph CircleSobolev.neckGraph s ℂ a (CircleSobolev.hasSum_zpow_smul_coeff_of_mem_neckGraph); the multiplicative form is CircleSobolev.mul_exp_mul_mul_exp_eq_of_mem_neckGraph. The positive coefficients of ξ = x e^F are the nonnegative coefficients of e^F, shifted by one. So the theorem asks to solve

indicator (Set.Ici 0) (e^F) = 1 + p, indicator (Set.Ici 0) (e^G) = 1 + q, (F, G) ∈ neckGraph s ℂ a

for (F, G) near 0, given a near 0 and nonnegative-frequency p, q near 0. Here e^F is the holomorphic Nemytskii map CircleSobolev.nemytskii exp F.

The neck graph is the graph of the bounded operator CircleSobolev.neckTransfer a over the nonnegative Laurent subspaces, which depends holomorphically on a and vanishes at a = 0. After substituting this parametrization, the equation is a holomorphic equation in a, p, q and the nonnegative parts of F and G, whose derivative in the last two variables at the origin is the identity, because the derivative of e^F at F = 0 is the identity (CircleSobolev.hasFDerivAt_nemytskii_zero). The holomorphic implicit function theorem then gives the solution and its local uniqueness.

Main statements #

References #

theorem TauCeti.CircleSobolev.mul_exp_mul_mul_exp_eq_of_mem_neckGraph {s T : ℝ} [Fact (0 < T)] {a : ℂ} (hs : 1 / 2 < s) (ha₀ : a ≠ 0) {p : CircleSobolev s ℂ × CircleSobolev s ℂ} (hp : p ∈ neckGraph s ℂ a) (x : AddCircle T) :
(fourier 1) x * Complex.exp (((toContinuousMap T hs) p.1) x) * (a / (fourier 1) x * Complex.exp (∑' (n : ℤ), (a / (fourier 1) x) ^ n * p.2.coeff n)) = a * Complex.exp (p.1.coeff 0 + p.2.coeff 0)

The node equation. For s > 1/2, a ≠ 0 and (F, G) in the neck graph, the boundary maps ξ = x e^F on |x| = 1 and η = y e^G on |y| = 1 satisfy ξ(x) η(a / x) = a e^{F₀ + G₀} at every point x = fourier 1 x of the unit circle, where η(a / x) is evaluated through the convergent Laurent series G(a / x) = ∑ₙ (a / x)ⁿ Gₙ.

theorem TauCeti.CircleSobolev.exists_analyticAt_hardyGraph {s : ℝ} [hs : Fact (1 / 2 < s)] :
∃ (ψ : ℂ × ↥(supported s ℂ (Set.Ici 0)) × ↥(supported s ℂ (Set.Ici 0)) → CircleSobolev s ℂ × CircleSobolev s ℂ), ψ 0 = 0 ∧ AnalyticAt ℂ ψ 0 ∧ ∃ W ∈ nhds 0, ∀ᶠ (y : ℂ × ↥(supported s ℂ (Set.Ici 0)) × ↥(supported s ℂ (Set.Ici 0))) in nhds 0, ψ y ∈ W ∧ ∀ p ∈ W, p ∈ neckGraph s ℂ y.1 ∧ (indicator (Set.Ici 0)) (nemytskii Complex.exp p.1) = 1 + ↑y.2.1 ∧ (indicator (Set.Ici 0)) (nemytskii Complex.exp p.2) = 1 + ↑y.2.2 ↔ p = ψ y

The nonlinear Hardy graph theorem at a plumbing node. For s > 1/2 there are a neighbourhood W of 0 in H^s × H^s and a map ψ, analytic at the origin with ψ 0 = 0, such that for all data y = (a, p, q) near 0, with p and q of nonnegative frequencies, ψ y is the unique (F, G) ∈ W with

  • (F, G) in the neck graph of the plumbing xy = a, and
  • nonnegative parts of e^F and e^G equal to 1 + p and 1 + q.

In terms of the boundary maps ξ = x e^F and η = y e^G, the conditions say that (ξ, η) solves the node equation ξ(x) η(a / x) = b with b = a e^{F₀ + G₀} (CircleSobolev.mul_exp_mul_mul_exp_eq_of_mem_neckGraph), and that the positive Fourier coefficients of ξ and η are those of x (1 + p) and y (1 + q). So the solution, its nonpositive coefficients and b depend holomorphically on a and on these positive coefficients, also at the node a = 0.