Scalar normalization preserves the external word radius and fixed Sobolev order.

@[simp]

theorem EulerParameterWordGevrey.block_zero_function {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q n : ℕ) (x : P) : block directions q (fun (x : P) => 0) n x = 0

theorem EulerParameterWordGevrey.block_normalize_bound {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) (A : ℝ) (hA : 0 < A) (R C : ℝ) (d n : ℕ) (x : P) (hb : block directions q f n x ≤ A * (C * EulerGevrey.majorant R d n)) : block directions q (fun (y : P) => A⁻¹ • f y) n x ≤ C * EulerGevrey.majorant R d n

Normalize a positive scalar envelope without changing R, d, or q.

theorem EulerParameterWordGevrey.block_restore_bound {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (f g : P → E) (hf : ContDiff ℝ (↑⊤) f) (A : ℝ) (hA : 0 ≤ A) (he : ∀ (y : P), g y = A • f y) (R C : ℝ) (d n : ℕ) (x : P) (hb : block directions q f n x ≤ C * EulerGevrey.majorant R d n) : block directions q g n x ≤ A * (C * EulerGevrey.majorant R d n)

Restore the same scalar envelope after estimating a normalized actual solution.

theorem EulerParameterWordGevrey.value_zero_of_block_zero_bound {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) (x : P) (h : block directions q f 0 x ≤ 0) : f x = 0

A vanishing zeroth external block forces the actual value to vanish.