Pointwise energy density for maps from the standard complex line

This file records pointwise energy-density bookkeeping. For a compatible pair (ω, J), the associated metric is g(v, w) = ω(v, J w). If a real-linear map F : ℝ × ℝ → V is complex-linear, then the standard energy density g(F ∂s, F ∂s) + g(F ∂t, F ∂t) is twice the symplectic area density ω(F ∂s, F ∂t).

Under a taming symplectic form the density is moreover nondegenerate: it is nonnegative for every real-linear map, vanishes exactly for the zero map, and is positive otherwise. The Frechet-derivative versions specialize this to pointwise and within-set constant-structure J-holomorphic maps.

For an arbitrary real-linear map the density obeys the Wirtinger inequality 2 ω(F ∂s, F ∂t) ≤ g(F ∂s, F ∂s) + g(F ∂t, F ∂t), the pointwise form of E(u) ≥ ∫ u^*ω: the difference is the Cauchy--Riemann defect square g(F ∂s + J (F ∂t), F ∂s + J (F ∂t)), which vanishes exactly when F is complex linear, so the inequality is an equality precisely for constant-structure J-holomorphic maps. This is the linear-algebra content behind "constant-structure J-holomorphic curves minimize energy in their homology class".

The statements here are pointwise linear algebra and Frechet-derivative calculus. They are integrated over a measure space in TauCeti.Geometry.Symplectic.JHolomorphic.Energy.Integral.

Main declarations

• TauCeti.SymplecticForm.stdComplexLineEnergyDensity: the metric energy density of a real-linear map from the standard complex line.
• TauCeti.IsComplexLinearMap.stdComplexLineEnergyDensity_eq_two_mul_symplecticForm: for a complex-linear map, energy density is twice symplectic area density.
• IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_eq_two_mul_symplecticForm: the corresponding Frechet-derivative statement for a pointwise constant-structure J-holomorphic map.
• TauCeti.SymplecticForm.stdComplexLineEnergyDensity_pos and TauCeti.SymplecticForm.stdComplexLineEnergyDensity_eq_zero_iff: nondegeneracy of the density under tameness, with TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_eq_zero_iff and IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineEnergyDensity_eq_zero_iff the Frechet-derivative versions.
• TauCeti.SymplecticForm.prod_stdComplexLineEnergyDensity: product-target energy density is the sum of the factor energy densities.
• TauCeti.SymplecticForm.stdComplexLineEnergyDensity_sub_two_mul_symplecticForm: the Wirtinger identity energyDensity F - 2 ω(F ∂s, F ∂t) = g(F ∂s + J (F ∂t), F ∂s + J (F ∂t)).
• TauCeti.SymplecticForm.two_mul_symplecticForm_le_stdComplexLineEnergyDensity: the Wirtinger inequality 2 ω(F ∂s, F ∂t) ≤ energyDensity F for a compatible pair, with the Frechet-derivative corollaries TauCeti.SymplecticForm.two_mul_symplecticForm_fderiv_le_stdComplexLineEnergyDensity and TauCeti.SymplecticForm.two_mul_symplecticForm_fderivWithin_le_stdComplexLineEnergyDensity.
• TauCeti.SymplecticForm.stdComplexLineEnergyDensity_eq_two_mul_symplecticForm_iff: equality holds exactly for complex-linear (constant-structure J-holomorphic) maps.

The convention follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1: for a compatible pair, g(·, ·) = ω(·, J ·) and du(∂t) = J du(∂s).

@[irreducible]

def TauCeti.SymplecticForm.stdComplexLineEnergyDensity {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (F : ℝ × ℝ →ₗ[ℝ] V) : ℝ

The pointwise metric energy density of a real-linear map from the standard complex line.

For a compatible pair (ω, J), this is g(F ∂s, F ∂s) + g(F ∂t, F ∂t), where g(v,w) = ω(v, J w).

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (F : ℝ × ℝ →ₗ[ℝ] V) : ω.stdComplexLineEnergyDensity J F = ((ω.associatedBilinForm J) (F stdComplexLineReal)) (F stdComplexLineReal) + ((ω.associatedBilinForm J) (F stdComplexLineImag)) (F stdComplexLineImag)

The standard complex-line energy density is the sum of the associated bilinear form evaluated on the images of the standard real and imaginary basis vectors.

@[simp]

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) : ω.stdComplexLineEnergyDensity J 0 = 0

The zero real-linear map has zero standard complex-line energy density. No hypothesis relating ω and J is needed, unlike in TauCeti.SymplecticForm.stdComplexLineEnergyDensity_eq_zero_iff.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_nonneg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hω : ω.Tames J) (F : ℝ × ℝ →ₗ[ℝ] V) : 0 ≤ ω.stdComplexLineEnergyDensity J F

The standard pointwise energy density of any real-linear map is nonnegative under tameness.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_pos {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hω : ω.Tames J) {F : ℝ × ℝ →ₗ[ℝ] V} (hFne : F ≠ 0) : 0 < ω.stdComplexLineEnergyDensity J F

Under tameness, the standard pointwise energy density of a nonzero real-linear map from the standard complex line is positive.

@[simp]

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hω : ω.Tames J) {F : ℝ × ℝ →ₗ[ℝ] V} : ω.stdComplexLineEnergyDensity J F = 0 ↔ F = 0

Under tameness, standard pointwise energy density vanishes exactly for the zero real-linear map from the standard complex line.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_pos_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hω : ω.Tames J) {F : ℝ × ℝ →ₗ[ℝ] V} : 0 < ω.stdComplexLineEnergyDensity J F ↔ F ≠ 0

Under tameness, the standard pointwise energy density is positive exactly for nonzero real-linear maps from the standard complex line.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_toLinearMap_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} [TopologicalSpace V] (hω : ω.Tames J) (F : ℝ × ℝ →L[ℝ] V) : ω.stdComplexLineEnergyDensity J ↑F = 0 ↔ F = 0

Under tameness, standard pointwise energy density of a continuous linear map vanishes exactly when the continuous linear map is zero.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_toLinearMap_pos_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} [TopologicalSpace V] (hω : ω.Tames J) (F : ℝ × ℝ →L[ℝ] V) : 0 < ω.stdComplexLineEnergyDensity J ↑F ↔ F ≠ 0

Under tameness, the standard pointwise energy density of a continuous linear map is positive exactly when the continuous linear map is nonzero.

@[simp]

theorem TauCeti.SymplecticForm.prod_stdComplexLineEnergyDensity {V : Type u_1} [AddCommGroup V] [Module ℝ V] {W : Type u_2} [AddCommGroup W] [Module ℝ W] {ω₁ : SymplecticForm V} {ω₂ : SymplecticForm W} {J₁ : AlmostComplexStructure V} {J₂ : AlmostComplexStructure W} (F : ℝ × ℝ →ₗ[ℝ] V × W) : (ω₁.prod ω₂).stdComplexLineEnergyDensity (J₁.prod J₂) F = ω₁.stdComplexLineEnergyDensity J₁ (LinearMap.fst ℝ V W ∘ₗ F) + ω₂.stdComplexLineEnergyDensity J₂ (LinearMap.snd ℝ V W ∘ₗ F)

The standard-line energy density of a real-linear map into a direct-sum target is the sum of the two factor energy densities of its coordinate projections.

theorem TauCeti.IsComplexLinearMap.associatedBilinForm_apply_stdComplexLineImag_self_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) : ((ω.associatedBilinForm J) (F stdComplexLineImag)) (F stdComplexLineImag) = ((ω.associatedBilinForm J) (F stdComplexLineReal)) (F stdComplexLineReal)

For a complex-linear map out of the standard complex line, the associated-bilinear-form diagonal of the imaginary-coordinate image equals that of the real-coordinate image.

theorem TauCeti.IsComplexLinearMap.associatedBilinForm_apply_stdComplexLineReal_self_eq_symplecticForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) : ((ω.associatedBilinForm J) (F stdComplexLineReal)) (F stdComplexLineReal) = (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag)

For a complex-linear map out of the standard complex line, the real-coordinate associated-bilinear-form diagonal is the symplectic area density of the ordered coordinate pair.

theorem TauCeti.IsComplexLinearMap.stdComplexLineEnergyDensity_eq_two_mul_symplecticForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {F : ℝ × ℝ →ₗ[ℝ] V} (hF : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F) : ω.stdComplexLineEnergyDensity J F = 2 * (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag)

For a complex-linear map out of the standard complex line, the standard pointwise energy density is twice the symplectic area density.

theorem TauCeti.IsConstStructureJHolomorphicAt.associatedBilinForm_fderiv_stdComplexLineImag_self_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicAt (AlmostComplexStructure.product ℝ) J f x) : ((ω.associatedBilinForm J) ((fderiv ℝ f x) stdComplexLineImag)) ((fderiv ℝ f x) stdComplexLineImag) = ((ω.associatedBilinForm J) ((fderiv ℝ f x) stdComplexLineReal)) ((fderiv ℝ f x) stdComplexLineReal)

For a pointwise constant-structure J-holomorphic map from the standard complex line, the associated-bilinear-form diagonal of the ∂t derivative equals that of the ∂s derivative.

theorem TauCeti.IsConstStructureJHolomorphicAt.associatedBilinForm_fderiv_stdComplexLineReal_self_eq_symplecticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicAt (AlmostComplexStructure.product ℝ) J f x) : ((ω.associatedBilinForm J) ((fderiv ℝ f x) stdComplexLineReal)) ((fderiv ℝ f x) stdComplexLineReal) = (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ f x) stdComplexLineReal) ((fderiv ℝ f x) stdComplexLineImag)

For a pointwise constant-structure J-holomorphic map from the standard complex line, the ∂s associated-bilinear-form diagonal is the symplectic area density ω(∂s u, ∂t u).

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_eq_two_mul_symplecticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicAt (AlmostComplexStructure.product ℝ) J f x) : ω.stdComplexLineEnergyDensity J ↑(fderiv ℝ f x) = 2 * (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ f x) stdComplexLineReal) ((fderiv ℝ f x) stdComplexLineImag)

For a pointwise constant-structure J-holomorphic map from the standard complex line, the derivative's standard energy density is twice its symplectic area density.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_nonneg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hω : ω.Tames J) : 0 ≤ ω.stdComplexLineEnergyDensity J ↑(fderiv ℝ f x)

The derivative's standard pointwise energy density is nonnegative under tameness.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_eq_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hω : ω.Tames J) : ω.stdComplexLineEnergyDensity J ↑(fderiv ℝ f x) = 0 ↔ fderiv ℝ f x = 0

Under tameness, the derivative standard energy density of a map from the standard complex line vanishes exactly when its Frechet derivative is zero.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_pos_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hω : ω.Tames J) : 0 < ω.stdComplexLineEnergyDensity J ↑(fderiv ℝ f x) ↔ fderiv ℝ f x ≠ 0

Under tameness, the derivative standard energy density of a map from the standard complex line is positive exactly when its Frechet derivative is nonzero.

theorem TauCeti.IsConstStructureJHolomorphicAt.fderiv_stdComplexLineEnergyDensity_pos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {x : ℝ × ℝ} (hω : ω.Tames J) (hfderiv : fderiv ℝ f x ≠ 0) : 0 < ω.stdComplexLineEnergyDensity J ↑(fderiv ℝ f x)

Under tameness, a map with nonzero Frechet derivative has positive standard derivative energy density.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.associatedBilinForm_fderivWithin_stdComplexLineImag_self_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicWithinAt (AlmostComplexStructure.product ℝ) J f s x) (hs : UniqueDiffWithinAt ℝ s x) : ((ω.associatedBilinForm J) ((fderivWithin ℝ f s x) stdComplexLineImag)) ((fderivWithin ℝ f s x) stdComplexLineImag) = ((ω.associatedBilinForm J) ((fderivWithin ℝ f s x) stdComplexLineReal)) ((fderivWithin ℝ f s x) stdComplexLineReal)

For a within-set constant-structure J-holomorphic map from the standard complex line, the associated-bilinear-form diagonal of the ∂t derivative equals that of the ∂s derivative, provided derivatives within the set are unique.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.associatedBilinForm_fderivWithin_stdComplexLineReal_self_eq_symplecticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicWithinAt (AlmostComplexStructure.product ℝ) J f s x) (hs : UniqueDiffWithinAt ℝ s x) : ((ω.associatedBilinForm J) ((fderivWithin ℝ f s x) stdComplexLineReal)) ((fderivWithin ℝ f s x) stdComplexLineReal) = (fun (v w : V) => (ω.toBilinForm v) w) ((fderivWithin ℝ f s x) stdComplexLineReal) ((fderivWithin ℝ f s x) stdComplexLineImag)

For a within-set constant-structure J-holomorphic map from the standard complex line, the ∂s associated-bilinear-form diagonal is the symplectic area density ω(∂s u, ∂t u), provided derivatives within the set are unique.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineEnergyDensity_eq_two_mul_symplecticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hf : IsConstStructureJHolomorphicWithinAt (AlmostComplexStructure.product ℝ) J f s x) (hs : UniqueDiffWithinAt ℝ s x) : ω.stdComplexLineEnergyDensity J ↑(fderivWithin ℝ f s x) = 2 * (fun (v w : V) => (ω.toBilinForm v) w) ((fderivWithin ℝ f s x) stdComplexLineReal) ((fderivWithin ℝ f s x) stdComplexLineImag)

For a within-set constant-structure J-holomorphic map from the standard complex line, the derivative's standard energy density is twice its symplectic area density, provided derivatives within the set are unique.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineEnergyDensity_nonneg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hω : ω.Tames J) : 0 ≤ ω.stdComplexLineEnergyDensity J ↑(fderivWithin ℝ f s x)

The within-set derivative's standard pointwise energy density is nonnegative under tameness.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineEnergyDensity_eq_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hω : ω.Tames J) : ω.stdComplexLineEnergyDensity J ↑(fderivWithin ℝ f s x) = 0 ↔ fderivWithin ℝ f s x = 0

Under tameness, the within-set derivative standard energy density of a map from the standard complex line vanishes exactly when its Frechet derivative within the set is zero.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineEnergyDensity_pos_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hω : ω.Tames J) : 0 < ω.stdComplexLineEnergyDensity J ↑(fderivWithin ℝ f s x) ↔ fderivWithin ℝ f s x ≠ 0

Under tameness, the within-set derivative standard energy density is positive exactly when the Frechet derivative within the set is nonzero.

theorem TauCeti.IsConstStructureJHolomorphicWithinAt.fderivWithin_stdComplexLineEnergyDensity_pos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} {f : ℝ × ℝ → V} {s : Set (ℝ × ℝ)} {x : ℝ × ℝ} (hω : ω.Tames J) (hfderiv : fderivWithin ℝ f s x ≠ 0) : 0 < ω.stdComplexLineEnergyDensity J ↑(fderivWithin ℝ f s x)

Under tameness, a map with nonzero Frechet derivative within a set has positive standard derivative energy density.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_sub_two_mul_symplecticForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hinv : ω.Invariant J) (F : ℝ × ℝ →ₗ[ℝ] V) : ω.stdComplexLineEnergyDensity J F - 2 * (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag) = ((ω.associatedBilinForm J) (F stdComplexLineReal + J.toLinearMap (F stdComplexLineImag))) (F stdComplexLineReal + J.toLinearMap (F stdComplexLineImag))

The Wirtinger identity out of the standard complex line: the standard energy density minus twice the symplectic area density is the Cauchy--Riemann defect square g(F ∂s + J (F ∂t), F ∂s + J (F ∂t)). Needs only J-invariance of ω.

theorem TauCeti.SymplecticForm.two_mul_symplecticForm_le_stdComplexLineEnergyDensity {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hcompat : ω.Compatible J) (F : ℝ × ℝ →ₗ[ℝ] V) : 2 * (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag) ≤ ω.stdComplexLineEnergyDensity J F

Wirtinger inequality. For a compatible pair (ω, J) and any real-linear map out of the standard complex line, twice the symplectic area density of the ordered coordinate pair is at most the standard energy density: the local form of E(u) ≥ ∫ u^*ω.

theorem TauCeti.SymplecticForm.stdComplexLineEnergyDensity_eq_two_mul_symplecticForm_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {J : AlmostComplexStructure V} {ω : SymplecticForm V} (hcompat : ω.Compatible J) (F : ℝ × ℝ →ₗ[ℝ] V) : ω.stdComplexLineEnergyDensity J F = 2 * (fun (v w : V) => (ω.toBilinForm v) w) (F stdComplexLineReal) (F stdComplexLineImag) ↔ IsComplexLinearMap (AlmostComplexStructure.product ℝ) J F

The Wirtinger inequality is an equality exactly when the map is complex linear, that is, constant-structure J-holomorphic out of the standard complex line: the energy density then equals twice the symplectic area density.

theorem TauCeti.SymplecticForm.two_mul_symplecticForm_fderiv_le_stdComplexLineEnergyDensity {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure W} {ω : SymplecticForm W} {f : ℝ × ℝ → W} (hcompat : ω.Compatible J) (x : ℝ × ℝ) : 2 * (fun (v w : W) => (ω.toBilinForm v) w) ((fderiv ℝ f x) stdComplexLineReal) ((fderiv ℝ f x) stdComplexLineImag) ≤ ω.stdComplexLineEnergyDensity J ↑(fderiv ℝ f x)

The Wirtinger inequality for the Frechet derivative of any map from the standard complex line: twice the symplectic area density of the derivative's coordinate pair is at most its standard energy density.

theorem TauCeti.SymplecticForm.two_mul_symplecticForm_fderivWithin_le_stdComplexLineEnergyDensity {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] {J : AlmostComplexStructure W} {ω : SymplecticForm W} {f : ℝ × ℝ → W} (hcompat : ω.Compatible J) (s : Set (ℝ × ℝ)) (x : ℝ × ℝ) : 2 * (fun (v w : W) => (ω.toBilinForm v) w) ((fderivWithin ℝ f s x) stdComplexLineReal) ((fderivWithin ℝ f s x) stdComplexLineImag) ≤ ω.stdComplexLineEnergyDensity J ↑(fderivWithin ℝ f s x)

The Wirtinger inequality for the within-set Frechet derivative of any map from the standard complex line.