Actual cylinder Sobolev arrays of smooth mixed translation orbits

Every coordinate is the literal L² derivative in its ordered spatial/angular word. The complete Sobolev norm is bounded by the exact finite word sum, and uniform-time mixed orbit regularity yields a continuous Sobolev path.

theorem EulerCylinderSmoothOrbit.iteratedFDeriv_orbitDerivative (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (v : EulerLiftedGradientSpace.LiftTangent) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) (m : Fin n → EulerLiftedGradientSpace.LiftTangent) : (iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) (orbitDerivative period u v)) a) m = (iteratedFDeriv ℝ (n + 1) (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) u) a) (Fin.snoc m v)

Iterating a genuine orbit derivative equals the next actual tensor derivative.

theorem EulerCylinderSmoothOrbit.spatialJet_word (period : ℝ) [Fact (0 < period)] (n q : ℕ) (hn : n ≤ q) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (w : Fin n → Fin 4) : (spatialJet period q u hu).word w = EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) w 0

Each actual strong jet word is its ordered mixed derivative in the true L² orbit.

theorem EulerCylinderSmoothOrbit.sobolev_coordinate (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (w : EulerCylinderSobolevSpace.SobolevWord q) : ↑(sobolev period q u hu) w = EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) w.snd 0

The actual coordinates of the complete Sobolev realization.

theorem EulerCylinderSmoothOrbit.sobolev_norm_le_baseSize (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) : ‖sobolev period q u hu‖ ≤ EulerParameterWordGevrey.baseSize EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) 0

A complete Sobolev norm is controlled by the genuine fixed-order word sum.

theorem EulerCylinderSmoothOrbit.path_evaluation_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) : SmoothOrbit period (p t)

Every time slice inherits genuine full mixed orbit smoothness.

theorem EulerCylinderSmoothOrbit.path_word_evaluation (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) {n : ℕ} (w : Fin n → Fin 4) (t : K) : EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) (p t)) w 0 = (EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) w 0) t

A time-slice word is evaluation of the actual uniform-time derivative word.

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

Genuine uniform-time mixed regularity gives continuity in every complete Sobolev norm.

noncomputable def EulerCylinderSmoothOrbit.sobolevPath (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) : C(K, ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The actual continuous Sobolev path.

Equations

• EulerCylinderSmoothOrbit.sobolevPath period q p hp = { toFun := fun (t : K) => EulerCylinderSmoothOrbit.sobolev period q (p t) ⋯, continuous_toFun := ⋯ }

@[simp]

theorem EulerCylinderSmoothOrbit.sobolevPath_value (period : ℝ) [Fact (0 < period)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (q : ℕ) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 period))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) (t : K) : EulerCylinderSobolevSpace.value period ((sobolevPath period q p hp) t) = p t