Genuine word-sum product estimates

The binomial convolution is proved directly for the sum over ordered directional words. The forcing and solution word sums stay unchanged; there is no dimension factor or enlargement of their radius.

theorem EulerParameterWordGevrey.directional_bilinear {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (directions : ι → P) (B : E →L[ℝ] F →L[ℝ] G) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : ι) : directional directions (fun (x : P) => (B (f x)) (g x)) i = (fun (x : P) => (B (f x)) (directional directions g i x)) + fun (x : P) => (B (directional directions f i x)) (g x)

The ordinary product rule in a fixed direction, as an equality of actual functions.

theorem EulerParameterWordGevrey.sum_convolution_right {ι : Type u_5} [Fintype ι] (A : ℕ → ℝ) (B : ι → ℕ → ℝ) (n : ℕ) : ∑ i : ι, EulerJetProductBounds.leibnizConvolution A (B i) n = EulerJetProductBounds.leibnizConvolution A (fun (k : ℕ) => ∑ i : ι, B i k) n

theorem EulerParameterWordGevrey.sum_convolution_left {ι : Type u_5} [Fintype ι] (A : ι → ℕ → ℝ) (B : ℕ → ℝ) (n : ℕ) : ∑ i : ι, EulerJetProductBounds.leibnizConvolution (A i) B n = EulerJetProductBounds.leibnizConvolution (fun (k : ℕ) => ∑ i : ι, A i k) B n

theorem EulerParameterWordGevrey.wordSum_bilinear_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [Fintype ι] (directions : ι → P) (B : E →L[ℝ] F →L[ℝ] G) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (x : P) : wordSum directions (fun (y : P) => (B (f y)) (g y)) n x ≤ ‖B‖ * EulerJetProductBounds.leibnizConvolution (fun (k : ℕ) => wordSum directions f k x) (fun (k : ℕ) => wordSum directions g k x) n

Sharp binomial convolution of the actual directional word sums.

theorem EulerParameterWordGevrey.wordSum_clm_apply_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype ι] (directions : ι → P) (A : P → E →L[ℝ] F) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : wordSum directions (fun (y : P) => (A y) (f y)) n x ≤ EulerJetProductBounds.leibnizConvolution (fun (k : ℕ) => wordSum directions A k x) (fun (k : ℕ) => wordSum directions f k x) n

Operator application has product constant one in the actual word-sum norm.