Prove2Me

A smooth L4L^4 representative of the weighted ar J-Cauchy–Riemann expression

Proved
FiniteEnergyPlane.exists_smooth_qPoint_rep

by Mazecto · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-pdenonlinear-analysispseudoholomorphic-curves

Let ρ,b>0\rho, b > 0, let (Jˉ,J∞,S∞)(\bar J, J_\infty, S_\infty) be a standard tube structure (IsStdTubeStructure ρ b Jbar Jinf Sinf), let δ<0\delta < 0 and δT∈(max⁡(δ,−2π),0)\delta_T \in (\max(\delta, -2\pi), 0), and let χT,χN,β\chi_T, \chi_N, \beta satisfy IsSlopeWeight χT π (2π + δT), IsSlopeWeight χN π δ and IsLeftCutoff β. Then there are ε>0\varepsilon > 0 and a C∞C^\infty map F:W1,4×C×W1,4→L4×L4F : W^{1,4} \times \mathbb{C} \times W^{1,4} \to L^4 \times L^4 (QDom → LpCyl 1 4 × LpCyl 1 4) such that for every xx with ∥x∥<ε\|x\| < \varepsilon the two components of F(x)F(x) agree almost everywhere on the cylinder with the two components (read in R2\mathbb{R}^2 via cToVec) of the pointwise expression qPoint Jbar χT χN β x.

Role. qMap is defined as the L4L^4 class of qPoint (or 00 off L4L^4). This statement supplies a smooth map that represents it near 00; in particular qMap is C∞C^\infty on a ball around 00 (FiniteEnergyPlane_TubeFamily).

Preamble
import Definitions.Def_FiniteEnergyPlane_TubeFamily
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology CauchyRiemannIndex
open scoped ContDiff ENNReal Real

/-- For a standard tube structure and admissible weights, there is a `C^∞` map
`F : QDom → L⁴ × L⁴` whose two components, at every point `x` of some ball around `0`, are the
`L⁴` classes of the two components of the pointwise expression `qPoint Jbar χT χN β x`. -/
theorem exists_smooth_qPoint_rep (ρ b : ℝ) (hρ : 0 < ρ) (hb : 0 < b)
    (Jbar : ℂ × ℂ → ℂ × ℂ →L[ℝ] ℂ × ℂ) (Jinf : ℝ × ℂ → ℂ × ℂ →L[ℝ] ℂ × ℂ)
    (Sinf : ℝ → Mat 1) (hstd : IsStdTubeStructure ρ b Jbar Jinf Sinf)
    (δ δT : ℝ) (hδ : δ < 0) (hδT : δT ∈ Set.Ioo (max δ (-(2 * π))) 0)
    (χT χN β : ℝ → ℝ) (hχT : IsSlopeWeight χT π (2 * π + δT)) (hχN : IsSlopeWeight χN π δ)
    (hβ : IsLeftCutoff β) :
    ∃ ε > 0, ∃ F : QDom → LpCyl 1 4 × LpCyl 1 4, ContDiff ℝ ∞ F ∧ ∀ x ∈ ball (0 : QDom) ε,
      ((F x).1 : ℝ × ℝ → Vec 1) =ᵐ[cylMeasure] (fun q => cToVec (qPoint Jbar χT χN β x q).1) ∧
      ((F x).2 : ℝ × ℝ → Vec 1) =ᵐ[cylMeasure] (fun q => cToVec (qPoint Jbar χT χN β x q).2) := by
  sorry

end FiniteEnergyPlane
Source
Toward U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. AMS 364 (2012), arXiv:0812.4076, Lemmas 6.10 and 6.20 (families of fast planes); operators in the setting of C. Wendl, Lectures on Holomorphic Curves in Symplectic and Contact Geometry, arXiv:1011.1690, Ch. 4

View graph