Ambient geometry for the optimal-transport / Vlasov development

Throughout, d : ℕ is the spatial dimension. Single-particle physical space is ℝ^d realised as a Euclidean space; single-particle phase space is its square (position × velocity). These are the shared ambient types that both the optimal-transport layer and the kinetic (Vlasov) layer are built over.

@[reducible, inline]

abbrev Vlasov.PhysSpace (d : ℕ) : Type

Abbreviation for ℝ^d as a Euclidean space.

Equations

• Vlasov.PhysSpace d = EuclideanSpace ℝ (Fin d)

@[reducible, inline]

abbrev Vlasov.PhaseSpace (d : ℕ) : Type

Abbreviation for the single-particle phase space ℝ^d × ℝ^d.

Equations

• Vlasov.PhaseSpace d = (Vlasov.PhysSpace d × Vlasov.PhysSpace d)