Composition preserves the Gevrey-two factorial bound

The inner function is only bounded in positive derivative orders, allowing unbounded coordinate changes such as a flow on all of Euclidean space. The Faà di Bruno partition estimate gives the fixed output radius R * (B*S + 2), independently of the derivative order.

theorem EulerGevreyComposition.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).factorial ^ 2 = A * R ^ n * partitionWeight (B * S) c

theorem EulerGevreyComposition.norm_taylorComp_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 : ℕ) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hq : ∀ j ≤ n, ‖q j‖ ≤ A * S ^ j * ↑j.factorial ^ 2) (hp : ∀ (j : ℕ), 0 < j → j ≤ n → ‖p j‖ ≤ B * R ^ j * ↑j.factorial ^ 2) : ‖q.taylorComp p n‖ ≤ A * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

A factorial-square bound for a formal Taylor composition, using exactly the derivatives that occur in its order-n Faà di Bruno formula.

theorem EulerGevreyComposition.norm_iteratedFDeriv_comp_gevrey_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 : ℕ) (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) (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.factorial ^ 2) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ A * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

The actual derivative of a composition obeys a Gevrey-two bound with a single fixed radius. Only finite jets at the two relevant points are needed.

theorem EulerGevreyComposition.norm_iteratedFDeriv_comp_gevrey {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) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hgjet : ∀ (j : ℕ) (y : F), ‖iteratedFDeriv ℝ j g y‖ ≤ A * S ^ j * ↑j.factorial ^ 2) (hfjet : ∀ (j : ℕ), 0 < j → ∀ (x : E), ‖iteratedFDeriv ℝ j f x‖ ≤ B * R ^ j * ↑j.factorial ^ 2) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ A * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

Uniform all-order composition bound. In particular the output radius does not grow with n and the outer amplitude remains linear.