Fixed Sobolev blocks of genuine external parameter words

The fixed base order is kept inside each actual external word. Product bounds place its finite cost on coefficient blocks, preserving the input and output external radius and factorial shift.

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

The fixed-order sum of the actual spatial derivative norms.

Equations

• EulerParameterWordGevrey.baseSize directions q f x = ∑ k ∈ Finset.range (q + 1), EulerParameterWordGevrey.wordSum directions f k x

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

A fixed Sobolev base norm inside the sum of actual external words.

Equations

• EulerParameterWordGevrey.block directions q f n x = ∑ w : Fin n → ι, EulerParameterWordGevrey.baseSize directions q (EulerParameterWordGevrey.wordDerivative directions f w) x

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

The finite base-order Leibniz constant belongs only to the coefficient block.

Equations

• EulerParameterWordGevrey.coefficientBlock directions q f n x = 2 ^ q * EulerParameterWordGevrey.block directions q f n x

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

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

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

theorem EulerParameterWordGevrey.baseSize_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) : baseSize directions 0 f x = ‖f x‖

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

theorem EulerParameterWordGevrey.baseSize_mono {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) {p q : ℕ} (hpq : p ≤ q) : baseSize directions p f x ≤ baseSize directions q f x

theorem EulerParameterWordGevrey.norm_le_baseSize {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (f : P → E) (x : P) : ‖f x‖ ≤ baseSize directions q f x

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

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

theorem EulerParameterWordGevrey.baseSize_clm_apply_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) (q : ℕ) (A : P → E →L[ℝ] F) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (x : P) : baseSize directions q (fun (y : P) => (A y) (f y)) x ≤ 2 ^ q * baseSize directions q A x * baseSize directions q f x

theorem EulerParameterWordGevrey.block_zero {P : Type u_1} {E : Type u_2} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (f : P → E) (x : P) : block directions q f 0 x = baseSize directions q f x

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

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

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

theorem EulerParameterWordGevrey.block_clm_apply_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) (q : ℕ) (A : P → E →L[ℝ] F) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : block directions q (fun (y : P) => (A y) (f y)) n x ≤ EulerJetProductBounds.leibnizConvolution (fun (k : ℕ) => coefficientBlock directions q A k x) (fun (k : ℕ) => block directions q f k x) n

Direct Leibniz in external words with fixed Sobolev blocks.