Prove2Me

Integral of ψ σ(∂su,∂tu)\psi\,\sigma(\partial_s u,\partial_t u) for an antisymmetric bilinear form σ\sigma and a compactly supported weight ψ\psi

Proved
FiniteEnergyPlane.integral_mul_bilin_fderiv_eq

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

calculusintegrationpseudoholomorphic-curvesstokes-theorem

Let FF be a real normed space and σ:F×F→R\sigma:F\times F\to\mathbb{R} a continuous bilinear form with σ(v,w)=−σ(w,v)\sigma(v,w)=-\sigma(w,v). Let U⊆CU\subseteq\mathbb{C} be open, let u:C→Fu:\mathbb{C}\to F be C2C^2 on UU, let q∈Fq\in F, and let ψ:C→R\psi:\mathbb{C}\to\mathbb{R} be C1C^1 with compact support contained in UU. Writing ∂sf=Df⋅1\partial_s f=Df\cdot1 and ∂tf=Df⋅i\partial_t f=Df\cdot i,

∫Cψ σ(∂su,∂tu)  =  −12∫C(∂sψ  σ(u−q,∂tu)−∂tψ  σ(u−q,∂su)).\int_{\mathbb{C}}\psi\,\sigma(\partial_su,\partial_tu)\;=\;-\frac12\int_{\mathbb{C}}\Bigl(\partial_s\psi\;\sigma(u-q,\partial_tu)-\partial_t\psi\;\sigma(u-q,\partial_su)\Bigr).

For F=R2nF=\mathbb{R}^{2n} and σ\sigma a symplectic form, the left side is ∫ψ u∗σ\int\psi\,u^*\sigma, and the identity expresses it through first derivatives of uu and of the weight only.

Formalization Note σ\sigma is F →L[ℝ] F →L[ℝ] ℝ; uu is ContDiffOn ℝ 2 u U, ψ\psi is ContDiff ℝ 1 ψ with HasCompactSupport ψ and tsupport ψ ⊆ U. Both integrals are Bochner integrals over C\mathbb{C} with Lebesgue measure; the integrands vanish outside tsupport⁡ψ\operatorname{tsupport}\psi.

Preamble
import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.FDeriv.CompCLM
import Mathlib.Analysis.Complex.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Formal statement
namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff

/-- Let `σ` be an antisymmetric continuous bilinear form on `F`, `u` a `C²` map on an open set
`U ⊆ ℂ`, `q ∈ F`, and `ψ` a real `C¹` function with compact support in `U`. Writing
`∂ₛ = D(·) 1`, `∂ₜ = D(·) i`,
`∫ ψ σ(∂ₛu, ∂ₜu) = -½ ∫ (∂ₛψ σ(u - q, ∂ₜu) - ∂ₜψ σ(u - q, ∂ₛu))`. -/
theorem integral_mul_bilin_fderiv_eq {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (σ : F →L[ℝ] F →L[ℝ] ℝ) (hσ : ∀ v w, σ v w = -σ w v) {U : Set ℂ} (hU : IsOpen U)
    {u : ℂ → F} (hu : ContDiffOn ℝ 2 u U) {ψ : ℂ → ℝ} (hψ : ContDiff ℝ 1 ψ)
    (hψc : HasCompactSupport ψ) (hψU : tsupport ψ ⊆ U) (q : F) :
    ∫ z, ψ z * σ (fderiv ℝ u z 1) (fderiv ℝ u z Complex.I) =
      -(1 / 2) * ∫ z, (fderiv ℝ ψ z 1 * σ (u z - q) (fderiv ℝ u z Complex.I) -
        fderiv ℝ ψ z Complex.I * σ (u z - q) (fderiv ℝ u z 1)) := by
  sorry

end FiniteEnergyPlane
Source
Standard (Stokes' theorem for an exact 2-form); used for the monotonicity lemma, A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331, Proposition 3.12; C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, p. 152

View graph