Prove2Me

Elements of W1,2(S1,R2n)W^{1,2}(S^1,\mathbb{R}^{2n}) have continuous representatives

Proved
AsymptoticOperator.exists_continuous_of_inW12

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

asymptotic-operatorfourier-analysissobolev-spaces

Let f∈L2(S1,R2n)f\in L^2(S^1,\mathbb{R}^{2n}), S1=R/ZS^1=\mathbb{R}/\mathbb{Z} with its Haar probability measure, and let f^k=∫S1e−2πiktf(t) dt∈C2n\hat f_k=\int_{S^1}e^{-2\pi i k t}f(t)\,dt\in\mathbb{C}^{2n} be its Fourier coefficients. If

∑k∈Z(1+k2) ∣f^k∣2<∞,\sum_{k\in\mathbb{Z}}(1+k^2)\,|\hat f_k|^2<\infty,

i.e. f∈W1,2(S1,R2n)f\in W^{1,2}(S^1,\mathbb{R}^{2n}), then there is a continuous map φ:S1→R2n\varphi:S^1\to\mathbb{R}^{2n} with f=φf=\varphi almost everywhere.

This is the one-dimensional Sobolev embedding W1,2(S1)⊂C0(S1)W^{1,2}(S^1)\subset C^0(S^1) in the Fourier-coefficient description of W1,2W^{1,2} used for asymptotic operators. It lets elements of the domain of AS=−J0∂t−SA_S=-J_0\partial_t-S be evaluated pointwise, for instance to compare kernel elements with solutions of the linear equation x˙=J0Sx\dot x=J_0Sx.

Formalization Note. L2 n is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle on UnitAddCircle, and InW12 f is the summability over ℤ of (1 + k²) * ∑ i, ‖coeff f k i‖², where coeff f k is fourierCoeff of the complexified representative (setting module). The conclusion is ∃ φ : C(UnitAddCircle, Vec n), ⇑f =ᵐ[haarAddCircle] ⇑φ.

Preamble
import Definitions.Def_AsymptoticOperator_Setting
Formal statement
namespace AsymptoticOperator

/-- Every element of `W^{1,2}(S¹, ℝ²ⁿ)` has a continuous representative: if `f ∈ L²` satisfies
`∑ₖ (1 + k²) |f̂ₖ|² < ∞`, then `f` agrees almost everywhere with a continuous loop. -/
theorem exists_continuous_of_inW12 {n : ℕ} (f : L2 n) (hf : InW12 f) :
    ∃ φ : C(UnitAddCircle, Vec n),
      (f : UnitAddCircle → Vec n) =ᵐ[AddCircle.haarAddCircle] (φ : UnitAddCircle → Vec n) := by
  sorry

end AsymptoticOperator
Source
Auxiliary statement for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 3, §3.4 p. 61 (kernel of the asymptotic operator)

View graph