Actual directional word calculus without changing radius

The word derivative and word sum are the existing ordered evaluations of the genuine iterated Fréchet derivative. Fixed bounded maps commute with every word and act boundedly on the same sum, without a dimension factor.

noncomputable def EulerParameterWordGevrey.directional {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f : P → E) (i : ι) : P → E

A genuine derivative in one prescribed constant direction.

Equations

• EulerParameterWordGevrey.directional directions f i x = (fderiv ℝ f x) (directions i)

theorem EulerParameterWordGevrey.directional_contDiff {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (i : ι) : ContDiff ℝ (↑⊤) (directional directions f i)

theorem EulerParameterWordGevrey.wordDerivative_zero {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f : P → E) (w : Fin 0 → ι) (x : P) : wordDerivative directions f w x = f x

theorem EulerParameterWordGevrey.wordDerivative_comp_clm {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] (directions : ι → P) (L : E →L[ℝ] F) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) (x : P) : wordDerivative directions (⇑L ∘ f) w x = L (wordDerivative directions f w x)

Every bounded linear map commutes with the actual ordered spatial derivative.

theorem EulerParameterWordGevrey.wordDerivative_add {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {n : ℕ} (w : Fin n → ι) (x : P) : wordDerivative directions (f + g) w x = wordDerivative directions f w x + wordDerivative directions g w x

theorem EulerParameterWordGevrey.wordDerivative_sub {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {n : ℕ} (w : Fin n → ι) (x : P) : wordDerivative directions (f - g) w x = wordDerivative directions f w x - wordDerivative directions g w x

theorem EulerParameterWordGevrey.wordDerivative_snoc {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) (i : ι) (x : P) : wordDerivative directions f (Fin.snoc w i) x = wordDerivative directions (directional directions f i) w x

Removing the last word letter differentiates the function in that direction first.

theorem EulerParameterWordGevrey.wordSum_zero {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (f : P → E) (x : P) : wordSum directions f 0 x = ‖f x‖

theorem EulerParameterWordGevrey.wordSum_nonneg {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (f : P → E) (n : ℕ) (x : P) : 0 ≤ wordSum directions f n x

theorem EulerParameterWordGevrey.wordSum_succ {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : wordSum directions f (n + 1) x = ∑ i : ι, wordSum directions (directional directions f i) n x

The genuine word sum decomposes as the sum of its first directional derivatives.

theorem EulerParameterWordGevrey.wordSum_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) (L : E →L[ℝ] F) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : wordSum directions (⇑L ∘ f) n x ≤ ‖L‖ * wordSum directions f n x

A fixed bounded map preserves the radius and factorial shift in the actual word sum.

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

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

theorem EulerParameterWordGevrey.wordSum_sub_const_succ {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (c : E) (n : ℕ) (x : P) : wordSum directions (f - fun (x : P) => c) (n + 1) x = wordSum directions f (n + 1) x

Subtracting a frozen coefficient has no positive-order derivative.