Absorbing a fixed Sobolev coefficient order once

The actual coefficient blocks are finite sums of ordinary coefficient jets. Their alphabet count and fixed base derivative order enlarge only the coefficient radius, once. No forcing or solution radius is changed.

theorem EulerParameterWordGevrey.block_eq_sum_levels {P : Type u_1} {E : Type u_2} {ι : Type u_3} [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 x = ∑ k ∈ Finset.range (q + 1), wordSum directions f (n + k) x

The actual fixed-base block is the finite sum of the higher word levels.

def EulerParameterWordGevrey.sobolevCoefficientRadius (ι : Type u_4) [Fintype ι] (Rc : ℝ) : ℝ

The enlarged radius is a property only of the coefficient alphabet.

Equations

• EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc = 4 * (max 1 ↑(Fintype.card ι) * Rc)

def EulerParameterWordGevrey.sobolevCoefficientAmplitude (ι : Type u_4) [Fintype ι] (q : ℕ) (Rc C : ℝ) : ℝ

For fixed q this is a literal polynomial in the original coefficient radius and amplitude, with numerical factorial coefficients.

Equations

• EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C = 2 ^ q * C * ∑ k ∈ Finset.range (q + 1), EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ^ k * ↑k.factorial ^ 2

theorem EulerParameterWordGevrey.sobolevCoefficientRadius_nonneg {ι : Type u_3} [Fintype ι] (Rc : ℝ) (hRc : 0 ≤ Rc) : 0 ≤ sobolevCoefficientRadius ι Rc

theorem EulerParameterWordGevrey.sobolevCoefficientAmplitude_nonneg {ι : Type u_3} [Fintype ι] (q : ℕ) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) : 0 ≤ sobolevCoefficientAmplitude ι q Rc C

theorem EulerParameterWordGevrey.coefficientBlock_of_tensor_bound {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) (q : ℕ) (A : P → E) (hA : ContDiff ℝ (↑⊤) A) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hAb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : coefficientBlock directions q A n x ≤ sobolevCoefficientAmplitude ι q Rc C * EulerGevrey.majorant (sobolevCoefficientRadius ι Rc) 0 n

All actual fixed-Sobolev coefficient blocks have an unshifted factorial bound after a single coefficient-radius enlargement.

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

theorem EulerParameterWordGevrey.baseSize_of_tensor_bound {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) (q : ℕ) (A : P → E) (hA : ContDiff ℝ (↑⊤) A) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hAb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (x : P) : baseSize directions q A x ≤ sobolevCoefficientAmplitude ι q Rc C