Fixed bounded maps preserve the actual fixed-Sobolev external word sums.

theorem EulerParameterWordGevrey.baseSize_comp_clm_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] (directions : ι → P) (q : ℕ) (L : E →L[ℝ] F) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (x : P) : baseSize directions q (⇑L ∘ f) x ≤ ‖L‖ * baseSize directions q f x

theorem EulerParameterWordGevrey.block_comp_clm_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] (directions : ι → P) (q : ℕ) (L : E →L[ℝ] F) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : block directions q (⇑L ∘ f) n x ≤ ‖L‖ * block directions q f n x

The exact same external radius and fixed Sobolev order pass through every fixed continuous linear map, with just its operator norm.

theorem EulerParameterWordGevrey.coefficientBlock_comp_clm_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] (directions : ι → P) (q : ℕ) (L : E →L[ℝ] F) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : coefficientBlock directions q (⇑L ∘ f) n x ≤ ‖L‖ * coefficientBlock directions q f n x

theorem EulerParameterWordGevrey.block_sub_le {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (x : P) : block directions q (f - g) n x ≤ block directions q f n x + block directions q g n x