Genuine spatial estimates for mean acceleration

The coordinate acceleration is recovered through the actual coercive Gram inverse. Covariance identifies its parameterized solve with spatial translation of the original field. Consequently the estimates below concern the real spatial orbit, with no assumed derivatives of the inverse.

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey8 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey9 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey9 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationGevrey.instMeanAccelerationGevrey10 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanAccelerationGevrey.instMeanAccelerationGevrey10 T = inferInstance

theorem EulerMeanAccelerationGevrey.meanAcceleration_orbit_eq (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) (EulerMeanGramTranslation.meanAcceleration T hT F F₁ c hc hLower v f)) = fun (a : EulerSmoothLimit.Space) => (EulerTimeLpGramInverse.gramSolver T hT (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F)) c hc ⋯) (EulerTimeLpAccelerationForcing.forcing T hT (fun (b : EulerSmoothLimit.Space) => EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T b F)) (fun (b : EulerSmoothLimit.Space) => EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T b F₁)) (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) v) a)

The actual acceleration orbit is the actual translated Gram solve.

theorem EulerMeanAccelerationGevrey.meanAcceleration_translation_contDiff (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) (hf : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) (EulerMeanGramTranslation.meanAcceleration T hT F F₁ c hc hLower v f)

Actual spatial smoothness passes from the solved coordinate velocity to the acceleration through the proved Gram inverse.

theorem EulerMeanAccelerationGevrey.meanAcceleration_translation_gevrey (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R CF CF₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hR : 0 ≤ R) (hRcR : Rc ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hstrong : 2 * EulerTimeLpGramGevrey.gramCost c CF (3 * CF * (Cf + 6 * CF₁ * Cv)) * (Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) a‖ ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) v) a‖ ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) (EulerMeanGramTranslation.meanAcceleration T hT F F₁ c hc hLower v f)) a‖ ≤ EulerGevrey.majorant R (d + 1) n

The genuine acceleration gains one factorial shift relative to its velocity and forcing inputs, with an explicit polynomial radius condition.