noncomputable def symplCapacity (r : ℝ) : NNReal

The symplectic capacity of a ball or cylinder of radius $r$, defined as $\pi r^2$.

class IsSymplecticBall {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type

Marker class identifying a symplectic manifold $S$ as the standard symplectic ball $B^{2n}(r)$ of radius $r > 0$.

• radius : ℝ
• halfDim : ℕ
• radius_pos : 0 < radius S
• halfDim_pos : 0 < halfDim S
• ω_exact : DifferentialFormSpace.IsExact' VF S.ω
• capacity_val : NNReal
• capacity_eq : capacity_val S = symplCapacity (radius S)

class IsSymplecticCylinder {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type

Marker class identifying a symplectic manifold $S$ as the standard symplectic cylinder $Z^{2n}(r) = B^2(r) \times \mathbb{R}^{2n-2}$.

• radius : ℝ
• halfDim : ℕ
• radius_pos : 0 < radius S
• halfDim_pos : 0 < halfDim S
• ω_exact : DifferentialFormSpace.IsExact' VF S.ω
• capacity_val : NNReal
• capacity_eq : capacity_val S = symplCapacity (radius S)

structure SymplecticEmbedding {Ω₁ : ℕ → Type u_1} {VF₁ : Type u_2} {Ω₂ : ℕ → Type u_3} {VF₂ : Type u_4} [inst₁ : DifferentialFormSpace Ω₁ VF₁] [inst₂ : DifferentialFormSpace Ω₂ VF₂] (S₁ : SymplecticManifold Ω₁ VF₁) (S₂ : SymplecticManifold Ω₂ VF₂) : Type (max u_1 u_3)

A symplectic embedding $\varphi : (S_1, \omega_1) \hookrightarrow (S_2, \omega_2)$: a morphism satisfying $\varphi^*\omega_2 = \omega_1$.

• toMorphism : DFSMorphism Ω₁ VF₁ Ω₂ VF₂
• pullback_symplectic : self.toMorphism.pullback S₂.ω = S₁.ω

structure SymplecticCapacity (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type u_1

A symplectic capacity $c$: a monotone invariant assigning $c(S) \in [0, \infty]$ to each symplectic manifold, satisfying $c(B^{2n}(r)) = c(Z^{2n}(r)) = \pi r^2$ (normalization) and $c(S_1) \le c(S_2)$ whenever $S_1$ embeds symplectically into $S_2$.

• cap : SymplecticManifold Ω VF → NNReal
• monotonicity (S₁ S₂ : SymplecticManifold Ω VF) (_φ : SymplecticEmbedding S₁ S₂) : self.cap S₁ ≤ self.cap S₂
• normalization_ball (S : SymplecticManifold Ω VF) [hBall : IsSymplecticBall S] : self.cap S = symplCapacity (IsSymplecticBall.radius S)
• normalization_cylinder (S : SymplecticManifold Ω VF) [hCyl : IsSymplecticCylinder S] : self.cap S = symplCapacity (IsSymplecticCylinder.radius S)

theorem SymplecticCapacity.cap_eq_ball_capacity_val {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (c : SymplecticCapacity Ω VF) (S : SymplecticManifold Ω VF) [hBall : IsSymplecticBall S] : c.cap S = IsSymplecticBall.capacity_val S

The capacity of a symplectic ball equals its stored capacity value: $c(B^{2n}(r)) = \pi r^2$.

theorem SymplecticCapacity.cap_eq_cylinder_capacity_val {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (c : SymplecticCapacity Ω VF) (S : SymplecticManifold Ω VF) [hCyl : IsSymplecticCylinder S] : c.cap S = IsSymplecticCylinder.capacity_val S

The capacity of a symplectic cylinder equals its stored capacity value: $c(Z^{2n}(r)) = \pi r^2$.

theorem SymplecticCapacity.cap_ball_eq_pi_rsq {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (c : SymplecticCapacity Ω VF) (S : SymplecticManifold Ω VF) [hBall : IsSymplecticBall S] : ↑(c.cap S) = Real.pi * IsSymplecticBall.radius S ^ 2

Numerical form of the ball normalization: $c(B^{2n}(r)) = \pi r^2$ as a real number.

theorem SymplecticCapacity.cap_cylinder_eq_pi_rsq {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (c : SymplecticCapacity Ω VF) (S : SymplecticManifold Ω VF) [hCyl : IsSymplecticCylinder S] : ↑(c.cap S) = Real.pi * IsSymplecticCylinder.radius S ^ 2

Numerical form of the cylinder normalization: $c(Z^{2n}(r)) = \pi r^2$ as a real number.