Bounded point evaluation and joint continuity of reconstructed ordinary-space fields.

theorem EulerMeanSmoothRepresentative.instMeanSpatialEvaluation1 : Fact (0 < 1)

theorem EulerMeanSmoothRepresentative.ordinaryLift_representative_ae (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) : ↑↑(EulerMeanOrdinaryLift.ordinaryLift u) =ᵐ[EulerLiftedGradientSpace.liftMeasure 1] fun (x : EulerLiftedGradientSpace.LiftDomain 1) => representative u hu x.1

theorem EulerMeanSmoothRepresentative.pointEvaluation_ordinary (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (x : EulerSmoothLimit.Space) : (EulerSobolevPointEvaluation.pointEvaluation 1 (x, 0)) (ordinarySobolev 3 u hu) = representative u hu x

The previously constructed bounded Sobolev evaluation is the actual ordinary representative.

theorem EulerMeanSmoothRepresentative.representative_bound (u : ↥EulerMeanSolenoidal.L2) (hu : SmoothOrbit u) (x : EulerSmoothLimit.Space) : ‖representative u hu x‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant 1 3 * ∑ n ∈ Finset.range 4, ‖iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) u) 0‖

Point values are controlled by finitely many actual L² derivatives, uniformly in the spatial point.

theorem EulerMeanSmoothRepresentative.representative_joint_continuous {T : Type u_1} [TopologicalSpace T] (u : T → ↥EulerMeanSolenoidal.L2) (hu : ∀ (t : T), SmoothOrbit (u t)) (hjet : ∀ n ≤ 3, Continuous fun (t : T) => iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (u t)) 0) : Continuous fun (p : T × EulerSmoothLimit.Space) => representative (u p.1) ⋯ p.2

A family with continuous genuine L² derivatives through order three has jointly continuous values.