Prove2Me

A uniform planar LpL^p estimate for ∂s+J0 ∂t\partial_s+J_0\,\partial_t over a compact family of complex structures

Proved
JHolomorphic.exists_eLpNorm_fderiv_le_of_isCompact

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

elliptic-regularitypseudoholomorphic-curvessobolev-spaces

Let EE be a finite-dimensional real normed space, p>1p>1, and let SS be a compact set of linear maps J0:E→EJ_0:E\to E with J02=−1J_0^2=-1 for every J0∈SJ_0\in S. Then there is C∈RC\in\mathbb R such that for every J0∈SJ_0\in S and every compactly supported C1C^1 map g:C→Eg:\mathbb C\to E,

∥∂sg∥Lp+∥∂tg∥Lp≤C ∥∂sg+J0 ∂tg∥Lp.\|\partial_sg\|_{L^p}+\|\partial_tg\|_{L^p}\le C\,\|\partial_sg+J_0\,\partial_tg\|_{L^p}.

Here z=s+itz=s+it, ∂sg=Dg(z)1\partial_sg=Dg(z)1 and ∂tg=Dg(z)i\partial_tg=Dg(z)i. This gives one constant for the frozen-coefficient estimate along a whole compact family of complex structures, as needed for uniform estimates on sequences of pseudoholomorphic maps.

Formalization Note S : Set (E →L[ℝ] E) is IsCompact and every J₀ ∈ S satisfies J₀.comp J₀ = -ContinuousLinearMap.id ℝ E; g satisfies ContDiff ℝ 1 g and HasCompactSupport g; the norms are eLpNorm (fun z => fderiv ℝ g z 1) (ENNReal.ofReal p) volume etc., and the constant enters as ENNReal.ofReal C.

Preamble
import Definitions.Def_JHolomorphic_Setting
import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
import Mathlib.MeasureTheory.Function.LpSpace.Indicator
import Mathlib.Analysis.Calculus.FDeriv.Const
import Mathlib.Topology.Compactness.Compact
Formal statement
namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ContDiff ENNReal NNReal

/-- The planar `L^p` estimate for `∂ₛ + J₀ ∂ₜ` holds with one constant for all `J₀` in a compact
set `S` of complex structures on `E` (`J₀² = -1`): for `1 < p` there is `C` such that
`‖∂ₛg‖_p + ‖∂ₜg‖_p ≤ C ‖∂ₛg + J₀ ∂ₜg‖_p` for every `J₀ ∈ S` and every compactly supported `C¹`
map `g : ℂ → E`. -/
theorem exists_eLpNorm_fderiv_le_of_isCompact {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (p : ℝ) (hp : 1 < p) (S : Set (E →L[ℝ] E))
    (hS : IsCompact S) (hSJ : ∀ J₀ ∈ S, J₀.comp J₀ = -ContinuousLinearMap.id ℝ E) :
    ∃ C : ℝ, ∀ J₀ ∈ S, ∀ g : ℂ → E, ContDiff ℝ 1 g → HasCompactSupport g →
      eLpNorm (fun z => fderiv ℝ g z 1) (ENNReal.ofReal p) volume +
          eLpNorm (fun z => fderiv ℝ g z Complex.I) (ENNReal.ofReal p) volume ≤
        ENNReal.ofReal C *
          eLpNorm (fun z => fderiv ℝ g z 1 + J₀ (fderiv ℝ g z Complex.I)) (ENNReal.ofReal p)
            volume := by
  sorry

end JHolomorphic
Source
Frozen-coefficient L^p estimates for the Cauchy-Riemann operator; used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Theorem 2.22

View graph