A genuine coherent cylinder tower with a weighted bound yields actual ordinary three-dimensional smooth L² slices and bounded coefficient paths. The zero-angle restriction costs one fixed radius enlargement, independent of the derivative order.

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey2 : NormedSpace ℝ EulerSmoothLimit.Space

Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey3 : NormedAddCommGroup EulerLiftedGradientSpace.LiftTangent

Cache the standard NormedAddCommGroup LiftTangent instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey3 = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey4 : NormedSpace ℝ EulerLiftedGradientSpace.LiftTangent

Cache the standard NormedSpace ℝ LiftTangent instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey4 = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey5 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (LiftTangent [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey5 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey6 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (LiftTangent [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey6 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey7 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey7 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey8 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey8 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey9 {T : ℝ} (n : ℕ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey9 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey10 (n : ℕ) : NormedAddCommGroup (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey10 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey11 (n : ℕ) : NormedSpace ℝ (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space [×n]→L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey11 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey12 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ (Space [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey12 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey13 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ (Space [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey13 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey14 {T : ℝ} (n : ℕ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, Space →ᵇ (Space [×n]→L[ℝ] Space)) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerGraphGevrey14 n = inferInstance

noncomputable def EulerAllOrderCorrectionData.FieldTower.zeroGraphField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Zero graph field, bundling field, smooth, integrable.

Equations

• A.zeroGraphField t = { field := A.physicalPointField 1 0 t, smooth := ⋯, integrable := ⋯ }

noncomputable def EulerAllOrderCorrectionData.FieldTower.zeroGraphCoefficient {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) : SmoothTimeField (↑(Set.Icc 0 T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

Zero graph coefficient, given by A.toSmoothTimeField.precompLinear (ContinuousLinearMap.inl ℝ Space ℝ).

Equations

• A.zeroGraphCoefficient = A.toSmoothTimeField.precompLinear (ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ)

@[simp]

theorem EulerAllOrderCorrectionData.FieldTower.zeroGraphField_apply {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (A.zeroGraphField t).field x = A.pointField t (EulerLiftedGradientSpace.coveringMap P (x, 0))

@[simp]

theorem EulerAllOrderCorrectionData.FieldTower.zeroGraphCoefficient_apply {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (A.zeroGraphCoefficient.field t) x = (A.zeroGraphField t).field x

theorem EulerAllOrderCorrectionData.FieldTower.zeroGraphField_jetLp {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (A.zeroGraphField t).jetLp n = (A.physicalTensorPath 1 0 n) t

theorem EulerAllOrderCorrectionData.FieldTower.zeroGraphField_jetLp_continuous {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (A.zeroGraphField t).jetLp n

theorem EulerAllOrderCorrectionData.FieldTower.zeroGraphCoefficient_bound {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (ρ C : ℝ) (hρ : 0 < ρ) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ ((A.realization (n + 6)) t) ≤ C) (n : ℕ) : ‖A.zeroGraphCoefficient.jet n‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * C * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * ρ⁻¹) ^ n * ↑n.factorial ^ 2

theorem EulerAllOrderCorrectionData.FieldTower.zeroGraphField_bound {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (ρ C : ℝ) (hρ : 0 < ρ) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n ρ ((A.realization (n + 6)) t) ≤ C) (t : ↑(Set.Icc 0 T)) : (A.zeroGraphField t).HasJetBound (√(2 / P + 2 * P) * C * (1 + ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * ρ⁻¹)) (4 * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * ρ⁻¹))