Integrated energy for maps from the standard complex line #
This file integrates the pointwise energy density from
TauCeti.Geometry.Symplectic.JHolomorphic.Energy.Basic. Given a measurable source X, a
measure μ, and a field
du : X → (ℝ × ℝ) →ₗ[ℝ] V,
its energy is
∫⁻ x, ENNReal.ofReal (energyDensity (du x) / 2) ∂μ.
The factor 1 / 2 is the standard convention for the energy of a map. The named pointwise
density stdComplexLineEnergyDensity is twice the symplectic area density on a complex-linear
differential, so it is the normalized half-density integrated here that equals the area density
ω (du ∂s) (du ∂t) exactly. The differential is kept explicit: for a differentiable map u,
consumers use
fun x ↦ (fderiv ℝ u x).toLinearMap. This avoids assigning a misleading energy to a
nondifferentiable map, since Mathlib defines fderiv to be zero where differentiability fails.
Under a taming hypothesis, zero energy is equivalent to the differential vanishing almost
everywhere (assuming the energy integrand is a.e. measurable). Under compatibility, the
integrated Wirtinger inequality bounds the integral of the symplectic area density by energy;
equality needs only that the differential is complex linear almost everywhere. These are the
first total-energy statements needed before the compactness theory for J-holomorphic curves.
Everything is stated for an abstract field of differentials over an abstract measure, so a domain
such as a strip or a disk is handled by restricting the measure to it.
Both integrands are wrapped in ENNReal.ofReal, so what is integrated is in each case a positive
part. A taming pair makes the energy density nonnegative, so nothing is truncated on the energy
side; the symplectic area density ω (du ∂s) (du ∂t) of an arbitrary differential can be
negative even for a compatible pair, and is truncated when it is. It is nonnegative once the
differential is complex linear and the pair tames, since then it is half the energy density.
Main declarations #
TauCeti.SymplecticForm.stdComplexLineEnergy: the integrated energy of a field of differentials.TauCeti.SymplecticForm.stdComplexLineEnergy_eq_zero_iff: zero energy detects a differential that vanishes almost everywhere.TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineEnergy: the integrated Wirtinger inequality.TauCeti.SymplecticForm.stdComplexLineEnergy_eq_lintegral_symplecticForm: equality of energy and symplectic area for an almost everywhere complex-linear differential.TauCeti.SymplecticForm.fderiv_stdComplexLineEnergy_eq_lintegral_symplecticForm: the energy--area identity for an almost everywhere constant-structureJ-holomorphic map.
The convention and the energy--area identity follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1.
The normalized energy of a field of real-linear maps out of the standard complex line: the
lower Lebesgue integral of the positive part of half the pointwise associated-form density
TauCeti.SymplecticForm.stdComplexLineEnergyDensity.
Nothing here relates ω and J. For a compatible pair the density is the energy density of the
associated metric g = ω(·, J ·), so this is the usual (1 / 2) ∫ |du|² measured in g and the
positive part loses nothing; for a general pair the density can be negative, and ENNReal.ofReal
truncates it. Values lie in ℝ≥0∞, so infinite energy is represented honestly rather than being
collapsed to zero by a nonintegrable Bochner integral.
Instances For
The energy of a differential field is the lower integral of its normalized pointwise energy density.
Energy depends only on the differential field almost everywhere.
Enlarging the source measure cannot decrease energy.
The zero differential has zero energy.
Every differential has zero energy with respect to the zero measure.
The energy of a constant differential is its normalized pointwise density times the total mass of the source.
Under tameness, energy vanishes exactly when the differential vanishes almost everywhere.
The a.e.-measurability assumption is necessary for the implication from zero energy to a.e.
vanishing: the lower Lebesgue integral of a nonmeasurable function can be zero without that
function vanishing almost everywhere. It is stated for the real-valued pointwise density, so no
consumer has to reassemble the normalization that TauCeti.SymplecticForm.stdComplexLineEnergy
applies to it.
If the differential vanishes almost everywhere, then its energy is zero. This direction does not require measurability.
Integrated Wirtinger inequality. For a compatible pair, the integral of the positive symplectic area density is at most the energy.
Equality in the integrated Wirtinger inequality. A differential that is complex linear
almost everywhere has energy equal to the integral of its symplectic area density. In particular,
this applies to the differential of a constant-structure J-holomorphic map.
No hypothesis on the pair (ω, J) is needed: complex linearity alone makes the pointwise energy
density twice the symplectic area density, so the two ENNReal.ofReal integrands agree pointwise.
Under a taming pair the common value is moreover nonnegative, and the identity is the
energy--area identity rather than one between positive parts.
The energy of a map that is constant-structure J-holomorphic almost everywhere is the lower
Lebesgue integral of its symplectic area density. Holomorphy is needed only almost everywhere, so
a map holomorphic on a strip or a disk is covered by restricting μ to that domain.
As in TauCeti.SymplecticForm.stdComplexLineEnergy_eq_lintegral_symplecticForm, no hypothesis
relating ω and J is needed for the identity; a taming pair is what additionally makes the
common integrand nonnegative, so that neither side is truncated by ENNReal.ofReal.