Prove2Me

Uniform interior W2,pW^{2,p} bounds for pseudoholomorphic maps with locally bounded W1,pW^{1,p} norms

Proved
JHolomorphic.exists_eLpNorm_fderiv_fderiv_le

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

elliptic-regularitypseudoholomorphic-curvessobolev-spaces

Let EE be a finite-dimensional real normed space, O⊆EO\subseteq E open, and let JνJ_\nu, JJ be smooth almost complex structures on OO with Jν→JJ_\nu\to J in Cloc∞C^\infty_{\mathrm{loc}} on OO. Let K0⊆OK_0\subseteq O be compact, U⊆CU\subseteq\mathbb{C} open and p>2p>2. Let uν:U→K0u_\nu:U\to K_0 be C∞C^\infty maps with ∂suν+Jν(uν) ∂tuν=0\partial_su_\nu+J_\nu(u_\nu)\,\partial_tu_\nu=0 on UU such that for every compact K⊆UK\subseteq U

sup⁡ν∥Duν∥Lp(K)<∞.\sup_\nu\|Du_\nu\|_{L^p(K)}<\infty.

Then for every compact K⊆UK\subseteq U

sup⁡ν∥D2uν∥Lp(K)<∞.\sup_\nu\|D^2u_\nu\|_{L^p(K)}<\infty.

This is the interior W2,pW^{2,p} part of the uniform regularity statement for sequences of pseudoholomorphic maps; it is used to bound the first derivatives of such sequences uniformly on compact sets.

Formalization Note The structures satisfy IsAlmostComplexOn J O, ∀ ν, IsAlmostComplexOn (Jν ν) O and TendstoCInftyLocOn Jν J O; the maps satisfy ContDiffOn ℝ ∞ (u ν) U, IsJHolomorphicOn (Jν ν) U (u ν) and Set.MapsTo (u ν) U K₀. The norms are eLpNorm (fderiv ℝ (u ν)) (ENNReal.ofReal p) (volume.restrict K) and eLpNorm (fderiv ℝ (fderiv ℝ (u ν))) (ENNReal.ofReal p) (volume.restrict K), in operator norm, bounded by a constant C : ℝ≥0 chosen for each compact K before ν.

Preamble
import Definitions.Def_JHolomorphic_Setting
Formal statement
namespace JHolomorphic

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal NNReal

/-- Uniform interior `L^p` bounds on second derivatives (Wendl, Lecture 2, Theorem 2.22 (2a) with
`k = 1`, the `W^{2,p}_loc` part): let `p > 2` and let `J_ν → J` in `C^∞_loc` be smooth almost
complex structures on an open set `O ⊆ E`. Let `u_ν` be smooth `J_ν`-holomorphic maps on an open set
`U ⊆ ℂ` with values in a fixed compact `K₀ ⊆ O`, such that on every compact `K ⊆ U` the norms
`‖Du_ν‖_{L^p(K)}` are bounded uniformly in `ν`. Then on every compact `K ⊆ U` the norms
`‖D²u_ν‖_{L^p(K)}` are bounded uniformly in `ν`. -/
theorem exists_eLpNorm_fderiv_fderiv_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (p : ℝ) (hp : 2 < p)
    (J : E → E →L[ℝ] E) (Jν : ℕ → E → E →L[ℝ] E) (O K₀ : Set E)
    (hJ : IsAlmostComplexOn J O) (hJν : ∀ ν, IsAlmostComplexOn (Jν ν) O)
    (hconv : TendstoCInftyLocOn Jν J O) (hK₀ : IsCompact K₀) (hK₀O : K₀ ⊆ O)
    (U : Set ℂ) (hU : IsOpen U) (u : ℕ → ℂ → E) (hu : ∀ ν, ContDiffOn ℝ ∞ (u ν) U)
    (hhol : ∀ ν, IsJHolomorphicOn (Jν ν) U (u ν)) (hmaps : ∀ ν, Set.MapsTo (u ν) U K₀)
    (hbd : ∀ K ⊆ U, IsCompact K → ∃ C : ℝ≥0, ∀ ν,
      eLpNorm (fderiv ℝ (u ν)) (ENNReal.ofReal p) (volume.restrict K) ≤ C) :
    ∀ K ⊆ U, IsCompact K → ∃ C : ℝ≥0, ∀ ν,
      eLpNorm (fderiv ℝ (fderiv ℝ (u ν))) (ENNReal.ofReal p) (volume.restrict K) ≤ C := by
  sorry

end JHolomorphic
Source
C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 2, Theorem 2.22 (2a), p. 35 (the case k = 1, interior W^{2,p} part)

View graph