Actual smooth cylinder fields from continuous mixed-orbit paths

Uniform-time mixed L² regularity constructs a jointly continuous genuine representative, smooth in all spatial/angular variables. A continuous L² time right-hand side lifts through the injective Sobolev inclusion and yields the actual pointwise within-time derivative, including both interval endpoints.

noncomputable def EulerCylinderSmoothOrbit.pointField (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (t : K) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSmoothLimit.Space

The genuine representative obtained by bounded H3 point evaluation.

Equations

• EulerCylinderSmoothOrbit.pointField period p hp t x = (EulerSobolevPointEvaluation.pointEvaluation period x) ((EulerCylinderSmoothOrbit.sobolevPath period 3 p hp) t)

theorem EulerCylinderSmoothOrbit.pointField_joint_continuous (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) : Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain period) => pointField period p hp z.1 z.2

The reconstructed field is jointly continuous in time and cylinder position.

theorem EulerCylinderSmoothOrbit.pointField_eq_representative (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (t : K) : pointField period p hp t = representative period (p t) ⋯

The bounded point evaluation is exactly the smooth representative of each actual L² slice.

theorem EulerCylinderSmoothOrbit.pointField_smooth (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (t : K) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (pointField period p hp t) x)

Every time slice is genuinely smooth in all three spatial and the angular variable.

theorem EulerCylinderSmoothOrbit.pointField_ae (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (t : K) : ↑↑(p t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] pointField period p hp t

The reconstructed field represents the original, rather than a separate chosen solution.

theorem EulerCylinderSmoothOrbit.sobolevPath_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (sobolevPath period q p hp)) ((sobolevPath period q f hf) t) (Set.Icc 0 T) ↑t

The time equation is actual in each complete Sobolev space, by injectivity of its L² inclusion.

theorem EulerCylinderSmoothOrbit.pointField_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) f) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : HasDerivWithinAt (fun (s : ℝ) => pointField period p hp (Set.projIcc 0 T hT s) x) (pointField period f hf t x) (Set.Icc 0 T) ↑t

The pointwise PDE time derivative holds within the closed interval at every cylinder point.