Finite sums preserve genuine fixed-Sobolev external-word estimates.

theorem EulerParameterWordGevrey.block_finset_sum_le {P : Type u_1} {E : Type u_2} {ι : Type u_3} {κ : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (s : Finset κ) (f : κ → P → E) (hf : ∀ k ∈ s, ContDiff ℝ (↑⊤) (f k)) (n : ℕ) (x : P) : block directions q (∑ k ∈ s, f k) n x ≤ ∑ k ∈ s, block directions q (f k) n x