A single-radius inverse estimate in genuine fixed Sobolev blocks

The fixed Sobolev inverse bound is applied to each actual external word. Its commutator contains only positive external coefficient derivatives. Consequently the original factorial radius is preserved at every grade.

Positive external-order commutators in actual fixed Sobolev blocks

The commutator is an explicit difference of genuine derivatives and the undifferentiated coefficient action. Its direct word recurrence places at least one external derivative on the coefficient in every term.

noncomputable def EulerParameterWordGevrey.wordCommutator {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] (directions : ι → P) (A : P → E →L[ℝ] F) (f : P → E) {n : ℕ} (w : Fin n → ι) : P → F

The actual external word commutator of operator multiplication.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerParameterWordGevrey.wordCommutator_contDiff {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] (directions : ι → P) (A : P → E →L[ℝ] F) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) : ContDiff ℝ (↑⊤) (wordCommutator directions A f w)

theorem EulerParameterWordGevrey.wordCommutator_snoc {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] (directions : ι → P) (A : P → E →L[ℝ] F) (f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) (i : ι) : wordCommutator directions A f (Fin.snoc w i) = wordCommutator directions A (directional directions f i) w + wordDerivative directions (fun (y : P) => (directional directions A i y) (f y)) w

noncomputable def EulerParameterWordGevrey.commutatorBlock {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) (n : ℕ) (x : P) : ℝ

Commutator block, given by ∑ w : Fin n → ι, baseSize directions q (wordCommutator directions A f w) x.

Equations

• EulerParameterWordGevrey.commutatorBlock directions q A f n x = ∑ w : Fin n → ι, EulerParameterWordGevrey.baseSize directions q (EulerParameterWordGevrey.wordCommutator directions A f w) x

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

theorem EulerParameterWordGevrey.commutatorBlock_zero {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) (x : P) : commutatorBlock directions q A f 0 x = 0

theorem EulerParameterWordGevrey.commutatorBlock_nonneg {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) (n : ℕ) (x : P) : 0 ≤ commutatorBlock directions q A f n x

theorem EulerParameterWordGevrey.commutatorBlock_succ_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) : commutatorBlock directions q A f (n + 1) x ≤ ∑ i : ι, (commutatorBlock directions q A (directional directions f i) n x + block directions q (fun (y : P) => (directional directions A i y) (f y)) n x)

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

theorem EulerParameterWordGevrey.commutatorBlock_bound {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) : commutatorBlock directions q A f n x ≤ EulerJetProductBounds.commutatorConvolution (fun (k : ℕ) => coefficientBlock directions q A k x) (fun (k : ℕ) => block directions q f k x) n

Every external commutator term contains a positive external derivative of the coefficient, with no enlargement of solution or forcing radii.

theorem EulerParameterWordGevrey.block_inverse_bound {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 →L[ℝ] E) (u f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (heq : ∀ (y : P), (A y) (u y) = f y) (x : P) (inverse : E →L[ℝ] E) (hleft : ∀ (v : E), inverse ((A x) v) = v) (I B : ℝ) (hinv : ‖inverse‖ ≤ I) (hbase : baseSize directions q A x ≤ B) (n : ℕ) : block directions q u n x ≤ sobolevInverseCost I B q * (block directions q f n x + commutatorBlock directions q A u n x)

theorem EulerParameterWordGevrey.block_inverse_recurrence {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 →L[ℝ] E) (u f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (heq : ∀ (y : P), (A y) (u y) = f y) (x : P) (inverse : E →L[ℝ] E) (hleft : ∀ (v : E), inverse ((A x) v) = v) (I B : ℝ) (hinv : ‖inverse‖ ≤ I) (hbase : baseSize directions q A x ≤ B) (n : ℕ) : block directions q u n x ≤ sobolevInverseCost I B q * (block directions q f n x + ∑ j ∈ Finset.range n, ↑(n.choose (j + 1)) * coefficientBlock directions q A (j + 1) x * block directions q u (n - (j + 1)) x)

Genuine fixed-Sobolev external-word recurrence with the computed base inverse constant.

theorem EulerParameterWordGevrey.block_inverse_gevrey {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 →L[ℝ] E) (u f : P → E) (hA : ContDiff ℝ (↑⊤) A) (hu : ContDiff ℝ (↑⊤) u) (hf : ContDiff ℝ (↑⊤) f) (heq : ∀ (y : P), (A y) (u y) = f y) (inverse : P → E →L[ℝ] E) (hleft : ∀ (x : P) (v : E), (inverse x) ((A x) v) = v) (I B C D M Rc R : ℝ) (_hC : 0 ≤ C) (_hD : 0 ≤ D) (hM : 1 ≤ M) (hMC : sobolevInverseCost I B q * C ≤ M) (hMD : sobolevInverseCost I B q * D ≤ M) (hRc : 0 ≤ Rc) (hR : 2 * M * (Rc + 1) ≤ R) (hinv : ∀ (x : P), ‖inverse x‖ ≤ I) (hbase : ∀ (x : P), baseSize directions q A x ≤ B) (hcoeff : ∀ (j : ℕ) (x : P), coefficientBlock directions q A (j + 1) x ≤ C * (Rc ^ (j + 1) * ↑(j + 1).factorial ^ 2)) (d : ℕ) (hforce : ∀ (n : ℕ) (x : P), block directions q f n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : block directions q u n x ≤ EulerGevrey.majorant R (d + 1) n

One factorial shift in fixed Hq, using the identical input and output radius and constants independent of the input shift and external order.