Actual forcing derivatives in the uniform time norm

Continuous paths of the literal ordinary spatial L² jets give genuine smoothness of the forcing translation orbit in C(time,L²). The derivative norm is bounded by the original uniform-time spatial jet norm, with no loss.

Actual spatial derivatives in the uniform norm on continuous paths

A family of continuous paths whose pointwise spatial derivatives are actual continuous paths, with uniform bounds, is smooth in the uniform path norm. The proof uses a quadratic Taylor remainder and loses no derivative-bound constant. No uniform-path differentiability is assumed.

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily1 {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily1 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily2 {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily2 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily3 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] : NormedAddCommGroup C(K, V)

Cache the standard NormedAddCommGroup C(K,V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily3 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily4 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ C(K, V)

Cache the standard NormedSpace ℝ C(K,V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily4 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily5 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup C(K, EulerSmoothLimit.Space →L[ℝ] V)

Cache the standard NormedAddCommGroup C(K,Space →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily5 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily6 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ C(K, EulerSmoothLimit.Space →L[ℝ] V)

Cache the standard NormedSpace ℝ C(K,Space →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily6 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily7 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] C(K, V))

Cache the standard NormedAddCommGroup (Space →L[ℝ] C(K,V)) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily7 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.instContinuousSpatialFamily8 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] C(K, V))

Cache the standard NormedSpace ℝ (Space →L[ℝ] C(K,V)) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.instContinuousSpatialFamily8 = inferInstance

noncomputable def EulerContinuousSpatialFamily.direction {K : Type u} [TopologicalSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : C(K, EulerSmoothLimit.Space →L[ℝ] V)) (a : EulerSmoothLimit.Space) : C(K, V)

Direction, given by ⟨fun t => D t a, D.continuous.clm_apply continuous_const⟩.

Equations

• EulerContinuousSpatialFamily.direction D a = { toFun := fun (t : K) => (D t) a, continuous_toFun := ⋯ }

theorem EulerContinuousSpatialFamily.direction_norm_le {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : C(K, EulerSmoothLimit.Space →L[ℝ] V)) (a : EulerSmoothLimit.Space) : ‖direction D a‖ ≤ ‖D‖ * ‖a‖

noncomputable def EulerContinuousSpatialFamily.derivativeLinear {K : Type u} [TopologicalSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : C(K, EulerSmoothLimit.Space →L[ℝ] V)) : EulerSmoothLimit.Space →ₗ[ℝ] C(K, V)

Derivative linear, bundling toFun, map_add, map_smul.

Equations

• EulerContinuousSpatialFamily.derivativeLinear D = { toFun := EulerContinuousSpatialFamily.direction D, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerContinuousSpatialFamily.derivativeMap {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : C(K, EulerSmoothLimit.Space →L[ℝ] V)) : EulerSmoothLimit.Space →L[ℝ] C(K, V)

Derivative map, bundling toLinearMap, cont.

Equations

• EulerContinuousSpatialFamily.derivativeMap D = { toLinearMap := EulerContinuousSpatialFamily.derivativeLinear D, cont := ⋯ }

@[simp]

theorem EulerContinuousSpatialFamily.derivativeMap_apply {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : C(K, EulerSmoothLimit.Space →L[ℝ] V)) (a : EulerSmoothLimit.Space) (t : K) : ((derivativeMap D) a) t = (D t) a

theorem EulerContinuousSpatialFamily.derivativeMap_norm_le {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : C(K, EulerSmoothLimit.Space →L[ℝ] V)) : ‖derivativeMap D‖ ≤ ‖D‖

noncomputable def EulerContinuousSpatialFamily.derivativeBundlingLinear {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : C(K, EulerSmoothLimit.Space →L[ℝ] V) →ₗ[ℝ] EulerSmoothLimit.Space →L[ℝ] C(K, V)

Derivative bundling linear, bundling toFun, map_add, map_smul.

Equations

• EulerContinuousSpatialFamily.derivativeBundlingLinear = { toFun := EulerContinuousSpatialFamily.derivativeMap, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerContinuousSpatialFamily.derivativeBundling {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : C(K, EulerSmoothLimit.Space →L[ℝ] V) →L[ℝ] EulerSmoothLimit.Space →L[ℝ] C(K, V)

Derivative bundling, bundling toLinearMap, cont.

Equations

• EulerContinuousSpatialFamily.derivativeBundling = { toLinearMap := EulerContinuousSpatialFamily.derivativeBundlingLinear, cont := ⋯ }

theorem EulerContinuousSpatialFamily.derivativeBundling_norm_le_one {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : ‖derivativeBundling‖ ≤ 1

structure EulerContinuousSpatialFamily.SpatialFamily (K : Type u) [TopologicalSpace K] [CompactSpace K] (V : Type v) [NormedAddCommGroup V] [NormedSpace ℝ V] : Type (max u v)

Actual continuous spatial derivative paths and finite uniform bounds. The jet_eq field identifies every supplied jet with the ordinary derivative.

• field : EulerSmoothLimit.Space → C(K, V)

  Underlying field of SpatialFamily, of type Space → C(K,V).

• smooth (t : K) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (self.field a) t
• jet (n : ℕ) : EulerSmoothLimit.Space → C(K, EulerSmoothLimit.Space [×n]→L[ℝ] V)

  Jet of SpatialFamily, of type (n : ℕ) → Space → C(K,Space [×n]→L[ℝ] V).

• jet_eq (n : ℕ) (a : EulerSmoothLimit.Space) (t : K) : (self.jet n a) t = iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (self.field b) t) a
• bound : ℕ → ℝ

  Bound of SpatialFamily, of type ℕ → ℝ.

• bound_nonneg (n : ℕ) : 0 ≤ self.bound n
• bounded (n : ℕ) (a : EulerSmoothLimit.Space) (t : K) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (self.field b) t) a‖ ≤ self.bound n

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily9 {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily9 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily10 {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] V)

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

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily10 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily11 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] : NormedAddCommGroup C(K, V)

Cache the standard NormedAddCommGroup C(K,V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily11 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily12 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ C(K, V)

Cache the standard NormedSpace ℝ C(K,V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily12 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily13 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup C(K, EulerSmoothLimit.Space →L[ℝ] V)

Cache the standard NormedAddCommGroup C(K,Space →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily13 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily14 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ C(K, EulerSmoothLimit.Space →L[ℝ] V)

Cache the standard NormedSpace ℝ C(K,Space →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily14 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily15 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] C(K, V))

Cache the standard NormedAddCommGroup (Space →L[ℝ] C(K,V)) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily15 = inferInstance

@[instance_reducible]

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily16 {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] C(K, V))

Cache the standard NormedSpace ℝ (Space →L[ℝ] C(K,V)) instance to shorten typeclass synthesis.

Equations

• EulerContinuousSpatialFamily.SpatialFamily.instContinuousSpatialFamily16 = inferInstance

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.derivativeField {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (a : EulerSmoothLimit.Space) : C(K, EulerSmoothLimit.Space →L[ℝ] V)

Derivative field, given by (continuousMultilinearCurryFin1 ℝ Space V).toContinuousLinearEquiv.toContinuousLinearMap.compLeftContinuous ℝ K (A.jet 1 a).

Equations

• A.derivativeField a = (ContinuousLinearMap.compLeftContinuous ℝ K ↑↑(continuousMultilinearCurryFin1 ℝ EulerSmoothLimit.Space V)) (A.jet 1 a)

theorem EulerContinuousSpatialFamily.SpatialFamily.derivativeField_eq {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (a : EulerSmoothLimit.Space) (t : K) : (A.derivativeField a) t = fderiv ℝ (fun (b : EulerSmoothLimit.Space) => (A.field b) t) a

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.derivativeJet {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (n : ℕ) (a : EulerSmoothLimit.Space) : C(K, EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space →L[ℝ] V)

Derivative jet as an element of C(K,Space [×n]→L[ℝ] (Space →L[ℝ] V)).

Equations

• A.derivativeJet n a = (ContinuousLinearMap.compLeftContinuous ℝ K ↑↑(continuousMultilinearCurryRightEquiv' ℝ n EulerSmoothLimit.Space V)) (A.jet (n + 1) a)

theorem EulerContinuousSpatialFamily.SpatialFamily.derivativeJet_eq {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (n : ℕ) (a : EulerSmoothLimit.Space) (t : K) : (A.derivativeJet n a) t = iteratedFDeriv ℝ n (fderiv ℝ fun (b : EulerSmoothLimit.Space) => (A.field b) t) a

noncomputable def EulerContinuousSpatialFamily.SpatialFamily.derivative {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) : SpatialFamily K (EulerSmoothLimit.Space →L[ℝ] V)

Derivative, bundling field, smooth, have, funext and the required compatibility proofs.

Equations

• A.derivative = { field := A.derivativeField, smooth := ⋯, jet := A.derivativeJet, jet_eq := ⋯, bound := fun (n : ℕ) => A.bound (n + 1), bound_nonneg := ⋯, bounded := ⋯ }

@[simp]

theorem EulerContinuousSpatialFamily.SpatialFamily.derivative_bound {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (n : ℕ) : A.derivative.bound n = A.bound (n + 1)

theorem EulerContinuousSpatialFamily.SpatialFamily.taylor_bound {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (a b : EulerSmoothLimit.Space) : ‖A.field b - A.field a - (derivativeMap (A.derivative.field a)) (b - a)‖ ≤ A.bound 2 * ‖b - a‖ ^ 2

theorem EulerContinuousSpatialFamily.SpatialFamily.hasFDerivAt_field {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (a : EulerSmoothLimit.Space) : HasFDerivAt A.field (derivativeMap (A.derivative.field a)) a

Genuine differentiability in the uniform path norm, from the pointwise Taylor estimate.

theorem EulerContinuousSpatialFamily.SpatialFamily.fderiv_field {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) : fderiv ℝ A.field = fun (a : EulerSmoothLimit.Space) => derivativeBundling (A.derivative.field a)

theorem EulerContinuousSpatialFamily.SpatialFamily.contDiff_field {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) : ContDiff ℝ (↑⊤) A.field

All ordinary pointwise derivatives produce genuine uniform-path smoothness.

theorem EulerContinuousSpatialFamily.SpatialFamily.norm_iteratedFDeriv_field_le {K : Type u} [TopologicalSpace K] [CompactSpace K] {V : Type v} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SpatialFamily K V) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n A.field a‖ ≤ A.bound n

The original pointwise uniform derivative bound holds without any additional factor.

noncomputable def EulerContinuousForcing.translate {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerSmoothLimit.Space) (f : C(K, ↥(EulerLpTranslation.L2Space V))) : C(K, ↥(EulerLpTranslation.L2Space V))

Ordinary translation applied to every value of an actual continuous L² path.

Equations

• EulerContinuousForcing.translate a f = (ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpTranslation.translation a).toContinuousLinearMap) f

@[simp]

theorem EulerContinuousForcing.translate_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : EulerSmoothLimit.Space) (f : C(K, ↥(EulerLpTranslation.L2Space V))) (t : K) : (translate a f) t = (EulerLpTranslation.translation a) (f t)

noncomputable def EulerContinuousForcing.spatialJetPath {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) : C(K, ↥(EulerLpTranslation.L2Space (EulerSmoothLimit.Space [×n]→L[ℝ] V)))

The original ordinary spatial jet, as a genuine continuous L² path.

Equations

• EulerContinuousForcing.spatialJetPath A hA n = { toFun := fun (t : K) => (A t).jetLp n, continuous_toFun := ⋯ }

noncomputable def EulerContinuousForcing.orbitJetPath {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (n : ℕ) (a : EulerSmoothLimit.Space) : C(K, EulerSmoothLimit.Space [×n]→L[ℝ] ↥(EulerLpTranslation.L2Space V))

The actual translation jets form a continuous path because they are bounded linear images of the original ordinary L² spatial jets.

Equations

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

theorem EulerContinuousForcing.orbitJetPath_eq {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (f : C(K, ↥(EulerLpTranslation.L2Space V))) (hf : ∀ (t : K), f t = (A t).toLp) (n : ℕ) (a : EulerSmoothLimit.Space) (t : K) : (orbitJetPath A hA n a) t = iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (translate b f) t) a

noncomputable def EulerContinuousForcing.forcingFamily {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (f : C(K, ↥(EulerLpTranslation.L2Space V))) (hf : ∀ (t : K), f t = (A t).toLp) : EulerContinuousSpatialFamily.SpatialFamily K ↥(EulerLpTranslation.L2Space V)

This package contains only actual pointwise spatial derivatives and their original uniform-time L² bounds.

Equations

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

theorem EulerContinuousForcing.forcing_translation_contDiff {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (f : C(K, ↥(EulerLpTranslation.L2Space V))) (hf : ∀ (t : K), f t = (A t).toLp) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => translate a f

Literal smooth forcing slices with continuous spatial L² jets have a genuinely smooth translation orbit in the uniform time norm.

theorem EulerContinuousForcing.forcing_translation_jet_bound {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : K → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (f : C(K, ↥(EulerLpTranslation.L2Space V))) (hf : ∀ (t : K), f t = (A t).toLp) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => translate b f) a‖ ≤ ‖spatialJetPath A hA n‖

Every actual orbit derivative is controlled by the original uniform-time ordinary L² spatial derivative with constant one.