Joint continuity of evaluation of genuine cylinder Sobolev fields.

theorem EulerSobolevJointEvaluation.pointEvaluation_norm_le (period : ℝ) [Fact (0 < period)] (x : EulerLiftedGradientSpace.LiftDomain period) : ‖EulerSobolevPointEvaluation.pointEvaluation period x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant period 3

The actual point-evaluation operators have a uniform bound independent of the spatial point.

theorem EulerSobolevJointEvaluation.pointEvaluation_joint_continuous (period : ℝ) [Fact (0 < period)] : Continuous fun (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3) × EulerLiftedGradientSpace.LiftDomain period) => (EulerSobolevPointEvaluation.pointEvaluation period p.2) p.1

Evaluation is jointly continuous in a genuine H3 field and a cylinder point.

theorem EulerSobolevJointEvaluation.path_representative_joint_continuous (period : ℝ) [Fact (0 < period)] {T : Type u_1} [TopologicalSpace T] (u : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) : Continuous fun (p : T × EulerLiftedGradientSpace.LiftDomain period) => (EulerSobolevPointEvaluation.pointEvaluation period p.2) (u p.1)

Every continuous genuine H3 path has a jointly continuous actual spatial representative.