Documentation

TauCeti.Geometry.Symplectic.Wirtinger

The Wirtinger inequality for a compatible triple #

Let ω be a symplectic form compatible with an almost complex structure J, and let g(v, w) = ω(v, J w) be the associated metric. The g-area of the parallelogram spanned by two vectors is the norm of their wedge product, |v ∧ w|_g = √(g(v, v) g(w, w) - g(v, w)²).

The degree-two Wirtinger inequality says that ω calibrates g: ω(v, w) ≤ |v ∧ w|_g, with equality for linearly independent v and w exactly when w = a v + b J v with b > 0, that is, when the oriented plane (v, w) is a J-complex line carrying its complex orientation. The proof is a Cauchy--Schwarz argument: ω(v, w) = g(J v, w), the vector J v is g-orthogonal to v and has the same length, and the component w⊥ of w orthogonal to the plane spanned by v and J v contributes nothing to ω(v, w) but increases |v ∧ w|_g² by g(v, v) g(w⊥, w⊥). In fact g(v, w)² + ω(v, w)² ≤ g(v, v) g(w, w).

The arithmetic-geometric mean inequality gives the second link of the chain ω(v, w) ≤ |v ∧ w|_g ≤ (g(v, v) + g(w, w)) / 2; the second inequality is an equality exactly when the pair (v, w) is conformal (g(v, v) = g(w, w) and g(v, w) = 0), and the two together are equalities exactly when w = J v. Applied to the partial derivatives of a map from a surface, this is the pointwise chain energy density ≥ area density ≥ symplectic area density of TauCeti.Geometry.Symplectic.JHolomorphic.Energy.Area, where the equality case of the whole chain is TauCeti.SymplecticForm.stdComplexLineEnergyDensity_eq_two_mul_symplecticForm_iff.

Everything is pointwise linear algebra: no integrability of J or closedness of ω is involved.

Main declarations #

References #

source
noncomputable def TauCeti.SymplecticForm.wedgeNorm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v w : V) :
ℝ

The norm |v ∧ w|_g of the wedge of two vectors for the associated metric g = ω(·, J ·): the square root of the Gram determinant g(v, v) g(w, w) - g(v, w)². For a compatible pair this is the g-area of the parallelogram spanned by v and w.

Instances For
    source
    theorem TauCeti.SymplecticForm.wedgeNorm_def {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v w : V) :
    ω.wedgeNorm J v w = √(((ω.associatedBilinForm J) v) v * ((ω.associatedBilinForm J) w) w - ((ω.associatedBilinForm J) v) w ^ 2)

    The wedge norm is the square root of the Gram determinant of the associated metric.

    source
    theorem TauCeti.SymplecticForm.wedgeNorm_nonneg {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v w : V) :
    0 ≤ ω.wedgeNorm J v w

    The wedge norm is nonnegative.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.wedgeNorm_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v : V) :
    ω.wedgeNorm J v v = 0

    The wedge of a vector with itself has norm zero.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.wedgeNorm_zero_left {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (w : V) :
    ω.wedgeNorm J 0 w = 0

    The wedge of the zero vector with any vector has norm zero.

    source
    @[simp]
    theorem TauCeti.SymplecticForm.wedgeNorm_zero_right {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (v : V) :
    ω.wedgeNorm J v 0 = 0

    The wedge of any vector with the zero vector has norm zero.

    source
    theorem TauCeti.SymplecticForm.Invariant.wedgeNorm_comm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) :
    ω.wedgeNorm J v w = ω.wedgeNorm J w v

    The wedge norm is symmetric for a J-invariant form, whose associated metric is symmetric.

    source
    theorem TauCeti.SymplecticForm.Compatible.sq_associatedBilinForm_add_sq_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    ((ω.associatedBilinForm J) v) w ^ 2 + (fun (v w : V) => (ω.toBilinForm v) w) v w ^ 2 ≤ ((ω.associatedBilinForm J) v) v * ((ω.associatedBilinForm J) w) w

    Cauchy--Schwarz along a complex line. For a compatible pair, the squares of the components g(v, w) and ω(v, w) = g(J v, w) of w along the orthogonal pair v, J v add up to at most g(v, v) g(w, w).

    source
    theorem TauCeti.SymplecticForm.Compatible.sq_wedgeNorm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    ω.wedgeNorm J v w ^ 2 = ((ω.associatedBilinForm J) v) v * ((ω.associatedBilinForm J) w) w - ((ω.associatedBilinForm J) v) w ^ 2

    For a compatible pair, the square of the wedge norm is the Gram determinant g(v, v) g(w, w) - g(v, w)².

    source
    theorem TauCeti.SymplecticForm.Compatible.wedgeNorm_pos_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    0 < ω.wedgeNorm J v w ↔ LinearIndependent ℝ ![v, w]

    For a compatible pair, the wedge norm is positive exactly for linearly independent pairs.

    source
    theorem TauCeti.SymplecticForm.Tames.wedgeNorm_apply_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Tames J) (v : V) :
    ω.wedgeNorm J v (J.toLinearMap v) = ((ω.associatedBilinForm J) v) v

    The wedge of v with J v has norm g(v, v): the pair (v, J v) is g-orthogonal and its two vectors have the same length.

    source
    theorem TauCeti.SymplecticForm.Compatible.abs_apply_le_wedgeNorm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    |(fun (v w : V) => (ω.toBilinForm v) w) v w| ≤ ω.wedgeNorm J v w

    For a compatible pair, |ω(v, w)| is at most the wedge norm |v ∧ w|_g.

    source
    theorem TauCeti.SymplecticForm.Compatible.apply_le_wedgeNorm {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    (fun (v w : V) => (ω.toBilinForm v) w) v w ≤ ω.wedgeNorm J v w

    The Wirtinger inequality. A symplectic form compatible with J calibrates the associated metric: ω(v, w) ≤ |v ∧ w|_g.

    source
    theorem TauCeti.SymplecticForm.Compatible.apply_eq_wedgeNorm_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) {v : V} (hv : v ≠ 0) (w : V) :
    (fun (v w : V) => (ω.toBilinForm v) w) v w = ω.wedgeNorm J v w ↔ ∃ (a : ℝ) (b : ℝ), 0 ≤ b ∧ w = a • v + b • J.toLinearMap v

    The equality case of the Wirtinger inequality for a nonzero first vector: ω(v, w) equals |v ∧ w|_g exactly when w lies in the closed half of the complex line through v on the side of J v, that is, w = a v + b J v with b ≥ 0.

    source
    theorem TauCeti.SymplecticForm.Compatible.apply_eq_wedgeNorm_iff_of_linearIndependent {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) {v w : V} (hvw : LinearIndependent ℝ ![v, w]) :
    (fun (v w : V) => (ω.toBilinForm v) w) v w = ω.wedgeNorm J v w ↔ ∃ (a : ℝ) (b : ℝ), 0 < b ∧ w = a • v + b • J.toLinearMap v

    The equality case of the Wirtinger inequality. For linearly independent v and w, ω(v, w) = |v ∧ w|_g exactly when w = a v + b J v with b > 0: the oriented plane (v, w) is a J-complex line with its complex orientation.

    source
    theorem TauCeti.SymplecticForm.Compatible.two_mul_wedgeNorm_le {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    2 * ω.wedgeNorm J v w ≤ ((ω.associatedBilinForm J) v) v + ((ω.associatedBilinForm J) w) w

    Area is at most energy. For a compatible pair, 2 |v ∧ w|_g ≤ g(v, v) + g(w, w).

    source
    theorem TauCeti.SymplecticForm.Compatible.two_mul_wedgeNorm_eq_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) :
    2 * ω.wedgeNorm J v w = ((ω.associatedBilinForm J) v) v + ((ω.associatedBilinForm J) w) w ↔ ((ω.associatedBilinForm J) v) v = ((ω.associatedBilinForm J) w) w ∧ ((ω.associatedBilinForm J) v) w = 0

    The equality case of 2 |v ∧ w|_g ≤ g(v, v) + g(w, w): it holds exactly for conformal pairs, those with g(v, v) = g(w, w) and g(v, w) = 0.