Exact coefficient functionals for the lifted Euler transport vector (κz,m·z).

noncomputable def EulerSobolevTransport.velocityComponents (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ

Coordinate functionals of the actual lifted transport vector, with the angle coordinate first.

Equations

• EulerSobolevTransport.velocityComponents κ m = Fin.cons ((innerSL ℝ) m) fun (i : Fin 3) => κ • EulerVectorCylinder.coordinate 3 i

theorem EulerSobolevTransport.velocityComponents_norm (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hκ : |κ| ≤ 1) (hm : ‖m‖ ≤ 1) (i : Fin 4) : ‖velocityComponents κ m i‖ ≤ 1

The scale-normalized lifted velocity coefficients have norm at most one.

theorem EulerSobolevTransport.velocityComponents_direction (κ : ℝ) (m z : EulerLiftedGradientSpace.Vector3) : ∑ i : Fin 4, (velocityComponents κ m i) z • EulerCylinderSobolev.standardDirection i = EulerMetricTransport.transportDirection κ m z

These functionals recover exactly the four-dimensional transport direction.