Contraction with a symplectic form

On a finite-dimensional real normed space, contraction with a symplectic form is an invertible continuous linear map to the continuous dual. This identifies covectors with vectors and allows the contraction equation in Moser's deformation argument to be solved using the continuous-linear-map inverse. The symplectic pairing of two continuous maps is continuous, and that of two differentiable curves satisfies the product rule. The pairing is bounded by the operator norm of the form.

See McDuff--Salamon, Introduction to Symplectic Topology, Section 3.2.

@[simp]

theorem TauCeti.SymplecticForm.isInvertible_toContinuousBilinearMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : (LinearMap.toContinuousBilinearMap ω.toBilinForm).IsInvertible

Contraction with a finite-dimensional symplectic form is an isomorphism to the continuous dual.

theorem TauCeti.SymplecticForm.continuousOn_apply_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {X : Type u_2} [TopologicalSpace X] {p q : X → V} {s : Set X} (ω : SymplecticForm V) (hp : ContinuousOn p s) (hq : ContinuousOn q s) : ContinuousOn (fun (z : X) => (fun (v w : V) => (ω.toBilinForm v) w) (p z) (q z)) s

The symplectic pairing of two maps continuous on a set is continuous on that set.

theorem TauCeti.SymplecticForm.continuous_apply_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {X : Type u_2} [TopologicalSpace X] {p q : X → V} (ω : SymplecticForm V) (hp : Continuous p) (hq : Continuous q) : Continuous fun (z : X) => (fun (v w : V) => (ω.toBilinForm v) w) (p z) (q z)

The symplectic pairing of two continuous maps is continuous.

theorem TauCeti.SymplecticForm.abs_apply_le_opNorm_mul_norm_mul_norm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (v w : V) : |(fun (v w : V) => (ω.toBilinForm v) w) v w| ≤ ‖LinearMap.toContinuousBilinearMap ω.toBilinForm‖ * ‖v‖ * ‖w‖

A symplectic form on a finite-dimensional space is bounded by the operator norm of its continuous bilinear map: |ω(v, w)| ≤ ‖ω‖ ‖v‖ ‖w‖.

theorem TauCeti.SymplecticForm.hasDerivAt_apply_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {p q : ℝ → V} {p' q' : V} {t : ℝ} (hp : HasDerivAt p p' t) (hq : HasDerivAt q q' t) : HasDerivAt (fun (t : ℝ) => (fun (v w : V) => (ω.toBilinForm v) w) (p t) (q t)) ((fun (v w : V) => (ω.toBilinForm v) w) p' (q t) + (fun (v w : V) => (ω.toBilinForm v) w) (p t) q') t

The product rule for the symplectic pairing of two curves.