Gevrey bounds from the actual inverse-map differential identity

If DY = A ∘ Y and A has Gevrey-two derivatives, the positive derivatives of Y have the stronger bound C * L^n * n!² at order n+1, where L = 1 + 2*C*R. The proof uses the shifted Faà di Bruno weights and a strong induction, rather than iterating the general composition radius.

A shifted partition estimate for a differential equation

For the relation DY = A ∘ Y, the useful induction controls the order-j derivative of Y by (j-1)!². With those inner weights the normalized Faà di Bruno partition sum stays bounded at every positive order, provided its scalar argument is at most one half.

theorem EulerGevreyComposition.partSize_add_length_le {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : c.partSize i + c.length ≤ n + 1

theorem EulerGevreyComposition.sum_partSize_sq_le {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, ↑(c.partSize i) ^ 2 ≤ (↑n - ↑c.length + 1) * ↑n

def EulerGevreyComposition.predecessorFactorialProduct {n : ℕ} (c : OrderedFinpartition n) : ℝ

Predecessor factorial product, given by ∏ i, ((c.partSize i - 1).factorial : ℝ).

Equations

• EulerGevreyComposition.predecessorFactorialProduct c = ∏ i : Fin c.length, ↑(c.partSize i - 1).factorial

def EulerGevreyComposition.predecessorPartitionWeight {n : ℕ} (x : ℝ) (c : OrderedFinpartition n) : ℝ

Predecessor partition weight, given by x^c.length * ((c.length.factorial : ℝ) * predecessorFactorialProduct c)^2.

Equations

• EulerGevreyComposition.predecessorPartitionWeight x c = x ^ c.length * (↑c.length.factorial * EulerGevreyComposition.predecessorFactorialProduct c) ^ 2

noncomputable def EulerGevreyComposition.predecessorPartitionSum (n : ℕ) (x : ℝ) : ℝ

Predecessor partition sum, given by ∑ c : OrderedFinpartition n, predecessorPartitionWeight x c.

Equations

• EulerGevreyComposition.predecessorPartitionSum n x = ∑ c : OrderedFinpartition n, EulerGevreyComposition.predecessorPartitionWeight x c

theorem EulerGevreyComposition.predecessorPartitionWeight_nonneg {n : ℕ} (x : ℝ) (hx : 0 ≤ x) (c : OrderedFinpartition n) : 0 ≤ predecessorPartitionWeight x c

theorem EulerGevreyComposition.predecessorFactorialProduct_extendLeft {n : ℕ} (c : OrderedFinpartition n) : predecessorFactorialProduct c.extendLeft = predecessorFactorialProduct c

theorem EulerGevreyComposition.predecessorFactorialProduct_extendMiddle {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : predecessorFactorialProduct (c.extendMiddle i) = ↑(c.partSize i) * predecessorFactorialProduct c

theorem EulerGevreyComposition.predecessorPartitionWeight_extendLeft {n : ℕ} (x : ℝ) (c : OrderedFinpartition n) : predecessorPartitionWeight x c.extendLeft = x * (↑c.length + 1) ^ 2 * predecessorPartitionWeight x c

theorem EulerGevreyComposition.predecessorPartitionWeight_extendMiddle {n : ℕ} (x : ℝ) (c : OrderedFinpartition n) (i : Fin c.length) : predecessorPartitionWeight x (c.extendMiddle i) = ↑(c.partSize i) ^ 2 * predecessorPartitionWeight x c

theorem EulerGevreyComposition.predecessorPartitionSum_succ (n : ℕ) (x : ℝ) : predecessorPartitionSum (n + 1) x = ∑ c : OrderedFinpartition n, (x * (↑c.length + 1) ^ 2 + ∑ i : Fin c.length, ↑(c.partSize i) ^ 2) * predecessorPartitionWeight x c

theorem EulerGevreyComposition.predecessorPartitionSum_succ_le (n : ℕ) (hn : 0 < n) (x : ℝ) (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) : predecessorPartitionSum (n + 1) x ≤ (↑n + 1) ^ 2 * predecessorPartitionSum n x

theorem EulerGevreyComposition.predecessorPartitionSum_le (n : ℕ) (hn : 0 < n) (x : ℝ) (hx : 0 ≤ x) (hxhalf : x ≤ 1 / 2) : predecessorPartitionSum n x ≤ x * ↑n.factorial ^ 2

Unlike the unshifted weights, these weights have a uniformly bounded normalized sum on the scalar interval [0, 1/2].

theorem EulerGevreyComposition.predecessor_partition_bound_factorization {n : ℕ} (c : OrderedFinpartition n) (A B R S : ℝ) : A * S ^ c.length * ↑c.length.factorial ^ 2 * ∏ i : Fin c.length, B * R ^ c.partSize i * ↑(c.partSize i - 1).factorial ^ 2 = A * R ^ n * predecessorPartitionWeight (B * S) c

theorem EulerGevreyComposition.norm_taylorComp_predecessor_le {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (q : FormalMultilinearSeries ℝ F G) (p : FormalMultilinearSeries ℝ E F) (n : ℕ) (hn : 0 < n) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hBS : B * S ≤ 1 / 2) (hq : ∀ j ≤ n, ‖q j‖ ≤ A * S ^ j * ↑j.factorial ^ 2) (hp : ∀ (j : ℕ), 0 < j → j ≤ n → ‖p j‖ ≤ B * R ^ j * ↑(j - 1).factorial ^ 2) : ‖q.taylorComp p n‖ ≤ A * R ^ n * (B * S) * ↑n.factorial ^ 2

theorem EulerGevreyComposition.norm_iteratedFDeriv_comp_predecessor_at {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : E → F) (g : F → G) (n : ℕ) (hn : 0 < n) (x : E) (hf : ContDiffAt ℝ (↑n) f x) (hg : ContDiffAt ℝ (↑n) g (f x)) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hBS : B * S ≤ 1 / 2) (hgjet : ∀ j ≤ n, ‖iteratedFDeriv ℝ j g (f x)‖ ≤ A * S ^ j * ↑j.factorial ^ 2) (hfjet : ∀ (j : ℕ), 0 < j → j ≤ n → ‖iteratedFDeriv ℝ j f x‖ ≤ B * R ^ j * ↑(j - 1).factorial ^ 2) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ A * R ^ n * (B * S) * ↑n.factorial ^ 2

def EulerGevreyComposition.inverseMapRadius (C R : ℝ) : ℝ

Inverse map radius, given by 1 + 2*C*R.

Equations

• EulerGevreyComposition.inverseMapRadius C R = 1 + 2 * C * R

theorem EulerGevreyComposition.inverseMapRadius_ge_one (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 1 ≤ inverseMapRadius C R

theorem EulerGevreyComposition.inverseMapRadius_pos (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) : 0 < inverseMapRadius C R

theorem EulerGevreyComposition.norm_iteratedFDeriv_of_fderiv_eq_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Y : E → F) (A : F → E →L[ℝ] F) (hY : ContDiff ℝ (↑⊤) Y) (hA : ContDiff ℝ (↑⊤) A) (hDY : ∀ (x : E), fderiv ℝ Y x = A (Y x)) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hAjet : ∀ (j : ℕ) (y : F), ‖iteratedFDeriv ℝ j A y‖ ≤ C * R ^ j * ↑j.factorial ^ 2) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ (n + 1) Y x‖ ≤ C * inverseMapRadius C R ^ n * ↑n.factorial ^ 2

Positive derivatives of a genuine solution of DY = A ∘ Y have one fixed polynomial Gevrey radius. The value of Y need not be bounded.

theorem EulerGevreyComposition.positive_jets_of_fderiv_eq_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Y : E → F) (A : F → E →L[ℝ] F) (hY : ContDiff ℝ (↑⊤) Y) (hA : ContDiff ℝ (↑⊤) A) (hDY : ∀ (x : E), fderiv ℝ Y x = A (Y x)) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hAjet : ∀ (j : ℕ) (y : F), ‖iteratedFDeriv ℝ j A y‖ ≤ C * R ^ j * ↑j.factorial ^ 2) (n : ℕ) (hn : 0 < n) (x : E) : ‖iteratedFDeriv ℝ n Y x‖ ≤ C * inverseMapRadius C R ^ n * ↑n.factorial ^ 2

The same estimate in the usual unshifted form, directly usable as the inner-function hypothesis of the composition theorem.

theorem EulerGevreyComposition.contDiff_of_fderiv_eq_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (Y : E → F) (A : F → E →L[ℝ] F) (hY : Differentiable ℝ Y) (hA : ContDiff ℝ (↑⊤) A) (hDY : ∀ (x : E), fderiv ℝ Y x = A (Y x)) : ContDiff ℝ (↑⊤) Y

Smoothness itself follows by differentiating the genuine differential identity; it need not be supplied as an independent inverse-map assumption.

theorem EulerGevreyComposition.fderiv_eq_inverse_field {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X Y : E → E) (A : E → E →L[ℝ] E) (hX : Differentiable ℝ X) (hY : Differentiable ℝ Y) (hXY : ∀ (x : E), X (Y x) = x) (hleft : ∀ (x v : E), (A x) ((fderiv ℝ X x) v) = v) (x : E) : fderiv ℝ Y x = A (Y x)

The differential equation follows from an actual inverse identity and the actual inverse of the derivative of the original coordinate map.

theorem EulerGevreyComposition.norm_iteratedFDeriv_inverseMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X Y : E → E) (A : E → E →L[ℝ] E) (hX : Differentiable ℝ X) (hY : ContDiff ℝ (↑⊤) Y) (hA : ContDiff ℝ (↑⊤) A) (hXY : ∀ (x : E), X (Y x) = x) (hleft : ∀ (x v : E), (A x) ((fderiv ℝ X x) v) = v) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hAjet : ∀ (j : ℕ) (y : E), ‖iteratedFDeriv ℝ j A y‖ ≤ C * R ^ j * ↑j.factorial ^ 2) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ (n + 1) Y x‖ ≤ C * inverseMapRadius C R ^ n * ↑n.factorial ^ 2

Gevrey-two regularity of an actual smooth inverse map with a Gevrey-two inverse derivative field.

theorem EulerGevreyComposition.norm_iteratedFDeriv_comp_of_fderiv_eq_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (Y : E → F) (A : F → E →L[ℝ] F) (g : F → G) (hY : Differentiable ℝ Y) (hA : ContDiff ℝ (↑⊤) A) (hg : ContDiff ℝ (↑⊤) g) (hDY : ∀ (x : E), fderiv ℝ Y x = A (Y x)) (C R D S : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hD : 0 ≤ D) (hS : 0 ≤ S) (hAjet : ∀ (j : ℕ) (y : F), ‖iteratedFDeriv ℝ j A y‖ ≤ C * R ^ j * ↑j.factorial ^ 2) (hgjet : ∀ (j : ℕ) (y : F), ‖iteratedFDeriv ℝ j g y‖ ≤ D * S ^ j * ↑j.factorial ^ 2) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (g ∘ Y) x‖ ≤ D * (inverseMapRadius C R * (C * S + 2)) ^ n * ↑n.factorial ^ 2

Pullback by a map satisfying the actual inverse differential equation preserves Gevrey two, with an explicit polynomial radius and unchanged outer amplitude. Only differentiability of the inverse is an input.