Prove2Me

L1→L∞L^1\to L^\infty bound for weak periodic solutions of a nondegenerate asymptotic operator

Proved
CauchyRiemannIndex.periodic_weak_solution_bound

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

cauchy-riemannelliptic-regularitysymplectic-geometryweak-solutions

Let S∞:R→R2n×2nS_\infty:\mathbb R\to\mathbb R^{2n\times2n} be a continuous 11-periodic loop of symmetric matrices whose asymptotic operator A=−J0∂t−S∞(t)A=-J_0\partial_t-S_\infty(t) is nondegenerate, and let J0=(0−IdId0)J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}. Then there is a constant CC, depending only on S∞S_\infty, with the following property. Let η,f:R→R2n\eta,f:\mathbb R\to\mathbb R^{2n} be integrable on [0,1)[0,1), and suppose η\eta is a weak periodic solution of J0η′+S∞η=fJ_0\eta'+S_\infty\eta=f, that is,

∫01⟨J0ψ′(t)+S∞(t)ψ(t), η(t)⟩ dt=∫01⟨ψ(t), f(t)⟩ dt\int_0^1\big\langle J_0\psi'(t)+S_\infty(t)\psi(t),\ \eta(t)\big\rangle\,dt=\int_0^1\big\langle\psi(t),\ f(t)\big\rangle\,dt

for every smooth 11-periodic ψ:R→R2n\psi:\mathbb R\to\mathbb R^{2n}. Then

∣η(t)∣≤C∫01∣f(τ)∣ dτfor almost every t∈[0,1).|\eta(t)|\le C\int_0^1|f(\tau)|\,d\tau\qquad\text{for almost every }t\in[0,1).

This is an L1→L∞L^1\to L^\infty estimate for the periodic problem of the asymptotic operator (Wendl (3.10)). It is applied to the slices t↦u(s,t)t\mapsto u(s,t) of maps on the cylinder R×S1\mathbb R\times S^1 in the analysis of the translation-invariant Cauchy–Riemann operator ∂s+J0∂t+S∞(t)\partial_s+J_0\partial_t+S_\infty(t) (Wendl, Theorem 4.11).

Formalization Note. R2n\mathbb R^{2n} is EuclideanSpace ℝ (Fin n ⊕ Fin n), J0J_0 is Matrix.J, and matrices act through Matrix.toEuclideanLin. The loop is IsSymLoop (continuous, 11-periodic, symmetric values); nondegeneracy is IsNondegenerate (det⁡(1−Ψ(1))≠0\det(1-\Psi(1))\ne0 for the fundamental solution Ψ′=J0S∞Ψ\Psi'=J_0S_\infty\Psi, Ψ(0)=1\Psi(0)=1). Integrals over [0,1)[0,1) are Bochner integrals for Lebesgue measure restricted to Set.Ico 0 1, ψ′\psi' is deriv ψ, and the conclusion is an almost-everywhere statement for that restricted measure. The constant CC is chosen before η\eta and ff.

Preamble
import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Integral.IntegrableOn
Formal statement
namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Let `S∞` be a nondegenerate loop of symmetric matrices. There is a constant `C` with the
following property. If `η, f : ℝ → ℝ²ⁿ` are integrable on `[0, 1)` and `η` is a weak periodic
solution of `J₀ η' + S∞(t) η = f`, meaning that
`∫₀¹ ⟨J₀ ψ' + S∞ ψ, η⟩ dt = ∫₀¹ ⟨ψ, f⟩ dt` for every smooth `1`-periodic `ψ : ℝ → ℝ²ⁿ`, then
`|η(t)| ≤ C ∫₀¹ |f|` for almost every `t ∈ [0, 1)`.

This is an `L¹ → L^∞` bound for the periodic problem of the asymptotic operator
`-J₀ ∂ₜ - S∞`, used for slices `t ↦ u(s, t)` of sections of the cylinder. -/
theorem periodic_weak_solution_bound (n : ℕ) (Sinf : ℝ → Mat n) (hS : IsSymLoop Sinf)
    (hnd : IsNondegenerate Sinf) :
    ∃ C : ℝ, ∀ η f : ℝ → Vec n, IntegrableOn η (Set.Ico 0 1) → IntegrableOn f (Set.Ico 0 1) →
      (∀ ψ : ℝ → Vec n, ContDiff ℝ ∞ ψ → Function.Periodic ψ 1 →
        ∫ t in Set.Ico (0 : ℝ) 1, inner ℝ (Matrix.toEuclideanLin (J₀ n) (deriv ψ t) +
          Matrix.toEuclideanLin (Sinf t) (ψ t)) (η t) =
        ∫ t in Set.Ico (0 : ℝ) 1, inner ℝ (ψ t) (f t)) →
      ∀ᵐ t ∂(volume.restrict (Set.Ico (0 : ℝ) 1)), ‖η t‖ ≤ C * ∫ t in Set.Ico (0 : ℝ) 1, ‖f t‖ := by
  sorry

end CauchyRiemannIndex
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 3, (3.10) (asymptotic operators) and Lecture 4, Theorem 4.11, p. 71 (setting of the translation-invariant operator)

View graph