An actual coherent Sobolev tower gives a smooth bounded coefficient on the real cylinder cover, including all spatial jets in the continuous uniform time norm. The construction uses its genuine derivative words; no translation-orbit hypothesis is added.

Continuous bounded coordinate fields reconstruct the actual tensor field. This is a qualitative finite-dimensional construction; subsequent norm estimates can use the actual tensor equality without a coordinate reassembly constant.

@[instance_reducible]

noncomputable def EulerBoundedTensorCoordinates.instBoundedTensorCoordinates1 {E : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] V)

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

Equations

• EulerBoundedTensorCoordinates.instBoundedTensorCoordinates1 n = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedTensorCoordinates.instBoundedTensorCoordinates2 {E : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] V)

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

Equations

• EulerBoundedTensorCoordinates.instBoundedTensorCoordinates2 n = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedTensorCoordinates.instBoundedTensorCoordinates3 {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction X (E [×n]→L[ℝ] V))

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

Equations

• EulerBoundedTensorCoordinates.instBoundedTensorCoordinates3 n = inferInstance

@[instance_reducible]

noncomputable def EulerBoundedTensorCoordinates.instBoundedTensorCoordinates4 {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction X (E [×n]→L[ℝ] V))

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

Equations

• EulerBoundedTensorCoordinates.instBoundedTensorCoordinates4 n = inferInstance

noncomputable def EulerBoundedTensorCoordinates.coordinates {E : Type u_3} {V : Type u_4} {ι : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (b : Module.Basis ι ℝ E) (n : ℕ) : (E [×n]→L[ℝ] V) →L[ℝ] (Fin n → ι) → V

Coordinates, given by ContinuousLinearMap.pi (fun w => (ContinuousLinearMap.id ℝ (E [×n]→L[ℝ] V)).flipMultilinear (fun i => b (w i))).

Equations

• EulerBoundedTensorCoordinates.coordinates b n = ContinuousLinearMap.pi fun (w : Fin n → ι) => (ContinuousLinearMap.id ℝ (E [×n]→L[ℝ] V)).flipMultilinear fun (i : Fin n) => b (w i)

theorem EulerBoundedTensorCoordinates.coordinates_injective {E : Type u_3} {V : Type u_4} {ι : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (b : Module.Basis ι ℝ E) (n : ℕ) : Function.Injective ⇑(coordinates b n)

noncomputable def EulerBoundedTensorCoordinates.reassembly {E : Type u_3} {V : Type u_4} {ι : Type u_5} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : Module.Basis ι ℝ E) (n : ℕ) : ((Fin n → ι) → V) →L[ℝ] E [×n]→L[ℝ] V

Reassembly, given by ((coordinates (V := V) b n).toLinearMap.leftInverse).toContinuousLinearMap.

Equations

• EulerBoundedTensorCoordinates.reassembly b n = LinearMap.toContinuousLinearMap (↑(EulerBoundedTensorCoordinates.coordinates b n)).leftInverse

theorem EulerBoundedTensorCoordinates.reassembly_coordinates {E : Type u_3} {V : Type u_4} {ι : Type u_5} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : Module.Basis ι ℝ E) (n : ℕ) (A : E [×n]→L[ℝ] V) : (reassembly b n) ((coordinates b n) A) = A

noncomputable def EulerBoundedTensorCoordinates.tupleBounded {X : Type u_2} {V : Type u_4} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] {j : Type u_6} [Fintype j] : (j → BoundedContinuousFunction X V) →L[ℝ] BoundedContinuousFunction X (j → V)

Tuple bounded as an element of (j → (X →ᵇ V)) →L[ℝ] (X →ᵇ (j → V)).

Equations

• EulerBoundedTensorCoordinates.tupleBounded = ∑ i : j, ContinuousLinearMap.compLeftContinuousBounded X (ContinuousLinearMap.single ℝ (fun (x : j) => V) i) ∘SL ContinuousLinearMap.proj i

theorem EulerBoundedTensorCoordinates.tupleBounded_apply {X : Type u_2} {V : Type u_4} [TopologicalSpace X] [NormedAddCommGroup V] [NormedSpace ℝ V] {j : Type u_6} [Fintype j] (u : j → BoundedContinuousFunction X V) (x : X) (i : j) : (tupleBounded u) x i = (u i) x

noncomputable def EulerBoundedTensorCoordinates.coordinatePath {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} {ι : Type u_5} [TopologicalSpace K] [TopologicalSpace X] [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : Module.Basis ι ℝ E) (n : ℕ) (u : (Fin n → ι) → C(K, BoundedContinuousFunction X V)) : C(K, BoundedContinuousFunction X (E [×n]→L[ℝ] V))

Coordinate path, bundling toFun, continuous_toFun.

Equations

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

theorem EulerBoundedTensorCoordinates.coordinatePath_eq {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} {ι : Type u_5} [TopologicalSpace K] [TopologicalSpace X] [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : Module.Basis ι ℝ E) (n : ℕ) (u : (Fin n → ι) → C(K, BoundedContinuousFunction X V)) (t : K) (x : X) (A : E [×n]→L[ℝ] V) (hu : ∀ (w : Fin n → ι), ((u w) t) x = A fun (i : Fin n) => b (w i)) : ((coordinatePath b n u) t) x = A

noncomputable def SmoothTimeField.ofCoordinateJets {K E V ι : Type u} [TopologicalSpace K] [CompactSpace K] [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (b : Module.Basis ι ℝ E) (f : C(K, BoundedContinuousFunction E V)) (hf : ∀ (t : K), ContDiff ℝ ↑⊤ ⇑(f t)) (u : (n : ℕ) → (Fin n → ι) → C(K, BoundedContinuousFunction E V)) (hu : ∀ (n : ℕ) (w : Fin n → ι) (t : K) (x : E), ((u n w) t) x = (iteratedFDeriv ℝ n (⇑(f t)) x) fun (i : Fin n) => b (w i)) : SmoothTimeField K E V

Of coordinate jets, bundling field, smooth, jet, jet_eq.

Equations

• SmoothTimeField.ofCoordinateJets b f hf u hu = { field := f, smooth := hf, jet := fun (n : ℕ) => EulerBoundedTensorCoordinates.coordinatePath b n (u n), jet_eq := ⋯ }

noncomputable def EulerAllOrderCorrectionData.FieldTower.coverBasis : Module.Basis (Fin 4) ℝ EulerLiftedGradientSpace.LiftTangent

Cover basis, given by (EuclideanSpace.basisFun (Fin 4) ℝ).toBasis.map coordinateLinearEquiv.

Equations

• EulerAllOrderCorrectionData.FieldTower.coverBasis = (EuclideanSpace.basisFun (Fin 4) ℝ).toBasis.map EulerCylinderCoordinates.coordinateLinearEquiv

@[simp]

theorem EulerAllOrderCorrectionData.FieldTower.coverBasis_apply (i : Fin 4) : coverBasis i = EulerCylinderSobolev.standardDirection i

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField1 {P : ℝ} [Fact (0 < P)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

Cache the standard NormedAddCommGroup (SobolevSpace P q) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField1 q = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField2 {P : ℝ} [Fact (0 < P)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

Cache the standard NormedSpace ℝ (SobolevSpace P q) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField2 q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField3 n = inferInstance

@[instance_reducible]

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

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

Equations

• EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField4 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField5 (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.instFieldTowerSmoothTimeField5 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.instFieldTowerSmoothTimeField6 (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.instFieldTowerSmoothTimeField6 n = inferInstance

noncomputable def EulerAllOrderCorrectionData.FieldTower.boundedCover {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Bounded cover, given by coverPathMap P (A.realization 3).

Equations

• A.boundedCover = (EulerCylinderBoundedCover.coverPathMap P) (A.realization 3)

@[simp]

theorem EulerAllOrderCorrectionData.FieldTower.boundedCover_apply {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (A.boundedCover t) x = A.pointField t (EulerLiftedGradientSpace.coveringMap P x)

noncomputable def EulerAllOrderCorrectionData.FieldTower.boundedWord {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (n : ℕ) (w : Fin n → Fin 4) : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space)

Bounded word, given by coverPathMap P ((wordAtLevel P 3 n w (le_refl (n+3))).compLeftContinuous ℝ (Icc (0 : ℝ) T) (A.realization (n+3))).

Equations

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

theorem EulerAllOrderCorrectionData.FieldTower.boundedWord_apply {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : ((A.boundedWord n w) t) x = EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) (EulerLiftedGradientSpace.coveringMap P x)

theorem EulerAllOrderCorrectionData.FieldTower.boundedWord_tensor {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : ((A.boundedWord n w) t) x = (iteratedFDeriv ℝ n (⇑(A.boundedCover t)) x) fun (i : Fin n) => coverBasis (w i)

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

To smooth time field, constructed using SmoothTimeField.ofCoordinateJets.

Equations

• A.toSmoothTimeField = SmoothTimeField.ofCoordinateJets EulerAllOrderCorrectionData.FieldTower.coverBasis A.boundedCover ⋯ A.boundedWord ⋯

@[simp]

theorem EulerAllOrderCorrectionData.FieldTower.toSmoothTimeField_apply {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (A.toSmoothTimeField.field t) x = A.pointField t (EulerLiftedGradientSpace.coveringMap P x)

theorem EulerAllOrderCorrectionData.FieldTower.toSmoothTimeField_timeDerivative {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) (hT : 0 ≤ T) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.realization 3)) ((B.realization 3) t) (Set.Icc 0 T) ↑t) : SmoothTimeField.TimeDerivative T hT A.toSmoothTimeField B.toSmoothTimeField

theorem EulerAllOrderCorrectionData.FieldTower.toSmoothTimeField_timeDerivative_of_interior {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) (hT : 0 ≤ T) (q : ℕ) (hq : 3 ≤ q) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization q)) ((B.realization q) ⟨t, ⋯⟩) t) : SmoothTimeField.TimeDerivative T hT A.toSmoothTimeField B.toSmoothTimeField

theorem EulerAllOrderCorrectionData.FieldTower.toSmoothTimeField_jet_norm_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), ‖iteratedFDeriv ℝ n (fun (y : EulerLiftedGradientSpace.LiftTangent) => A.pointField t (EulerLiftedGradientSpace.coveringMap P y)) x‖ ≤ C) : ‖A.toSmoothTimeField.jet n‖ ≤ C

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