Smoothness and exact concatenation of genuine directional word derivatives.

theorem EulerParameterWordGevrey.wordDerivative_contDiff {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) : ContDiff ℝ (↑⊤) (wordDerivative directions f w)

theorem EulerParameterWordGevrey.sum_words_snoc {ι : Type u_3} [Fintype ι] (n : ℕ) (a : (Fin (n + 1) → ι) → ℝ) : ∑ w : Fin (n + 1) → ι, a w = ∑ i : ι, ∑ w : Fin n → ι, a (Fin.snoc w i)

The sum over all words can be decomposed for any scalar expression on words.