Related estimates used together by the same construction modules.

Actual projected acceleration in the same fixed Sobolev word blocks.

theorem EulerTimeLpAccelerationSobolev.forcing_block_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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) (Rc R C₀ C₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q v n x ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (EulerTimeLpAccelerationForcing.forcing T hT Q Q₁ f v) n x ≤ EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf Cv * EulerGevrey.majorant R d n

The actual acceleration forcing retains the forcing/velocity grade and radius.

theorem EulerTimeLpAccelerationSobolev.solution_block_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (w : U), c * ‖w‖ ^ 2 ≤ ‖((Q x) t) w‖ ^ 2) (f : P → ↥(EulerTimeLp.TimeLp T E)) (v : P → ↥(EulerTimeLp.TimeLp T U)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (Rc R C₀ C₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hR : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf Cv) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q v n x ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (fun (y : P) => (EulerTimeLpGramInverse.gramSolver T hT (Q y) c hc ⋯) (EulerTimeLpAccelerationForcing.forcing T hT Q Q₁ f v y)) n x ≤ EulerGevrey.majorant R (d + 1) n

The genuine Gram solution adds one shift, with no change of radius or fixed Sobolev order and no assumption about solution derivatives.

Actual uniform-time acceleration in fixed Sobolev word blocks

The genuine continuous Gram solve incurs one factorial shift at the original radius. Time endpoint values are included in the continuous-path norm.

theorem EulerContinuousAccelerationSobolev.forcing_block_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (f : P → C(↑(Set.Icc 0 T), E)) (v : P → C(↑(Set.Icc 0 T), U)) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (Rc R C₀ C₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q v n x ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (EulerContinuousAccelerationForcing.forcing Q Q₁ f v) n x ≤ EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf Cv * EulerGevrey.majorant R d n

theorem EulerContinuousAccelerationSobolev.acceleration_block_bound {P : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (w : U), c * ‖w‖ ^ 2 ≤ ‖((Q x) t) w‖ ^ 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) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hR : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf Cv) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q v n x ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (fun (y : P) => EulerContinuousGramAcceleration.accelerationPath T (Q y) (Q₁ y) c hc ⋯ (v y) (f y)) n x ≤ EulerGevrey.majorant R (d + 1) n

The actual acceleration path has one more grade in the same fixed Sobolev order; there is no additional conversion of external words.