Multiplication preserves the radius of genuine fixed-Sobolev word blocks #
Only coefficient blocks are compared with the coefficient radius. The input field's ordered word sum passes directly through the Leibniz estimate.
theorem
EulerParameterWordGevrey.block_clm_apply_gevrey
{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)
(Rc R C D : ℝ)
(hRc : 0 ≤ Rc)
(hRcR : Rc ≤ R)
(hC : 0 ≤ C)
(hD : 0 ≤ D)
(hcoeff : ∀ (n : ℕ) (x : P), coefficientBlock directions q A n x ≤ C * EulerGevrey.majorant Rc 0 n)
(d : ℕ)
(hfield : ∀ (n : ℕ) (x : P), block directions q f n x ≤ D * EulerGevrey.majorant R d n)
(n : ℕ)
(x : P)
:
theorem
EulerParameterWordGevrey.block_linear_gevrey
{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 : ℕ)
(L : E →L[ℝ] F)
(f : P → E)
(hf : ContDiff ℝ (↑⊤) f)
(R C : ℝ)
(d : ℕ)
(hb : ∀ (n : ℕ) (x : P), block directions q f n x ≤ C * EulerGevrey.majorant R d n)
(n : ℕ)
(x : P)
:
theorem
EulerParameterWordGevrey.block_add_gevrey
{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)
(R C D : ℝ)
(d : ℕ)
(hb : ∀ (n : ℕ) (x : P), block directions q f n x ≤ C * EulerGevrey.majorant R d n)
(hc : ∀ (n : ℕ) (x : P), block directions q g n x ≤ D * EulerGevrey.majorant R d n)
(n : ℕ)
(x : P)
: