Exact classical mixed-word norms of the reconstructed cylinder field

The actual classical spatial/angular derivatives represent the exact L² translation words. Consequently the fixed-Hq external-word sum equals the block used by the inverse estimate, with no alphabet factor or radius loss.

noncomputable def EulerCylinderSmoothOrbit.strongWord (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) {n : ℕ} (w : Fin n → Fin 4) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual strong L² derivative for an ordered mixed word.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerCylinderSmoothOrbit.strongWord_zero (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (w : Fin 0 → Fin 4) : strongWord period u w = u

theorem EulerCylinderSmoothOrbit.strongWord_snoc (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) {n : ℕ} (w : Fin n → Fin 4) (i : Fin 4) : strongWord period u (Fin.snoc w i) = strongWord period (orbitDerivative period u (EulerCylinderSobolev.standardDirection i)) w

Appending a direction differentiates the actual field.

theorem EulerCylinderSmoothOrbit.strongWord_translation (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) {n : ℕ} (w : Fin n → Fin 4) (a : EulerLiftedGradientSpace.LiftTangent) : (EulerLpCylinderTranslation.translate period a) (strongWord period u w) = EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) u) w a

A strong word is the actual mixed derivative at each translated label.

theorem EulerCylinderSmoothOrbit.strongWord_smooth (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) {n : ℕ} (w : Fin n → Fin 4) : SmoothOrbit period (strongWord period u w)

Every strong word has its genuine smooth full mixed orbit.

theorem EulerCylinderSmoothOrbit.strongWord_ae (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) {n : ℕ} (w : Fin n → Fin 4) : ↑↑(strongWord period u w) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCylinderSobolev.iteratedFieldDerivative period w (representative period u hu)

The genuine strong word represents the literal classical cylinder derivative.

theorem EulerCylinderSmoothOrbit.representative_strongWord (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) {n : ℕ} (w : Fin n → Fin 4) : representative period (strongWord period u w) ⋯ = EulerCylinderSobolev.iteratedFieldDerivative period w (representative period u hu)

The reconstructed derivative representative equals the actual classical derivative pointwise.

theorem EulerCylinderSmoothOrbit.classicalWord_memLp (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) {n : ℕ} (w : Fin n → Fin 4) : MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (representative period u hu)) 2 (EulerLiftedGradientSpace.liftMeasure period)

Every actual classical mixed derivative lies in L²; this is proved from the solved orbit.

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

The actual classical Hq norm is exactly the finite mixed-word base sum.

noncomputable def EulerCylinderSmoothOrbit.classicalBlockSize (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (n : ℕ) : ℝ

The source's actual fixed-Hq external-word sum, on the literal classical field.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerCylinderSmoothOrbit.classicalBlockSize_eq (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hu : SmoothOrbit period u) (n : ℕ) : classicalBlockSize period q u hu n = EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) u) n 0

Exact norm identification, with no dimension factor and no radius enlargement.

theorem EulerCylinderSmoothOrbit.path_classicalBlockSize_le (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) (n : ℕ) : classicalBlockSize period q (p t) ⋯ n ≤ EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) p) n 0

Time evaluation is a contraction, including for the full actual mixed-word Hq norm.