The metric of a compatible pair

A symplectic form ω compatible with an almost complex structure J determines a Riemannian metric g(v, w) = ω(v, J w). This file records the standard compatible-triple identities tying ω, J, and g together, and packages the metric of a compatible pair as a genuine inner product through Mathlib's InnerProductSpace.Core.

The metric is TauCeti.SymplecticForm.associatedBilinForm, already defined in AlmostComplex.lean. Compatibility makes it symmetric and positive definite (recorded there); here we add the relations that turn (ω, J, g) into a compatible triple: J is a g-isometry, J is g-skew-adjoint, and ω is recovered from g and J. The capstone TauCeti.SymplecticForm.Compatible.innerProductCore exhibits g as an inner product, the witness that the pointwise compatibility definition is non-vacuous and behaves as a metric should; the energy of a J-holomorphic curve is measured against exactly this metric.

Main declarations

• TauCeti.SymplecticForm.associatedBilinForm_apply_right_apply: g(v, J w) = -ω(v, w), holding for any J from the identity J² = -1 alone.
• TauCeti.SymplecticForm.Invariant.associatedBilinForm_apply_left_apply: g(J v, w) = ω(v, w), recovering ω from the metric.
• TauCeti.SymplecticForm.Invariant.associatedBilinForm_invariant: J is a g-isometry, g(J v, J w) = g(v, w).
• TauCeti.SymplecticForm.Invariant.associatedBilinForm_skewAdjoint: J is g-skew-adjoint, g(J v, w) = -g(v, J w).
• TauCeti.SymplecticForm.Invariant.associatedBilinForm_add_apply_self: the symmetric polarization identity for g(a + J b, a + J b).
• TauCeti.SymplecticForm.associatedBilinForm_apply_apply_of_isComplexLinearMap: symplectic complex-linear maps preserve the metric.
• TauCeti.SymplecticForm.Compatible.innerProductCore: the metric of a compatible pair as an InnerProductSpace.Core ℝ V.
• TauCeti.SymplecticForm.abs_apply_le_norm_mul_norm: when the inner product of V is the metric ω(·, J ·), the symplectic form is bounded by it, |ω(v, w)| ≤ ‖v‖ ‖w‖.

The conventions follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1: a compatible pair (ω, J) determines a metric g(v, w) = ω(v, J w).

theorem TauCeti.SymplecticForm.associatedBilinForm_apply_right_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (v w : V) : ((ω.associatedBilinForm J) v) (J.toLinearMap w) = -(fun (v w : V) => (ω.toBilinForm v) w) v w

Applying J to the right argument of the metric g(v, w) = ω(v, J w) negates the symplectic form: g(v, J w) = -ω(v, w). This uses only J² = -1, not compatibility.

@[simp]

theorem TauCeti.SymplecticForm.Invariant.apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) : (fun (v w : V) => (ω.toBilinForm v) w) (J.toLinearMap v) (J.toLinearMap w) = (fun (v w : V) => (ω.toBilinForm v) w) v w

Pointwise form of invariance under applying J to both arguments.

theorem TauCeti.SymplecticForm.Invariant.associatedBilinForm_apply_left_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) : ((ω.associatedBilinForm J) (J.toLinearMap v)) w = (fun (v w : V) => (ω.toBilinForm v) w) v w

The metric recovers the symplectic form: g(J v, w) = ω(v, w).

theorem TauCeti.SymplecticForm.Invariant.symplecticForm_apply_eq_associatedBilinForm_apply_left_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) : (fun (v w : V) => (ω.toBilinForm v) w) v w = ((ω.associatedBilinForm J) (J.toLinearMap v)) w

Pointwise recovery of the symplectic form from the metric and J: ω(v, w) = g(J v, w).

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

J is an isometry of the metric g: g(J v, J w) = g(v, w).

theorem TauCeti.SymplecticForm.Invariant.associatedBilinForm_skewAdjoint {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) : ((ω.associatedBilinForm J) (J.toLinearMap v)) w = -((ω.associatedBilinForm J) v) (J.toLinearMap w)

J is skew-adjoint for the metric g: g(J v, w) = -g(v, J w).

theorem TauCeti.SymplecticForm.Invariant.associatedBilinForm_add_apply_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (a b : V) : ((ω.associatedBilinForm J) (a + J.toLinearMap b)) (a + J.toLinearMap b) = ((ω.associatedBilinForm J) a) a + ((ω.associatedBilinForm J) b) b - 2 * (fun (v w : V) => (ω.toBilinForm v) w) a b

The polarization identity for the associated metric of a J-invariant form: g(a + J b, a + J b) = g(a, a) + g(b, b) - 2 ω(a, b), where g = ω.associatedBilinForm J.

theorem TauCeti.SymplecticForm.associatedBilinForm_self_nonneg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hpositive : (LinearMap.BilinMap.toQuadraticMap (ω.associatedBilinForm J)).PosDef) (v : V) : 0 ≤ ((ω.associatedBilinForm J) v) v

The metric g(v, v) = ω(v, J v) is nonnegative under positive-definiteness.

theorem TauCeti.SymplecticForm.symplecticForm_apply_apply_self_nonneg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hpositive : (LinearMap.BilinMap.toQuadraticMap (ω.associatedBilinForm J)).PosDef) (v : V) : 0 ≤ (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap v)

The diagonal ω(v, J v) is nonnegative under positive-definiteness of the associated metric.

theorem TauCeti.SymplecticForm.associatedBilinForm_self_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hpositive : (LinearMap.BilinMap.toQuadraticMap (ω.associatedBilinForm J)).PosDef) {v : V} : ((ω.associatedBilinForm J) v) v = 0 ↔ v = 0

Positive-definiteness of the associated metric detects zero vectors on the diagonal.

theorem TauCeti.SymplecticForm.associatedBilinForm_apply_apply_of_isComplexLinearMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} {W : Type u_2} [AddCommGroup W] [Module ℝ W] {ω₂ : SymplecticForm W} {J₂ : AlmostComplexStructure W} {F : V →ₗ[ℝ] W} (hω : ∀ (v w : V), (fun (v w : W) => (ω₂.toBilinForm v) w) (F v) (F w) = (fun (v w : V) => (ω.toBilinForm v) w) v w) (hF : IsComplexLinearMap J J₂ F) (v w : V) : ((ω₂.associatedBilinForm J₂) (F v)) (F w) = ((ω.associatedBilinForm J) v) w

A linear map carrying ω to ω₂ and complex linear from J to J₂ carries the metric ω(·, J ·) to the metric ω₂(·, J₂ ·). In particular a symplectic map commuting with J preserves the metric of (ω, J).

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

The metric recovers the symplectic form: g(J v, w) = ω(v, w).

theorem TauCeti.SymplecticForm.Compatible.symplecticForm_apply_eq_associatedBilinForm_apply_left_apply {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 = ((ω.associatedBilinForm J) (J.toLinearMap v)) w

Pointwise recovery of the symplectic form from the metric and J: ω(v, w) = g(J v, w).

theorem TauCeti.SymplecticForm.Compatible.associatedBilinForm_invariant {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) : ((ω.associatedBilinForm J) (J.toLinearMap v)) (J.toLinearMap w) = ((ω.associatedBilinForm J) v) w

J is an isometry of the metric g: g(J v, J w) = g(v, w).

theorem TauCeti.SymplecticForm.Compatible.associatedBilinForm_skewAdjoint {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v w : V) : ((ω.associatedBilinForm J) (J.toLinearMap v)) w = -((ω.associatedBilinForm J) v) (J.toLinearMap w)

J is skew-adjoint for the metric g: g(J v, w) = -g(v, J w).

theorem TauCeti.SymplecticForm.Compatible.associatedBilinForm_self_nonneg {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) (v : V) : 0 ≤ ((ω.associatedBilinForm J) v) v

The metric g(v, v) = ω(v, J v) is nonnegative.

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

The diagonal ω(v, J v) of the associated metric is nonnegative.

theorem TauCeti.SymplecticForm.Compatible.associatedBilinForm_self_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) {v : V} : ((ω.associatedBilinForm J) v) v = 0 ↔ v = 0

The metric is positive definite in the sense that g(v, v) = 0 exactly when v = 0.

@[implicit_reducible]

noncomputable def TauCeti.SymplecticForm.Compatible.innerProductCore {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (h : ω.Compatible J) : InnerProductSpace.Core ℝ V

The metric of a compatible pair, packaged as an InnerProductSpace.Core ℝ V.

The inner product is the associated metric ⟪v, w⟫ = ω(v, J w).

@[simp]

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

The inner product from innerProductCore is the associated metric ω(v, J w).

theorem TauCeti.SymplecticForm.invariant_of_apply_apply_eq_inner {V : Type u_2} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hg : ∀ (v w : V), (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap w) = inner ℝ v w) : ω.Invariant J

Identifying the associated metric with a real inner product makes the symplectic form invariant under the almost complex structure.

theorem TauCeti.SymplecticForm.norm_apply_eq_norm_of_apply_apply_self_eq_inner {V : Type u_2} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hg : ∀ (v : V), (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap v) = inner ℝ v v) (v : V) : ‖J.toLinearMap v‖ = ‖v‖

The almost complex structure preserves a norm when its squared norm is the diagonal ω(v, J v). Only equality on the diagonal is needed.

theorem TauCeti.SymplecticForm.abs_apply_le_norm_mul_norm {V : Type u_2} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hg : ∀ (v w : V), (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap w) = inner ℝ v w) (v w : V) : |(fun (v w : V) => (ω.toBilinForm v) w) v w| ≤ ‖v‖ * ‖w‖

If the inner product of V is the metric ω(·, J ·) of a symplectic form and an almost complex structure, then ω is bounded by the inner product norm: |ω(v, w)| ≤ ‖v‖ ‖w‖.