Canonical smooth pointwise representatives of any genuine all-order field tower. All spatial regularity follows from its actual Sobolev jets.

noncomputable def EulerAllOrderCorrectionData.FieldTower.spatialJet {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (q : ℕ) (t : ↑(Set.Icc 0 T)) : EulerSpatialSobolevInverse.SpatialJet P EulerCylinderSobolev.standardDirection q (A.field t)

Spatial jet, given by A.value_eq q t ▸ toJet P (A.realization q t).

Equations

• A.spatialJet q t = ⋯ ▸ EulerCylinderSobolevSpace.toJet P ((A.realization q) t)

noncomputable def EulerAllOrderCorrectionData.FieldTower.pointField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerLiftedGradientSpace.Vector3

Point field, given by pointEvaluation P x (A.realization 3 t).

Equations

• A.pointField t x = (EulerSobolevPointEvaluation.pointEvaluation P x) ((A.realization 3) t)

theorem EulerAllOrderCorrectionData.FieldTower.pointField_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) : ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] A.pointField t

theorem EulerAllOrderCorrectionData.FieldTower.pointField_joint_continuous {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) : Continuous (Function.uncurry A.pointField)

theorem EulerAllOrderCorrectionData.FieldTower.pointField_unique {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hg : Continuous g) (ha : ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] g) : A.pointField t = g

theorem EulerAllOrderCorrectionData.FieldTower.pointField_smooth {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (A.pointField t) x)

theorem EulerAllOrderCorrectionData.FieldTower.restrict_realization {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) {p q : ℕ} (h : q ≤ p) (t : ↑(Set.Icc 0 T)) : (EulerCylinderSobolevSpace.restrictOperator P h) ((A.realization p) t) = (A.realization q) t

theorem EulerAllOrderCorrectionData.FieldTower.pointField_eq_high {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (q : ℕ) (hq : 3 ≤ q) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : A.pointField t x = (EulerSobolevPointEvaluation.pointEvaluation P x) ((EulerCylinderSobolevSpace.restrictOperator P hq) ((A.realization q) t))

theorem EulerAllOrderCorrectionData.FieldTower.pointField_hasDerivWithinAt {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) (hT : 0 ≤ T) (t : ↑(Set.Icc 0 T)) (hd : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.realization 3)) ((B.realization 3) t) (Set.Icc 0 T) ↑t) (x : EulerLiftedGradientSpace.LiftDomain P) : HasDerivWithinAt (fun (r : ℝ) => A.pointField (Set.projIcc 0 T hT r) x) (B.pointField t x) (Set.Icc 0 T) ↑t