Holomorphic Nemytskii maps on the circle Sobolev spaces

For s > 1/2 the Fourier-coefficient Sobolev space H^s of the circle consists of continuous functions and is an algebra. This file shows that it is also stable under holomorphic functions: if F is holomorphic on an open set U ⊆ ℂ and u ∈ H^s takes values in U, then F ∘ u lies in H^s, and the Nemytskii map u ↦ F ∘ u is holomorphic on the open set of such u. These are the nonlinear maps of boundary values used in the Hardy decompositions of cut Riemann surfaces, for instance products and quotients of nonvanishing boundary maps.

The proof expands F in Taylor series around a nearby trigonometric polynomial p. A trigonometric polynomial extends to an entire periodic function, which maps a thin strip around the real axis close to the values of p. Composed with the derivatives F^{(k)}, it stays holomorphic and, by Cauchy's estimates, bounded by k! M / ε ^ k on that strip, so the Fourier coefficients of F^{(k)} ∘ p decay exponentially (TauCeti.norm_fourierCoeff_le_of_differentiableOn_strip) and ‖F^{(k)} ∘ p‖_{H^s} ≤ k! B / ε ^ k. The product estimate of H^s then makes ∑ₖ (k!)⁻¹ (F^{(k)} ∘ p) (u - p) ^ k converge in H^s for u near p, to F ∘ u, and the same series is a power series expansion of the Nemytskii map around p.

Main definitions

• TauCeti.CircleSobolev.nemytskii F u: the element of H^s whose continuous representative is F ∘ u, when there is one (and 0 otherwise).

Main statements

• TauCeti.CircleSobolev.exists_toContinuousMap_eq_of_differentiableOn_strip: a function on the circle extending to a periodic function holomorphic and bounded on a strip lies in every H^s, s > 1/2, with an explicit norm bound.
• TauCeti.CircleSobolev.toContinuousMap_nemytskii: for F holomorphic on an open set U and u ∈ H^s with values in U, the continuous representative of nemytskii F u is F ∘ u.
• TauCeti.CircleSobolev.analyticOnNhd_nemytskii: the map nemytskii F is analytic on the open set of u ∈ H^s with values in U.
• TauCeti.CircleSobolev.hasFDerivAt_nemytskii: its derivative at u is multiplication by F' ∘ u; at u = 0 it is multiplication by the scalar F'(0) (TauCeti.CircleSobolev.hasFDerivAt_nemytskii_zero).

References

• Y. Katznelson, An Introduction to Harmonic Analysis, 3rd ed., Cambridge University Press, 2004, Chapter I (Fourier coefficients of functions holomorphic in a strip).
• M. E. Taylor, Partial Differential Equations III, Chapter 13, Section 3 (Sobolev spaces as algebras and their stability under smooth functions).
• J. W. Robbin and D. A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699 (nonlinear maps of boundary Sobolev spaces in Hardy decompositions).

theorem TauCeti.CircleSobolev.exists_toContinuousMap_eq_of_differentiableOn_strip {s : ℝ} (T : ℝ) [hT : Fact (0 < T)] (hs : 1 / 2 < s) (f : C(AddCircle T, ℂ)) {g : ℂ → ℂ} {δ M : ℝ} (hδ : 0 < δ) (hfg : ∀ (x : ℝ), f ↑x = g ↑x) (hper : ∀ (z : ℂ), |z.im| ≤ δ → g (z + ↑T) = g z) (hg : DifferentiableOn ℂ g {z : ℂ | |z.im| ≤ δ}) (hM : ∀ (z : ℂ), |z.im| ≤ δ → ‖g z‖ ≤ M) : ∃ (w : CircleSobolev s ℂ), (toContinuousMap T hs) w = f ∧ ‖w‖ ≤ M * √(∑' (n : ℤ), weight (2 * s) n * Real.exp (-(4 * Real.pi * δ / T * |↑n|)))

Functions holomorphic in a strip lie in every H^s. A continuous function f on AddCircle T which is the restriction of a T-periodic function g, holomorphic and bounded by M on the closed strip |Im z| ≤ δ, is the continuous representative of an element of H^s, s > 1/2, of norm at most M (∑ₙ (1 + |n|) ^ (2 s) e^{-4πδ|n|/T}) ^ (1/2).

Trigonometric polynomials in a strip

The Nemytskii map

noncomputable def TauCeti.CircleSobolev.nemytskii {s : ℝ} [hs : Fact (1 / 2 < s)] (F : ℂ → ℂ) (u : CircleSobolev s ℂ) : CircleSobolev s ℂ

The Nemytskii map of F : ℂ → ℂ on H^s, s > 1/2: it sends u to the element of H^s whose continuous representative is F ∘ u, if there is one, and to 0 otherwise. The composition is tested on the circle AddCircle 1; it does not depend on the length of the circle (nemytskii_eq_of_forall_toContinuousMap_apply). For F holomorphic on an open set containing the values of u, the composition F ∘ u always lies in H^s (toContinuousMap_nemytskii).

theorem TauCeti.CircleSobolev.nemytskii_eq_of_forall_toContinuousMap_apply {s : ℝ} (T : ℝ) [hT : Fact (0 < T)] [hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} {u w : CircleSobolev s ℂ} (h : ∀ (x : AddCircle T), ((toContinuousMap T ⋯) w) x = F (((toContinuousMap T ⋯) u) x)) : nemytskii F u = w

The Nemytskii map is determined by continuous representatives: if the continuous representative of w ∈ H^s is F ∘ u on some circle, then nemytskii F u = w.

theorem TauCeti.CircleSobolev.toContinuousMap_nemytskii {s : ℝ} (T : ℝ) [hT : Fact (0 < T)] [hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) {u : CircleSobolev s ℂ} (hu : ∀ (x : AddCircle T), ((toContinuousMap T ⋯) u) x ∈ U) (x : AddCircle T) : ((toContinuousMap T ⋯) (nemytskii F u)) x = F (((toContinuousMap T ⋯) u) x)

Holomorphic functions act on H^s, s > 1/2. If F is holomorphic on an open set U and the continuous representative of u ∈ H^s takes values in U, then F ∘ u is the continuous representative of nemytskii F u ∈ H^s.

theorem TauCeti.CircleSobolev.analyticOnNhd_nemytskii {s : ℝ} (T : ℝ) [hT : Fact (0 < T)] [hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) : AnalyticOnNhd ℂ (nemytskii F) {u : CircleSobolev s ℂ | ∀ (x : AddCircle T), ((toContinuousMap T ⋯) u) x ∈ U}

The holomorphic Nemytskii map is holomorphic. If F is holomorphic on an open set U, then u ↦ nemytskii F u is analytic on the open subset of H^s, s > 1/2, of elements with values in U (isOpen_setOf_forall_toContinuousMap_mem).

theorem TauCeti.CircleSobolev.analyticAt_nemytskii {s : ℝ} [hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} (hF : Differentiable ℂ F) (u : CircleSobolev s ℂ) : AnalyticAt ℂ (nemytskii F) u

The Nemytskii map of an entire function is analytic on all of H^s, s > 1/2.

@[simp]

theorem TauCeti.CircleSobolev.nemytskii_zero {s : ℝ} [hs : Fact (1 / 2 < s)] (F : ℂ → ℂ) : nemytskii F 0 = (single 0) (F 0)

The Nemytskii map of any F sends the zero function to the constant function F 0.

theorem TauCeti.CircleSobolev.hasFDerivAt_nemytskii {s : ℝ} (T : ℝ) [hT : Fact (0 < T)] [hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) {u : CircleSobolev s ℂ} (hu : ∀ (x : AddCircle T), ((toContinuousMap T ⋯) u) x ∈ U) : HasFDerivAt (nemytskii F) ((convolution ⋯ (ContinuousLinearMap.mul ℂ ℂ)) (nemytskii (deriv F) u)) u

The derivative of the holomorphic Nemytskii map. If F is holomorphic on an open set U and u ∈ H^s takes values in U, then the derivative of nemytskii F at u is multiplication by nemytskii (deriv F) u, the element of H^s with continuous representative F' ∘ u.

theorem TauCeti.CircleSobolev.hasFDerivAt_nemytskii_zero {s : ℝ} [hs : Fact (1 / 2 < s)] {F : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) (h₀ : 0 ∈ U) : HasFDerivAt (nemytskii F) (deriv F 0 • ContinuousLinearMap.id ℂ (CircleSobolev s ℂ)) 0

At the zero function, the derivative of the Nemytskii map of F is multiplication by the scalar F'(0).