Norm of the real physical part of a complete Sobolev path

Taking the physical realization and real part is contractive on continuous complete H²ᵏ trajectories.

theorem CKN.Leray.regularisedBesselRealPartPath_norm_le (k : ℕ) (T : ℝ) (u : C(↑(RegularizedMildTimeInterval T), BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2)) : ‖regularisedBesselRealPartPath k T u‖ ≤ ‖u‖

The real physical part of a complete H²ᵏ path has no larger continuous trajectory norm.