Pointwise and integrated energy for curves into almost complex manifolds #
This file lifts the energy theory of $J$-holomorphic curves from normed vector spaces
(TauCeti.Geometry.Symplectic.JHolomorphic.Energy.Basic and Integral.lean) to smooth manifolds.
Given a manifold $M$ carrying a smooth two-form $\omega$ (TauCeti.SmoothTwoForm) and a smooth
almost complex structure $J$ (TauCeti.SmoothAlmostComplexStructure), we define:
Pointwise energy density. For a real-linear map $F : \mathbb{R}^2 \to T_x M$ from the standard complex line into a tangent space, its metric energy density is $$e(F) = \omega_x(F(\partial_s), J_x(F(\partial_s))) + \omega_x(F(\partial_t), J_x(F(\partial_t))).$$ When $\omega$ is fiberwise nondegenerate, this agrees with
TauCeti.SymplecticForm.stdComplexLineEnergyDensityon the tangent space $T_x M$.The energy--area identity. When $F$ is complex-linear (or when $u : \mathbb{R}^2 \to M$ is pseudoholomorphic at $z$), the energy density equals twice the symplectic area density: $$e(du_z) = 2 \omega_{u(z)}(du_z(\partial_s), du_z(\partial_t)).$$
The Wirtinger identity and inequality on manifolds. For an invariant pair, $$e(F) - 2 \omega_x(F(\partial_s), F(\partial_t)) = \omega_x(F(\partial_s) + J_x(F(\partial_t)), J_x(F(\partial_s) + J_x(F(\partial_t)))),$$ which under tameness/compatibility yields the pointwise bound $2 \omega_x(F(\partial_s), F(\partial_t)) \le e(F)$, with equality if and only if $F$ satisfies the Cauchy--Riemann equation $F(\partial_t) = J_x(F(\partial_s))$.
Integrated energy. For a curve $u : \mathbb{R}^2 \to M$, a field of candidate differentials $du_z$, and a measure $\mu$, its energy is the lower integral of the positive part $$E(u,du) = \int^\ast \operatorname{ofReal}\!\left(\frac{1}{2} e(du_z)\right) \, d\mu(z).$$ For an almost-everywhere complex-linear differential, this equals the lower integral of the positive part of the symplectic area density $\operatorname{ofReal}(\omega_{u(z)}(du_z(\partial_s),du_z(\partial_t)))$. Under tameness, nothing is truncated on the energy side, and zero energy detects an almost-everywhere vanishing differential, assuming the energy integrand is almost everywhere measurable. The area density of an arbitrary differential can still be negative even for a compatible pair. The differential is kept explicit because Mathlib defines
mfderivto be zero where differentiability fails; consumers usingmfderivmust assume differentiability separately when that convention matters.
These are the first manifold-level energy statements needed before the local theory of $J$-holomorphic curves.
Main declarations #
TauCeti.SmoothTwoForm.stdComplexLineEnergyDensity: the pointwise metric energy density of a real-linear map into a tangent fiber.TauCeti.SmoothTwoForm.IsNondegenerate.stdComplexLineEnergyDensity_eq: identification with the linear symplectic energy density when the two-form is fiberwise nondegenerate.TauCeti.SmoothTwoForm.Tames.stdComplexLineEnergyDensity_nonneg,TauCeti.SmoothTwoForm.Tames.stdComplexLineEnergyDensity_pos,TauCeti.SmoothTwoForm.Tames.stdComplexLineEnergyDensity_eq_zero_iff: nonnegativity, positivity, and exact nondegeneracy of the density under tameness.TauCeti.IsComplexLinearMap.stdComplexLineEnergyDensity_eq_two_mul_twoForm: for a complex-linear map into a tangent fiber, energy density is twice the symplectic area density.TauCeti.IsPseudoholomorphicAt.mfderiv_stdComplexLineEnergyDensity_eq_two_mul_twoForm: energy--area identity for the manifold derivative of a pseudoholomorphic curve.IsPseudoholomorphicWithinAt.mfderivWithin_stdComplexLineEnergyDensity_eq_two_mul_twoForm: energy--area identity for the within-set derivative of a pseudoholomorphic curve.TauCeti.SmoothTwoForm.Invariant.stdComplexLineEnergyDensity_sub_two_mul_twoForm: the Wirtinger identity on manifolds.TauCeti.SmoothTwoForm.Compatible.two_mul_twoForm_le_stdComplexLineEnergyDensity: the Wirtinger inequality on manifolds, andTauCeti.SmoothTwoForm.Compatible.stdComplexLineEnergyDensity_eq_two_mul_twoForm_iff: characterization of equality in the Wirtinger inequality.TauCeti.SmoothTwoForm.stdComplexLineEnergy: the integrated energy of a field of differentials along a curve $u : \mathbb{R}^2 \to M$.TauCeti.SmoothTwoForm.Compatible.lintegral_twoForm_le_stdComplexLineEnergy: the integrated Wirtinger inequality.TauCeti.SmoothTwoForm.stdComplexLineEnergy_eq_lintegral_twoForm: equality of integrated energy and symplectic area for an almost-everywhere complex-linear differential.TauCeti.SmoothTwoForm.mfderiv_stdComplexLineEnergy_eq_lintegral_twoForm: the specialization to an almost-everywhere pseudoholomorphic curve.TauCeti.SmoothTwoForm.stdComplexLineEnergy_eq_zero_of_ae_eq_zero: zero energy for an almost everywhere vanishing differential.TauCeti.SmoothTwoForm.Tames.stdComplexLineEnergy_eq_zero_iff: under tameness, zero energy characterizes an almost everywhere vanishing differential.
The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1.
The pointwise metric energy density of a real-linear map from the standard complex line into
the tangent space at x.
For a compatible pair (form, J), this is g(F ∂s, F ∂s) + g(F ∂t, F ∂t), where
g(v, w) = form x v (J x w).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Unfolding the definition of standard complex-line energy density on a manifold.
The zero real-linear map into a tangent fiber has zero standard complex-line energy density.
When a smooth two-form is fiberwise nondegenerate, the manifold energy density is the linear symplectic energy density on the tangent fiber.
The standard pointwise energy density of any real-linear map into a tangent fiber is nonnegative under tameness.
Under tameness, the standard pointwise energy density of a nonzero real-linear map into a tangent fiber is positive.
Under tameness, standard pointwise energy density vanishes exactly for the zero real-linear map into a tangent fiber.
Under tameness, standard pointwise energy density is positive exactly for nonzero real-linear maps into a tangent fiber.
Under tameness, standard pointwise energy density of a continuous linear map into a tangent fiber vanishes exactly when the continuous linear map is zero.
Under tameness, the standard pointwise energy density of a continuous linear map into a tangent fiber is positive exactly when the continuous linear map is nonzero.
For a complex-linear map out of the standard complex line into a tangent fiber, the pointwise energy density is twice the symplectic area density.
For a pseudoholomorphic curve from the standard complex line into an almost complex manifold, the manifold derivative's energy density is twice its symplectic area density.
For a within-set pseudoholomorphic curve from the standard complex line into an almost complex manifold, the within-set manifold derivative's energy density is twice its symplectic area density, provided derivatives within the set are unique.
Wirtinger identity on manifolds. For an invariant pair (form, J), the standard energy
density minus twice the symplectic area density is the Cauchy--Riemann defect square:
$$e(F) - 2 \omega_x(F \partial_s, F \partial_t) = \omega_x(F \partial_s + J_x F \partial_t, J_x(F \partial_s + J_x F \partial_t)).$$
Wirtinger inequality on manifolds. For a compatible pair (form, J), twice the symplectic
area density of any real-linear map into a tangent fiber is at most its standard energy density.
The Wirtinger inequality is an equality exactly when the linear map is complex-linear with
respect to AlmostComplexStructure.product ℝ and J.almostComplexStructureAt x.
Integrated energy on manifolds #
The integrated energy of a field of real-linear maps along a curve from the standard complex line into a manifold: the lower Lebesgue integral of the positive part of half the pointwise energy density.
Nothing here relates form and J. For a taming pair the density is nonnegative, so the positive
part loses nothing; for a general pair it can be negative, and ENNReal.ofReal truncates it. The
differential field is explicit rather than fixed to mfderiv, which Mathlib defines to be zero
where differentiability fails.
Equations
- form.stdComplexLineEnergy J u du μ = ∫⁻ (z : ℝ × ℝ), ENNReal.ofReal (form.stdComplexLineEnergyDensity J (u z) (du z) / 2) ∂μ
Instances For
Unfolding the definition of integrated energy.
Energy depends only on the differential field almost everywhere.
Enlarging the source measure cannot decrease the manifold energy.
Every differential field has zero energy with respect to the zero measure.
The zero differential field has zero energy.
The energy of a constant differential along a constant curve is its normalized pointwise density times the total mass of the source.
Integrated Wirtinger inequality on manifolds. For a compatible pair (form, J), the
integral of the positive part of the symplectic area density is bounded by the integrated energy.
Equality in the integrated Wirtinger inequality on manifolds. A differential field that is complex linear almost everywhere has energy equal to the lower integral of the positive part of its symplectic area density. For a taming pair the common density is nonnegative, so neither side is truncated.
The energy of an almost-everywhere pseudoholomorphic curve, computed using mfderiv, equals
the lower integral of the positive part of its symplectic area density.
If a differential field vanishes almost everywhere, its energy is zero.
A constant curve has zero energy when its differential field is mfderiv.
Under tameness, integrated energy vanishes exactly when the differential field vanishes almost everywhere, assuming the energy integrand is almost everywhere measurable.
For a field built from mfderiv, this detects mfderiv = 0 almost everywhere, not genuine local
constancy: Mathlib assigns mfderiv the value zero wherever differentiability fails.