Metric area between energy and symplectic area

For a compatible pair (ω, J) with associated metric g = ω(·, J ·), the metric area density of a real-linear map F out of the standard complex line is the wedge norm |F ∂s ∧ F ∂t|_g (TauCeti.SymplecticForm.wedgeNorm). It sits between the two densities of TauCeti.Geometry.Symplectic.JHolomorphic.Energy.Basic:

ω(F ∂s, F ∂t) ≤ |F ∂s ∧ F ∂t|_g ≤ (g(F ∂s, F ∂s) + g(F ∂t, F ∂t)) / 2.

The first inequality is the Wirtinger inequality. It is an equality 0 = 0 when F ∂s and F ∂t are linearly dependent (F has rank at most one); when F has rank two it is an equality exactly when the image plane is a J-complex line with its complex orientation. The second is an equality exactly when F is conformal for g. Both are equalities exactly when F is complex linear.

Integrating over a measure on the source gives the chain E(u) ≥ Area_g(u) ≥ ∫ u^*ω for the energy TauCeti.SymplecticForm.stdComplexLineEnergy and the metric area TauCeti.SymplecticForm.stdComplexLineArea of a field of differentials, with equality throughout for an almost everywhere complex-linear differential, in particular for a constant-structure J-holomorphic map. As there, the differential is kept explicit and all integrals are lower Lebesgue integrals of positive parts.

Main declarations

• TauCeti.SymplecticForm.two_mul_wedgeNorm_le_stdComplexLineEnergyDensity: the pointwise inequality 2 |F ∂s ∧ F ∂t|_g ≤ energyDensity F, with equality case TauCeti.SymplecticForm.two_mul_wedgeNorm_eq_stdComplexLineEnergyDensity_iff for conformal F.
• TauCeti.SymplecticForm.stdComplexLineArea: the metric area of a field of differentials.
• TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineArea: ∫ u^*ω ≤ Area_g(u).
• TauCeti.SymplecticForm.stdComplexLineArea_le_stdComplexLineEnergy: Area_g(u) ≤ E(u).
• TauCeti.SymplecticForm.stdComplexLineArea_eq_stdComplexLineEnergy and TauCeti.SymplecticForm.fderiv_stdComplexLineArea_eq_stdComplexLineEnergy: equality for complex-linear differentials and for constant-structure J-holomorphic maps.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Lemma 2.2.1.

theorem TauCeti.SymplecticForm.two_mul_wedgeNorm_le_stdComplexLineEnergyDensity {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hcompat : ω.Compatible J) (F : ℝ × ℝ →ₗ[ℝ] V) : 2 * ω.wedgeNorm J (F stdComplexLineReal) (F stdComplexLineImag) ≤ ω.stdComplexLineEnergyDensity J F

Area is at most energy, pointwise. For a compatible pair, twice the metric area density |F ∂s ∧ F ∂t|_g of a real-linear map out of the standard complex line is at most its energy density.

theorem TauCeti.SymplecticForm.two_mul_wedgeNorm_eq_stdComplexLineEnergyDensity_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hcompat : ω.Compatible J) (F : ℝ × ℝ →ₗ[ℝ] V) : 2 * ω.wedgeNorm J (F stdComplexLineReal) (F stdComplexLineImag) = ω.stdComplexLineEnergyDensity J F ↔ ((ω.associatedBilinForm J) (F stdComplexLineReal)) (F stdComplexLineReal) = ((ω.associatedBilinForm J) (F stdComplexLineImag)) (F stdComplexLineImag) ∧ ((ω.associatedBilinForm J) (F stdComplexLineReal)) (F stdComplexLineImag) = 0

Twice the metric area density equals the energy density exactly when the map is conformal for the associated metric: F ∂s and F ∂t have the same length and are orthogonal.

noncomputable def TauCeti.SymplecticForm.stdComplexLineArea {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (du : X → ℝ × ℝ →ₗ[ℝ] V) (μ : MeasureTheory.Measure X) : ENNReal

The metric area of a field of real-linear maps out of the standard complex line: the lower Lebesgue integral of the wedge norm |du ∂s ∧ du ∂t|_g for the associated form g = ω(·, J ·). The source measure μ is arbitrary. For a compatible pair, Lebesgue measure on a planar domain X, and the differential du of a C¹ immersion u, the area formula identifies this with the area of the image surface counted with multiplicity, measured in g.

theorem TauCeti.SymplecticForm.stdComplexLineArea_def {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (du : X → ℝ × ℝ →ₗ[ℝ] V) (μ : MeasureTheory.Measure X) : ω.stdComplexLineArea J du μ = ∫⁻ (x : X), ENNReal.ofReal (ω.wedgeNorm J ((du x) stdComplexLineReal) ((du x) stdComplexLineImag)) ∂μ

The metric area of a differential field is the lower integral of its wedge norm.

@[simp]

theorem TauCeti.SymplecticForm.stdComplexLineArea_zero {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (μ : MeasureTheory.Measure X) : ω.stdComplexLineArea J 0 μ = 0

The zero differential field has zero metric area.

@[simp]

theorem TauCeti.SymplecticForm.stdComplexLineArea_zero_measure {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (du : X → ℝ × ℝ →ₗ[ℝ] V) : ω.stdComplexLineArea J du 0 = 0

Metric area for the zero source measure is zero.

theorem TauCeti.SymplecticForm.stdComplexLineArea_congr_ae {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {μ : MeasureTheory.Measure X} {du dv : X → ℝ × ℝ →ₗ[ℝ] V} (h : du =ᵐ[μ] dv) : ω.stdComplexLineArea J du μ = ω.stdComplexLineArea J dv μ

Metric area depends only on the differential field almost everywhere.

theorem TauCeti.SymplecticForm.stdComplexLineArea_mono_measure {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {μ ν : MeasureTheory.Measure X} {du : X → ℝ × ℝ →ₗ[ℝ] V} (hμν : μ ≤ ν) : ω.stdComplexLineArea J du μ ≤ ω.stdComplexLineArea J du ν

Enlarging the source measure cannot decrease metric area.

theorem TauCeti.SymplecticForm.lintegral_symplecticForm_le_stdComplexLineArea {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {μ : MeasureTheory.Measure X} {du : X → ℝ × ℝ →ₗ[ℝ] V} (hcompat : ω.Compatible J) : ∫⁻ (x : X), ENNReal.ofReal ((fun (v w : V) => (ω.toBilinForm v) w) ((du x) stdComplexLineReal) ((du x) stdComplexLineImag)) ∂μ ≤ ω.stdComplexLineArea J du μ

Integrated Wirtinger inequality, area form. For a compatible pair, the integral of the positive symplectic area density is at most the metric area.

theorem TauCeti.SymplecticForm.stdComplexLineArea_le_stdComplexLineEnergy {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {μ : MeasureTheory.Measure X} {du : X → ℝ × ℝ →ₗ[ℝ] V} (hcompat : ω.Compatible J) : ω.stdComplexLineArea J du μ ≤ ω.stdComplexLineEnergy J du μ

Area is at most energy. For a compatible pair, the metric area of a differential field is at most its energy.

theorem TauCeti.SymplecticForm.stdComplexLineArea_eq_stdComplexLineEnergy {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {μ : MeasureTheory.Measure X} {du : X → ℝ × ℝ →ₗ[ℝ] V} (hcompat : ω.Compatible J) (hdu : ∀ᵐ (x : X) ∂μ, IsComplexLinearMap (AlmostComplexStructure.product ℝ) J (du x)) : ω.stdComplexLineArea J du μ = ω.stdComplexLineEnergy J du μ

For a compatible pair, a differential field that is complex linear almost everywhere has metric area equal to its energy, and hence, by TauCeti.SymplecticForm.stdComplexLineEnergy_eq_lintegral_symplecticForm, to the integral of its symplectic area density.

theorem TauCeti.SymplecticForm.fderiv_stdComplexLineArea_eq_stdComplexLineEnergy {W : Type u_3} [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure W} {ω : SymplecticForm W} {f : ℝ × ℝ → W} {μ : MeasureTheory.Measure (ℝ × ℝ)} (hcompat : ω.Compatible J) (hf : ∀ᵐ (x : ℝ × ℝ) ∂μ, IsConstStructureJHolomorphicAt (AlmostComplexStructure.product ℝ) J f x) : ω.stdComplexLineArea J (fun (x : ℝ × ℝ) => ↑(fderiv ℝ f x)) μ = ω.stdComplexLineEnergy J (fun (x : ℝ × ℝ) => ↑(fderiv ℝ f x)) μ

For a compatible pair, a map that is constant-structure J-holomorphic almost everywhere has metric area equal to its energy.