Spatial radius bookkeeping for composition with an actual flow map.

theorem AVenhance.Infra.Section4.amnr_iteratedFDeriv_comp_radius_bound {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {g : E → E} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {ε C D : ℝ} (hε : 0 < ε) (hD : 1 ≤ D) (n : ℕ) (x : E) (houter : ∀ i ≤ n, ‖iteratedFDeriv ℝ i f (g x)‖ ≤ C * ε⁻¹ ^ i) (hinner : ∀ i < n, ‖iteratedFDeriv ℝ (i + 1) g x‖ ≤ D * ε⁻¹ ^ i) : ‖iteratedFDeriv ℝ n (f ∘ g) x‖ ≤ ↑n.factorial * C * D ^ n * ε⁻¹ ^ n

A function whose jets cost ε⁻ⁱ, composed with a state map whose positive jets cost ε⁻⁽ⁱ⁻¹⁾, retains the same spatial radius.