Actual continuous-time acceleration forcing

The expression Q*(f-2 Q₁v) is a genuine continuous path. Its smoothness and factorial bound are proved in the uniform time norm and are shared by the mean and transverse strong equations.

noncomputable def EulerContinuousAccelerationForcing.forcing {K : Type u_1} {P : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : P → C(K, U →L[ℝ] E)) (f : P → C(K, E)) (v : P → C(K, U)) (x : P) : C(K, U)

The literal continuous forcing in the projected acceleration equation.

Equations

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

theorem EulerContinuousAccelerationForcing.forcing_contDiff {K : Type u_1} {P : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : P → C(K, U →L[ℝ] E)) (f : P → C(K, E)) (v : P → C(K, U)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hf : ContDiff ℝ n f) (hv : ContDiff ℝ n v) : ContDiff ℝ n (forcing Q Q₁ f v)

Actual uniform-time regularity of the acceleration forcing.

theorem EulerContinuousAccelerationForcing.forcing_bound {K : Type u_1} {P : Type u_2} {U : Type u_3} {E : Type u_4} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : P → C(K, U →L[ℝ] E)) (f : P → C(K, E)) (v : P → C(K, U)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (R C₀ C₁ F V : ℝ) (hR : 0 ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hF : 0 ≤ F) (hV : 0 ≤ V) (d : ℕ) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant R 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ F * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n v x‖ ≤ V * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (forcing Q Q₁ f v) x‖ ≤ 3 * C₀ * (F + 6 * C₁ * V) * EulerGevrey.majorant R d n

One fixed amplitude controls the genuine derivatives at every order.