Jointly continuous ordinary spatial representatives of continuous L² paths with smooth spatial orbits.

theorem EulerMeanSmoothRepresentative.instMeanPathSpatialRepresentative1 : Fact (0 < 1)

theorem EulerMeanSmoothRepresentative.path_orbit_tensor_evaluation (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (n : ℕ) (t : ↑(Set.Icc 0 T)) : iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (p t)) 0 = (ContinuousMap.evalCLM ℝ t).compContinuousMultilinearMap (iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) 0)

Evaluation at time commutes with every actual spatial derivative tensor.

theorem EulerMeanSmoothRepresentative.ordinarySobolev_path_continuous (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (q : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => ordinarySobolev q (p t) ⋯

The finite Sobolev array is a continuous path, constructed from actual tensor evaluations. No operator-norm continuity of the time-evaluation operators is needed.

theorem EulerMeanSmoothRepresentative.path_representative_joint_continuous (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) : Continuous fun (z : ↑(Set.Icc 0 T) × EulerSmoothLimit.Space) => representative (p z.1) ⋯ z.2

The reconstructed spatial field is jointly continuous in actual time and space.

theorem EulerMeanSmoothRepresentative.path_representative_smooth (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (representative (p t) ⋯)

theorem EulerMeanSmoothRepresentative.path_representative_ae (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) : ↑↑(p t) =ᵐ[MeasureTheory.volume] representative (p t) ⋯