Actual spatial orbits of continuous mean acceleration

The ordinary solenoidal Gram inverse commutes with simultaneous translation of its data. This identifies the parameterized continuous solve with the genuine spatial orbit of the acceleration, including endpoint times.

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration7 (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

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration8 (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

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration8 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration9 (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

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration9 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousAcceleration.instMeanContinuousAcceleration10 (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

• EulerMeanContinuousAcceleration.instMeanContinuousAcceleration10 T = inferInstance

noncomputable def EulerMeanContinuousAcceleration.meanAccelerationPath (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 : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) (f : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)

The continuous mean acceleration constructed at each actual time.

Equations

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

theorem EulerMeanContinuousAcceleration.meanAccelerationPath_orbit_eq (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 : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) (f : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) : (fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) (meanAccelerationPath T F F₁ c hc hLower v f)) = fun (a : EulerSmoothLimit.Space) => EulerContinuousGramAcceleration.accelerationPath T (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F)) (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F₁)) c hc ⋯ ((EulerMeanCoordinatePath.coordinatePathTranslation T a) v) ((EulerMeanTimeContinuousTranslation.pathTranslation T a) f)

The genuine spatial orbit equals the actual solve with translated data.

theorem EulerMeanContinuousAcceleration.meanAccelerationPath_translation_contDiff (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 : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) (f : C(↑(Set.Icc 0 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) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) v) (hf : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) f) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) (meanAccelerationPath T F F₁ c hc hLower v f)

Smooth coefficient and data orbits give the actual continuous acceleration orbit.

theorem EulerMeanContinuousAcceleration.meanAccelerationPath_translation_gevrey (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 : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) (f : C(↑(Set.Icc 0 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) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) v) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation 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) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) f) a‖ ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) v) a‖ ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) (meanAccelerationPath T F F₁ c hc hLower v f)) a‖ ≤ EulerGevrey.majorant R (d + 1) n

All actual spatial acceleration derivatives have a uniform-time bound with one factorial shift and an explicit polynomial radius condition.