Actual ordered parameter derivatives and their factorial word sums

The parameter estimates are stated for the genuine iterated Fréchet derivative. Evaluation on an ordered family of directions gives the mixed word derivative. Summing all words changes the radius by one fixed alphabet factor, independent of the derivative order and factorial shift.

noncomputable def EulerParameterWordGevrey.wordDerivative {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f : P → E) {n : ℕ} (w : Fin n → ι) (x : P) : E

The actual mixed differential evaluated on an ordered word of directions.

Equations

• EulerParameterWordGevrey.wordDerivative directions f w x = (iteratedFDeriv ℝ n f x) fun (j : Fin n) => directions (w j)

noncomputable def EulerParameterWordGevrey.wordSum {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (f : P → E) (n : ℕ) (x : P) : ℝ

The sum of the actual norms over all ordered words.

Equations

• EulerParameterWordGevrey.wordSum directions f n x = ∑ w : Fin n → ι, ‖EulerParameterWordGevrey.wordDerivative directions f w x‖

theorem EulerParameterWordGevrey.wordDerivative_norm {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (f : P → E) {n : ℕ} (w : Fin n → ι) (x : P) : ‖wordDerivative directions f w x‖ ≤ ‖iteratedFDeriv ℝ n f x‖

Unit directions do not enlarge the norm of the actual differential.

theorem EulerParameterWordGevrey.wordSum_le {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (f : P → E) (n : ℕ) (x : P) : wordSum directions f n x ≤ ↑(Fintype.card ι) ^ n * ‖iteratedFDeriv ℝ n f x‖

Summing the actual word norms costs precisely the number of words.

theorem EulerParameterWordGevrey.wordSum_gevrey {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (f : P → E) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : wordSum directions f n x ≤ C * EulerGevrey.majorant (max 1 ↑(Fintype.card ι) * R) d n

The actual word sum has a factorial bound with one dimension-dependent radius enlargement.