Spatial translations of continuous ordinary-L² time paths

The actual H¹ reconstruction commutes with spatial translation. Therefore regularity and bounds for its two Bochner fields imply uniform-in-time spatial orbit regularity, and evaluation at each time loses no derivative or additional constant.

@[instance_reducible]

noncomputable def EulerMeanTimeContinuousTranslation.instMeanTimeContinuousTranslation1 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanTimeContinuousTranslation.instMeanTimeContinuousTranslation1 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTimeContinuousTranslation.instMeanTimeContinuousTranslation2 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanTimeContinuousTranslation.instMeanTimeContinuousTranslation2 T = inferInstance

noncomputable def EulerMeanTimeContinuousTranslation.pathTranslation (T : ℝ) (a : EulerSmoothLimit.Space) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2) →L[ℝ] C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Ordinary spatial translation of every time value of a continuous L² path.

Equations

• EulerMeanTimeContinuousTranslation.pathTranslation T a = ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerMeanSolenoidal.translation a).toContinuousLinearMap

@[simp]

theorem EulerMeanTimeContinuousTranslation.pathTranslation_apply (T : ℝ) (a : EulerSmoothLimit.Space) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (t : ↑(Set.Icc 0 T)) : ((pathTranslation T a) p) t = (EulerMeanSolenoidal.translation a) (p t)

theorem EulerMeanTimeContinuousTranslation.pathTranslation_reconstruction (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (p q : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (pathTranslation T a) ((EulerTimeH1Reconstruction.reconstruction T hT) (p, q)) = (EulerTimeH1Reconstruction.reconstruction T hT) ((EulerMeanTimeTranslation.timeTranslation T a) p, (EulerMeanTimeTranslation.timeTranslation T a) q)

Translation of the actual continuous reconstruction equals reconstruction of the translated value and derivative fields.

theorem EulerMeanTimeContinuousTranslation.reconstruction_translation_contDiff (T : ℝ) (hT : 0 ≤ T) (p q : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hp : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) p) (hq : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) q) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (pathTranslation T a) ((EulerTimeH1Reconstruction.reconstruction T hT) (p, q))

Uniform-in-time spatial regularity follows from the actual two-field H¹ data.

theorem EulerMeanTimeContinuousTranslation.reconstruction_translation_gevrey (T : ℝ) (hT : 0 < T) (p q : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) q) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (d : ℕ) (hbp : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) p) a‖ ≤ C * EulerGevrey.majorant R d n) (hbq : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) q) a‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (pathTranslation T b) ((EulerTimeH1Reconstruction.reconstruction T ⋯) (p, q))) a‖ ≤ (T⁻¹ * √T * C + 2 * √T * D) * EulerGevrey.majorant R d n

The true uniform-time norm of every spatial orbit derivative has only the proved H¹ trace cost.

theorem EulerMeanTimeContinuousTranslation.evaluation_norm_le (T : ℝ) (t : ↑(Set.Icc 0 T)) : ‖ContinuousMap.evalCLM ℝ t‖ ≤ 1

Time evaluation is a norm contraction on continuous ordinary-L² paths.

theorem EulerMeanTimeContinuousTranslation.pathTranslation_evaluation_contDiff (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hp : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (p t)

Every actual time value has a smooth ordinary spatial translation orbit.

theorem EulerMeanTimeContinuousTranslation.pathTranslation_evaluation_gevrey (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (pathTranslation T a) p) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (pathTranslation T b) p) a‖ ≤ C * EulerGevrey.majorant R d n) (t : ↑(Set.Icc 0 T)) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation b) (p t)) a‖ ≤ C * EulerGevrey.majorant R d n

Time evaluation preserves every uniform spatial factorial bound without loss.