Prove2Me

Weak solutions of −J0∂t-J_0\partial_t on L2(S1,R2n)L^2(S^1,\mathbb{R}^{2n}) lie in W1,2W^{1,2}

Proved
AsymptoticOperator.inW12_of_forall_inner

by Mazecto · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

asymptotic-operatorconley-zehnder-indexfourier-seriesunbounded-operator

Let S1=R/ZS^1=\mathbb R/\mathbb Z with its Haar probability measure and let Ln2=L2(S1,R2n)L^2_n=L^2(S^1,\mathbb R^{2n}) with inner product ⟨f,g⟩L2=∫S1⟨f(t),g(t)⟩ dt\langle f,g\rangle_{L^2}=\int_{S^1}\langle f(t),g(t)\rangle\,dt. For f∈Ln2f\in L^2_n and k∈Zk\in\mathbb Z let f^k=∫S1e−2πiktf(t) dt∈C2n\hat f_k=\int_{S^1}e^{-2\pi ikt}f(t)\,dt\in\mathbb C^{2n} be its kk-th Fourier coefficient, computed componentwise after viewing the real entries of ff as complex numbers. Let W1,2={f∈Ln2:∑k(1+k2)∣f^k∣2<∞}W^{1,2}=\{f\in L^2_n:\sum_k(1+k^2)|\hat f_k|^2<\infty\} and let J0=(0−II0)J_0=\begin{pmatrix}0&-I\\ I&0\end{pmatrix}.

Let g,u∈Ln2g,u\in L^2_n. Suppose that for every f∈W1,2f\in W^{1,2} and every p∈Ln2p\in L^2_n with p^k=−2πik J0f^k\hat p_k=-2\pi ik\,J_0\hat f_k for all kk (that is, p=−J0f′p=-J_0f'),

⟨p,g⟩L2=⟨f,u⟩L2.\langle p,g\rangle_{L^2}=\langle f,u\rangle_{L^2}.

Then g∈W1,2g\in W^{1,2} and u^k=−2πik J0g^k\hat u_k=-2\pi ik\,J_0\hat g_k for every k∈Zk\in\mathbb Z, that is, u=−J0g′u=-J_0g'.

In other words, the operator −J0∂t-J_0\partial_t with domain W1,2W^{1,2} is self-adjoint on L2(S1,R2n)L^2(S^1,\mathbb R^{2n}): every weak solution of −J0g′=u-J_0g'=u with g,u∈L2g,u\in L^2 is a strong one. This is the first-order part of the self-adjointness of the asymptotic operator AS=−J0∂t−SA_S=-J_0\partial_t-S.

Formalization note: L2 n, coeff and InW12 come from the definition module AsymptoticOperator_Setting; coeff f k is f^k\hat f_k, InW12 f means f∈W1,2f\in W^{1,2}, J₀ n is J0J_0 (mapped entrywise into C\mathbb C), and inner ℝ is the L2L^2 inner product.

Preamble
import Definitions.Def_AsymptoticOperator_Setting
Formal statement
namespace AsymptoticOperator

open Matrix ConleyZehnder

/-- Weak solutions of `-J₀ ∂ₜ` on the circle are strong: if `g, u ∈ L²(S¹, ℝ²ⁿ)` satisfy
`⟨-J₀ f', g⟩_{L²} = ⟨f, u⟩_{L²}` for every `f ∈ W^{1,2}(S¹, ℝ²ⁿ)` (with `p = -J₀ f'` given by
its Fourier coefficients `p̂ₖ = -2πik J₀ f̂ₖ`), then `g ∈ W^{1,2}` and `u = -J₀ g'`. -/
theorem inW12_of_forall_inner {n : ℕ} (g u : L2 n)
    (h : ∀ f p : L2 n, InW12 f →
      (∀ k : ℤ, coeff p k =
        -((2 * Real.pi * k : ℝ) * Complex.I) • ((J₀ n).map (fun x : ℝ => (x : ℂ)) *ᵥ coeff f k)) →
      inner ℝ p g = inner ℝ f u) :
    InW12 g ∧ ∀ k : ℤ, coeff u k =
      -((2 * Real.pi * k : ℝ) * Complex.I) • ((J₀ n).map (fun x : ℝ => (x : ℂ)) *ᵥ coeff g k) := by
  sorry

end AsymptoticOperator
Source
Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, §3.2, equation (3.4), p. 55; Hofer-Wysocki-Zehnder (GAFA 1995), §3

View graph