Prove2Me

Local linear Cauchy–Riemann inequality for the ξ\xi-part of ∂s(pr∘u)\partial_s(\mathrm{pr}\circ u) on an open set

Proved
FiniteEnergyPlane.norm_dbar_xiPart_le_on

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

pseudoholomorphic-curvesreeb-dynamicssymplectization

Let S=H−1(1)⊂R2n+2S=H^{-1}(1)\subset\mathbb{R}^{2n+2} be a strictly star-shaped level, JJ a smooth dλ0d\lambda_0-compatible complex structure on ξ\xi, and J~\tilde J the induced almost complex structure on R2n+2∖{0}\mathbb{R}^{2n+2}\setminus\{0\}. Let U⊆CU\subseteq\mathbb{C} be open and u:U→R2n+2∖{0}u:U\to\mathbb{R}^{2n+2}\setminus\{0\} a smooth J~\tilde J-holomorphic map, w=pr∘uw=\mathrm{pr}\circ u, and

ζ(z)=πw(z) ∂sw(z),πwv=v−dH(w)vdH(w)w w−λ0(w)(v) R(w).\zeta(z)=\pi_{w(z)}\,\partial_s w(z),\qquad \pi_w v=v-\frac{dH(w)v}{dH(w)w}\,w-\lambda_0(w)(v)\,R(w).

Then every z0∈Uz_0\in U has a disc B(z0,ρ)⊆UB(z_0,\rho)\subseteq U and a constant MM with

∥∂sζ+J~(u) ∂tζ∥≤M ∥ζ∥on B(z0,ρ).\big\|\partial_s\zeta+\tilde J(u)\,\partial_t\zeta\big\|\le M\,\|\zeta\|\quad\text{on }B(z_0,\rho).

This is the version of norm_dbar_xiPart_le (89044077) for maps defined only on an open subset of C\mathbb{C}, as needed near the punctures of a finite-energy sphere.

Formalization Note The map is given by ContDiffOn ℝ ∞ u U, u z ≠ 0 on U and JHolomorphic.IsJHolomorphicOn (Jtilde H J) U u; ζ\zeta is written out with proj, liouville and reeb exactly as in norm_dbar_xiPart_le.

Preamble
import Definitions.Def_FiniteEnergyPlane_Setting
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- For a smooth `J̃`-holomorphic map `u ≠ 0` on an open set
`U ⊆ ℂ`, the `ξ`-part `ζ = π_w ∂ₛw` of `w = proj ∘ u` satisfies a linear Cauchy–Riemann inequality
with respect to `J̃(u)` on a disc around each point of `U`. -/
theorem norm_dbar_xiPart_le_on {n : ℕ} (H : V n → ℝ) (hH : IsStrictlyStarShapedLevel H)
    (J : V n → V n →L[ℝ] V n) (hJ : IsCompatibleXiStructure H J) (U : Set ℂ) (hU : IsOpen U)
    (u : ℂ → V n) (hu : ContDiffOn ℝ ∞ u U) (hu0 : ∀ z ∈ U, u z ≠ 0)
    (hhol : JHolomorphic.IsJHolomorphicOn (Jtilde H J) U u) (z₀ : ℂ) (hz₀ : z₀ ∈ U) :
    let ζ : ℂ → V n := fun z =>
      let w := proj H (u z)
      let v := fderiv ℝ (fun z => proj H (u z)) z 1
      v - (fderiv ℝ H w v / fderiv ℝ H w w) • w - liouville w v • reeb H w
    ∃ ρ > (0 : ℝ), ball z₀ ρ ⊆ U ∧ ∃ M : ℝ, ∀ z ∈ ball z₀ ρ,
      ‖fderiv ℝ ζ z 1 + Jtilde H J (u z) (fderiv ℝ ζ z Complex.I)‖ ≤ M * ‖ζ z‖ := by
  sorry

end FiniteEnergyPlane
Source
U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Section 2.2.4 (local version of the inequality behind formula (14))

View graph