The actual smooth cylinder paths produced by the packet construction give coherent continuous Sobolev realizations at every finite order.

noncomputable def EulerPacketCylinderField.Field.toFieldTower {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : EulerAllOrderCorrectionData.FieldTower P T

No Sobolev realizations are hypothesized: each is constructed from the genuine mixed translation orbit of the prescribed field.

Equations

• G.toFieldTower = { field := G.path, realization := fun (q : ℕ) => EulerCylinderSmoothOrbit.sobolevPath P q G.path ⋯, value_eq := ⋯ }

@[simp]

theorem EulerPacketCylinderField.Field.toFieldTower_field {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : G.toFieldTower.field = G.path

@[simp]

theorem EulerPacketCylinderField.Field.toFieldTower_realization {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (q : ℕ) : G.toFieldTower.realization q = EulerCylinderSmoothOrbit.sobolevPath P q G.path ⋯

theorem EulerPacketCylinderField.Field.toFieldTower_value {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value P ((G.toFieldTower.realization q) t) = G.path t

theorem EulerPacketCylinderField.Field.toFieldTower_value_ae {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (q : ℕ) (t : ↑(Set.Icc 0 T)) : ↑↑(EulerCylinderSobolevSpace.value P ((G.toFieldTower.realization q) t)) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerCylinderSmoothOrbit.pointField P G.path ⋯ t

The common value has the very same pointwise cylinder representative as the literal packet field.

theorem EulerPacketCylinderField.Field.toFieldTower_hasDerivWithinAt {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hT : 0 ≤ T) (hd : TimeDerivative hT G H) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (G.toFieldTower.realization q)) ((H.toFieldTower.realization q) t) (Set.Icc 0 T) ↑t

Genuine time derivatives lift simultaneously to all finite Sobolev orders, including the one-sided derivatives at the interval endpoints.