Real physical paths in the complete Sobolev trajectory space

The physical real-part path is continuous, and paths whose physical realization equals that complexification form a closed subset.

noncomputable def CKN.Leray.regularisedBesselRealPartPath (k : ℕ) (T : ℝ) (u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) : C(↑(RegularizedMildTimeInterval T), ↥RealVectorL2)

The real physical part of a complete H²ᵏ velocity trajectory.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.regularisedBesselRealPath_isClosed (k : ℕ) (T : ℝ) : IsClosed {u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2) | ∀ (t : ↑(RegularizedMildTimeInterval T)), (regularisedBesselSobolevToL2CLM ↑(2 * k) ⋯) (u t) = complexifyVectorL2 ((regularisedBesselRealPartPath k T u) t)}

The complete H²ᵏ trajectories representing real physical L² paths form a closed subset of the continuous trajectory Banach space.