The actual forcing in the projected acceleration equation

Both the mean and transverse strong equations use Q* (f - 2 Q₁ v). This module gives its genuine parameter regularity and factorial estimate, with the explicit amplitude needed by the actual Gram inverse.

noncomputable def EulerTimeLpAccelerationForcing.forcing {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 : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (f : P → ↥(EulerTimeLp.TimeLp T E)) (v : P → ↥(EulerTimeLp.TimeLp T U)) (x : P) : ↥(EulerTimeLp.TimeLp T U)

The literal right side of the projected strong acceleration equation.

Equations

• EulerTimeLpAccelerationForcing.forcing T hT Q Q₁ f v x = (ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT (Q x))) (f x - 2 • (EulerTimeLp.timeMultiplier T hT (Q₁ x)) (v x))

theorem EulerTimeLpAccelerationForcing.forcing_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 : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (f : P → ↥(EulerTimeLp.TimeLp T E)) (v : P → ↥(EulerTimeLp.TimeLp T U)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hf : ContDiff ℝ n f) (hv : ContDiff ℝ n v) : ContDiff ℝ n (forcing T hT Q Q₁ f v)

The actual strong forcing is smoothly parameterized whenever its inputs are.

theorem EulerTimeLpAccelerationForcing.forcing_bound {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 : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (f : P → ↥(EulerTimeLp.TimeLp T E)) (v : P → ↥(EulerTimeLp.TimeLp T 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 T hT Q Q₁ f v) x‖ ≤ 3 * C₀ * (F + 6 * C₁ * V) * EulerGevrey.majorant R d n

One fixed polynomial amplitude controls all genuine forcing derivatives.