Prove2Me

Stability of the planar LpL^p estimate for ∂s+A ∂t\partial_s+A\,\partial_t under perturbation of AA

Proved
JHolomorphic.exists_eLpNorm_fderiv_le_of_norm_sub_lt

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 A:E→EA:E\to E linear with A2=−1A^2=-1. Then there are δ>0\delta>0 and C∈RC\in\mathbb R such that for every linear B:E→EB:E\to E with ∥B−A∥<δ\|B-A\|<\delta and every compactly supported C1C^1 map g:C→Eg:\mathbb C\to E,

∥∂sg∥Lp+∥∂tg∥Lp≤C ∥∂sg+B ∂tg∥Lp.\|\partial_sg\|_{L^p}+\|\partial_tg\|_{L^p}\le C\,\|\partial_sg+B\,\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. The operator BB is not required to satisfy B2=−1B^2=-1. This makes the planar Cauchy–Riemann type estimate locally uniform in the frozen structure.

Formalization Note A : E →L[ℝ] E with A.comp A = -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

/-- Stability of the planar `L^p` estimate for `∂ₛ + A ∂ₜ` (`A² = -1`) under perturbation of
`A`: for `1 < p` there are `δ > 0` and `C` such that for every linear `B : E → E` with
`‖B - A‖ < δ` and every compactly supported `C¹` map `g : ℂ → E`,
`‖∂ₛg‖_p + ‖∂ₜg‖_p ≤ C ‖∂ₛg + B ∂ₜg‖_p`. -/
theorem exists_eLpNorm_fderiv_le_of_norm_sub_lt {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (p : ℝ) (hp : 1 < p) (A : E →L[ℝ] E)
    (hA : A.comp A = -ContinuousLinearMap.id ℝ E) :
    ∃ δ > 0, ∃ C : ℝ, ∀ B : E →L[ℝ] E, ‖B - A‖ < δ → ∀ 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 + B (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