Uniform-time regularity of actual acceleration

The continuous acceleration is the already constructed Gram inverse applied to its literal forcing. Smoothness and factorial estimates therefore apply to the actual continuous path, including its endpoint values.

theorem EulerContinuousAccelerationGevrey.acceleration_eq_solve {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (v : P → C(↑(Set.Icc 0 T), U)) (f : P → C(↑(Set.Icc 0 T), E)) : (fun (x : P) => EulerContinuousGramAcceleration.accelerationPath T (Q x) (Q₁ x) c hc ⋯ (v x) (f x)) = fun (x : P) => (EulerContinuousGramPath.solve T (Q x) c hc ⋯) (EulerContinuousAccelerationForcing.forcing Q Q₁ f v x)

The continuous acceleration is the genuine continuous Gram solve.

theorem EulerContinuousAccelerationGevrey.acceleration_contDiff {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (v : P → C(↑(Set.Icc 0 T), U)) (f : P → C(↑(Set.Icc 0 T), E)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hv : ContDiff ℝ n v) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => EulerContinuousGramAcceleration.accelerationPath T (Q x) (Q₁ x) c hc ⋯ (v x) (f x)

Actual uniform-time acceleration depends smoothly on the actual coefficients and data.

theorem EulerContinuousAccelerationGevrey.acceleration_gevrey {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (v : P → C(↑(Set.Icc 0 T), U)) (f : P → C(↑(Set.Icc 0 T), E)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hv : ContDiff ℝ (↑⊤) v) (hf : ContDiff ℝ (↑⊤) f) (Rc R C₀ C₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hR : 0 ≤ R) (hRcR : Rc ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hstrong : 2 * EulerTimeLpGramGevrey.gramCost c C₀ (3 * C₀ * (Cf + 6 * C₁ * Cv)) * (Rc + 1) ≤ R) (hQb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hQ₁b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n v x‖ ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerContinuousGramAcceleration.accelerationPath T (Q y) (Q₁ y) c hc ⋯ (v y) (f y)) x‖ ≤ EulerGevrey.majorant R (d + 1) n

The actual continuous acceleration has one factorial shift relative to its velocity and forcing data, with a polynomial radius condition.