Same-radius operations on literal fixed-base ordered derivative blocks.

theorem EulerParameterWordGevrey.block_smul_le {P : Type u_1} {E : Type u_2} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (a : ℝ) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : block directions q (fun (y : P) => a • f y) n x ≤ |a| * block directions q f n x

theorem EulerParameterWordGevrey.block_smul_gevrey {P : Type u_1} {E : Type u_2} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (a : ℝ) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (R C : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), block directions q f n x ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : block directions q (fun (y : P) => a • f y) n x ≤ |a| * C * EulerGevrey.majorant R d n

theorem EulerParameterWordGevrey.block_sub_gevrey {P : Type u_1} {E : Type u_2} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (R C D : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), block directions q f n x ≤ C * EulerGevrey.majorant R d n) (hc : ∀ (n : ℕ) (x : P), block directions q g n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : block directions q (f - g) n x ≤ (C + D) * EulerGevrey.majorant R d n

theorem EulerParameterWordGevrey.block_acceleration_forcing_gevrey {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [Fintype ι] (directions : ι → P) (q : ℕ) (A : P → E →L[ℝ] F) (B : P → G →L[ℝ] E) (f : P → E) (v : P → G) (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (hf : ContDiff ℝ (↑⊤) f) (hv : ContDiff ℝ (↑⊤) v) (Rc R CA CB Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : Rc ≤ R) (hCA : 0 ≤ CA) (hCB : 0 ≤ CB) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hbA : ∀ (n : ℕ) (x : P), coefficientBlock directions q A n x ≤ CA * EulerGevrey.majorant Rc 0 n) (hbB : ∀ (n : ℕ) (x : P), coefficientBlock directions q B n x ≤ CB * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), block directions q v n x ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : block directions q (fun (y : P) => (A y) (f y - 2 • (B y) (v y))) n x ≤ 3 * CA * (Cf + 6 * CB * Cv) * EulerGevrey.majorant R d n

The acceleration right side has the same fixed base order and external radius as its given velocity and forcing. Only coefficient blocks enter its explicit amplitude.