Actual smooth four-dimensional coefficients of the corrected packet. The lifted field equals the constructed exact velocity, has the genuine time derivative, is periodic, and has zero divergence.

Transposing a tensor with continuous bounded path values gives an actual continuous path of bounded tensor fields. Finite coordinates prove continuity; the norm estimate uses the original multilinear map directly and therefore has constant one.

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor1 {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

• EulerContinuousBoundedTensor.instContinuousBoundedTensor1 n = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor2 {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

• EulerContinuousBoundedTensor.instContinuousBoundedTensor2 n = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor3 {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

• EulerContinuousBoundedTensor.instContinuousBoundedTensor3 n = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor4 {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

• EulerContinuousBoundedTensor.instContinuousBoundedTensor4 n = inferInstance

noncomputable def EulerContinuousBoundedTensor.coordinates {E : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : (E [×n]→L[ℝ] V) →L[ℝ] (Fin n → Fin (Module.finrank ℝ E)) → V

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

Equations

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

noncomputable def EulerContinuousBoundedTensor.reassembly {E : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : ((Fin n → Fin (Module.finrank ℝ E)) → V) →L[ℝ] E [×n]→L[ℝ] V

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

Equations

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

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

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

Equations

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

noncomputable def EulerContinuousBoundedTensor.tensorPath {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) : C(K, BoundedContinuousFunction X (E [×n]→L[ℝ] V))

Tensor path, bundling toFun, continuous_toFun.

Equations

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

theorem EulerContinuousBoundedTensor.tensorPath_eq {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) (t : K) (x : X) : ((tensorPath n A) t) x = (BoundedContinuousFunction.evalCLM ℝ x).compContinuousMultilinearMap ((ContinuousMap.evalCLM ℝ t).compContinuousMultilinearMap A)

@[simp]

theorem EulerContinuousBoundedTensor.tensorPath_apply {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) (t : K) (x : X) (v : Fin n → E) : (((tensorPath n A) t) x) v = ((A v) t) x

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor5 {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup C(K, BoundedContinuousFunction X (E [×n]→L[ℝ] V))

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

Equations

• EulerContinuousBoundedTensor.instContinuousBoundedTensor5 n = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor6 {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ C(K, BoundedContinuousFunction X (E [×n]→L[ℝ] V))

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

Equations

• EulerContinuousBoundedTensor.instContinuousBoundedTensor6 n = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor7 {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V))

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

Equations

• EulerContinuousBoundedTensor.instContinuousBoundedTensor7 n = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousBoundedTensor.instContinuousBoundedTensor8 {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V))

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

Equations

• EulerContinuousBoundedTensor.instContinuousBoundedTensor8 n = inferInstance

theorem EulerContinuousBoundedTensor.tensorPath_norm_le {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) : ‖tensorPath n A‖ ≤ ‖A‖

noncomputable def EulerContinuousBoundedTensor.tensorPathLinear {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : (E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) →ₗ[ℝ] C(K, BoundedContinuousFunction X (E [×n]→L[ℝ] V))

Tensor path linear, bundling toFun, map_add, map_smul.

Equations

• EulerContinuousBoundedTensor.tensorPathLinear n = { toFun := EulerContinuousBoundedTensor.tensorPath n, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerContinuousBoundedTensor.tensorPathMap {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : (E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) →L[ℝ] C(K, BoundedContinuousFunction X (E [×n]→L[ℝ] V))

Tensor path map, bundling toLinearMap, cont.

Equations

• EulerContinuousBoundedTensor.tensorPathMap n = { toLinearMap := EulerContinuousBoundedTensor.tensorPathLinear n, cont := ⋯ }

@[simp]

theorem EulerContinuousBoundedTensor.tensorPathMap_apply {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) (A : E [×n]→L[ℝ] C(K, BoundedContinuousFunction X V)) (t : K) (x : X) (v : Fin n → E) : ((((tensorPathMap n) A) t) x) v = ((A v) t) x

theorem EulerContinuousBoundedTensor.tensorPathMap_norm_le {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (n : ℕ) : ‖tensorPathMap n‖ ≤ 1

theorem EulerContinuousBoundedTensor.tensorPath_iteratedFDeriv {K : Type u_1} {X : Type u_2} {E : Type u_3} {V : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (f : E → C(K, BoundedContinuousFunction X V)) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (a : E) (t : K) (x : X) : (((tensorPathMap n) (iteratedFDeriv ℝ n f a)) t) x = iteratedFDeriv ℝ n (fun (b : E) => ((f b) t) x) a

The actual finite packet fields supply bounded smooth cover coefficients. Their fixed-Hq word bounds give uniform tensor-jet bounds, with a single fixed coordinate radius conversion.

Actual smooth bounded real-cover coefficients obtained from a smooth mixed translation orbit in cylinder L². Every spatial tensor jet is a continuous path in the uniform norm. No integrability on the real cover is asserted or used.

@[instance_reducible]

noncomputable def EulerCylinderSmoothTimeField.instCylinderSmoothTimeField1 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSmoothTimeField.instCylinderSmoothTimeField1 n = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSmoothTimeField.instCylinderSmoothTimeField2 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSmoothTimeField.instCylinderSmoothTimeField2 n = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSmoothTimeField.instCylinderSmoothTimeField3 (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

• EulerCylinderSmoothTimeField.instCylinderSmoothTimeField3 n = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSmoothTimeField.instCylinderSmoothTimeField4 (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

• EulerCylinderSmoothTimeField.instCylinderSmoothTimeField4 n = inferInstance

noncomputable def EulerCylinderSmoothTimeField.coverJet (P : ℝ) [Fact (0 < P)] {K : Type} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) : C(K, BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space))

Cover jet, given by tensorPathMap n (iteratedFDeriv ℝ n (coverOrbit P p hp) 0).

Equations

• EulerCylinderSmoothTimeField.coverJet P p hp n = (EulerContinuousBoundedTensor.tensorPathMap n) (iteratedFDeriv ℝ n (EulerCylinderBoundedCover.coverOrbit P p hp) 0)

theorem EulerCylinderSmoothTimeField.coverJet_eq (P : ℝ) [Fact (0 < P)] {K : Type} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) (t : K) (x : EulerLiftedGradientSpace.LiftTangent) : ((coverJet P p hp n) t) x = iteratedFDeriv ℝ n (⇑((EulerCylinderBoundedCover.coverPath P p hp) t)) x

theorem EulerCylinderSmoothTimeField.coverPath_smooth (P : ℝ) [Fact (0 < P)] {K : Type} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : ContDiff ℝ ↑⊤ ⇑((EulerCylinderBoundedCover.coverPath P p hp) t)

noncomputable def EulerCylinderSmoothTimeField.ofPath (P : ℝ) [Fact (0 < P)] {K : Type} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : SmoothTimeField K EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

Of path, bundling field, smooth, jet, jet_eq.

Equations

• EulerCylinderSmoothTimeField.ofPath P p hp = { field := EulerCylinderBoundedCover.coverPath P p hp, smooth := ⋯, jet := EulerCylinderSmoothTimeField.coverJet P p hp, jet_eq := ⋯ }

@[simp]

theorem EulerCylinderSmoothTimeField.ofPath_apply (P : ℝ) [Fact (0 < P)] {K : Type} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) (x : EulerLiftedGradientSpace.LiftTangent) : ((ofPath P p hp).field t) x = EulerCylinderSmoothOrbit.pointField P p hp t (EulerLiftedGradientSpace.coveringMap P x)

theorem EulerCylinderSmoothTimeField.ofPath_jet_norm_le (P : ℝ) [Fact (0 < P)] {K : Type} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : K) (x : EulerLiftedGradientSpace.LiftTangent), ‖iteratedFDeriv ℝ n (fun (y : EulerLiftedGradientSpace.LiftTangent) => EulerCylinderSmoothOrbit.pointField P p hp t (EulerLiftedGradientSpace.coveringMap P y)) x‖ ≤ C) : ‖(ofPath P p hp).jet n‖ ≤ C

@[instance_reducible]

noncomputable def EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField1 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField1 n = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField2 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField2 n = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField3 (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

• EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField3 n = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField4 (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

• EulerPacketCylinderField.Field.instPacketFieldSmoothTimeField4 n = inferInstance

noncomputable def EulerPacketCylinderField.Field.toSmoothTimeField {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

To smooth time field, given by ofPath P G.path G.orbit.

Equations

• G.toSmoothTimeField = EulerCylinderSmoothTimeField.ofPath P G.path ⋯

theorem EulerPacketCylinderField.Field.toSmoothTimeField_apply {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (G.toSmoothTimeField.field t) x = raw (↑t, x)

theorem EulerPacketCylinderField.Field.toSmoothTimeField_timeDerivative {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) : SmoothTimeField.TimeDerivative T hT G.toSmoothTimeField H.toSmoothTimeField

theorem EulerPacketCylinderField.Field.toSmoothTimeField_map_jet {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (n : ℕ) : (G.map L).toSmoothTimeField.jet n = (SmoothTimeField.map L G.toSmoothTimeField).jet n

theorem EulerPacketCylinderField.Field.WordBound.toSmoothTimeField_jet_bound {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (hq : 3 ≤ q) (hR : 0 ≤ R) (hA : 0 ≤ A) (n : ℕ) : ‖G.toSmoothTimeField.jet n‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * R) ^ n * ↑n.factorial ^ 2

The constructed all-order correction and its true time derivative are actual smooth bounded cover coefficients. Their quantitative bounds come from the checked weighted Sobolev estimates.

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField1 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3)

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

Equations

• EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField1 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField2 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3)

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

Equations

• EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField2 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField3 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3))

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

Equations

• EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField3 n = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField4 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3))

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

Equations

• EulerAllOrderDriftCorrection.instCorrectionSmoothTimeField4 n = inferInstance

noncomputable def EulerAllOrderDriftCorrection.Budget.correctionCoefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.Vector3

Correction coefficient, given by (B.fieldTower P).toSmoothTimeField.

Equations

• EulerAllOrderDriftCorrection.Budget.correctionCoefficient P B = (EulerAllOrderDriftCorrection.Budget.fieldTower P B).toSmoothTimeField

noncomputable def EulerAllOrderDriftCorrection.Budget.correctionDerivativeCoefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.Vector3

Correction derivative coefficient, given by (B.timeDerivativeTower P).toSmoothTimeField.

Equations

• EulerAllOrderDriftCorrection.Budget.correctionDerivativeCoefficient P B = (EulerAllOrderDriftCorrection.Budget.timeDerivativeTower P B).toSmoothTimeField

theorem EulerAllOrderDriftCorrection.Budget.correctionCoefficient_timeDerivative (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) : SmoothTimeField.TimeDerivative T ⋯ (correctionCoefficient P B) (correctionDerivativeCoefficient P B)

theorem EulerAllOrderDriftCorrection.Budget.correctionCoefficient_jet_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (n : ℕ) : ‖(correctionCoefficient P B).jet n‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * correctionSize P B * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (reducedRadius P B)⁻¹) ^ n * ↑n.factorial ^ 2

theorem EulerAllOrderDriftCorrection.Budget.correctionDerivativeCoefficient_jet_bound (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm P 6 n (reducedRadius P B) (((timeDerivativeTower P B).realization (n + 6)) t) ≤ C) (n : ℕ) : ‖(correctionDerivativeCoefficient P B).jet n‖ ≤ EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * C * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (reducedRadius P B)⁻¹) ^ n * ↑n.factorial ^ 2

noncomputable def EulerAllOrderDriftCorrection.Budget.packetCoefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

Packet coefficient, given by G.toSmoothTimeField.add (B.correctionCoefficient P).

Equations

• EulerAllOrderDriftCorrection.Budget.packetCoefficient P B G = G.toSmoothTimeField.add (EulerAllOrderDriftCorrection.Budget.correctionCoefficient P B)

noncomputable def EulerAllOrderDriftCorrection.Budget.packetDerivativeCoefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerSmoothLimit.Space

Packet derivative coefficient, given by H.toSmoothTimeField.add (B.correctionDerivativeCoefficient P).

Equations

• EulerAllOrderDriftCorrection.Budget.packetDerivativeCoefficient P B H = H.toSmoothTimeField.add (EulerAllOrderDriftCorrection.Budget.correctionDerivativeCoefficient P B)

noncomputable def EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

Lifted packet coefficient, given by lift (B.packetCoefficient P G) A.κ A.direction.

Equations

• EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B G = EulerLiftedSmoothTimeField.lift (EulerAllOrderDriftCorrection.Budget.packetCoefficient P B G) A.κ A.direction

noncomputable def EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw_t : EulerPacketProfileRecursion.VectorField} (H : EulerPacketCylinderField.Field P T raw_t) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

Lifted packet derivative coefficient, given by lift (B.packetDerivativeCoefficient P H) A.κ A.direction.

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.packetCoefficient_eq_corrected (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hG : A.approximation = G.toFieldTower) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : ((packetCoefficient P B G).field t) x = (correctedFieldTower P B).pointField t (EulerLiftedGradientSpace.coveringMap P x)

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_eq_corrected (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hG : A.approximation = G.toFieldTower) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : ((liftedPacketCoefficient P B G).field t) x = EulerMetricTransport.transportDirection A.κ A.direction ((correctedFieldTower P B).pointField t (EulerLiftedGradientSpace.coveringMap P x))

theorem EulerAllOrderDriftCorrection.Budget.packetCoefficient_timeDerivative (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (H : EulerPacketCylinderField.Field P T raw_t) (h : EulerPacketCylinderField.TimeDerivative ⋯ G H) : SmoothTimeField.TimeDerivative T ⋯ (packetCoefficient P B G) (packetDerivativeCoefficient P B H)

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_timeDerivative (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (H : EulerPacketCylinderField.Field P T raw_t) (h : EulerPacketCylinderField.TimeDerivative ⋯ G H) : SmoothTimeField.TimeDerivative T ⋯ (liftedPacketCoefficient P B G) (liftedPacketDerivativeCoefficient P B H)

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_periodic (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : ((liftedPacketCoefficient P B G).field t) (x.1, ↑c + x.2) = ((liftedPacketCoefficient P B G).field t) x

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_trace (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hG : A.approximation = G.toFieldTower) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent) : (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑((liftedPacketCoefficient P B G).field t)) x) = 0