Preserve the exact spatial radius in the all-order fixed-equation induction.

theorem AVenhance.Infra.Section4.amnrNormalizedJacobian_fixed_equation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Q : E → F} {A : F → F →L[ℝ] F} (hQ : ContDiff ℝ (↑⊤) Q) {ε : ℝ} (hε : 0 < ε) (R : E →L[ℝ] F) (heq : ∀ (y : E), fderiv ℝ Q y = R + A (Q y) ∘SL fderiv ℝ Q y) (x : E) : fderiv ℝ (fun (y : E) => ε⁻¹ • Q (ε • y)) x = R + A (ε • ε⁻¹ • Q (ε • x)) ∘SL fderiv ℝ (fun (y : E) => ε⁻¹ • Q (ε • y)) x

Normalize the initial and trajectory states by the same positive radius. The derivative equation retains its constant initial-data operator.

theorem AVenhance.Infra.Section4.amnrJacobianJet_norm_le_of_scaled_fixed_equation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Q : E → F} {A : F → F →L[ℝ] F} (hQ : ContDiff ℝ (↑⊤) Q) (hA : ContDiff ℝ (↑⊤) A) (R : E →L[ℝ] F) (hR : ‖R‖ ≤ 1) (heq : ∀ (y : E), fderiv ℝ Q y = R + A (Q y) ∘SL fderiv ℝ Q y) {ε : ℝ} (hε : 0 < ε) (x : E) (hsmall : ‖A (Q x)‖ ≤ 1 / 2) {C : ℝ} {N : ℕ} (hprimitive : ∀ i ≤ N, ‖iteratedFDeriv ℝ i A (Q x)‖ ≤ C * ε⁻¹ ^ i) (n : ℕ) (hbudget : n ≤ N) : ‖iteratedFDeriv ℝ (n + 1) Q x‖ ≤ amnrJacobianJetConstant C n * ε⁻¹ ^ n

Radius normalization loses no extra spatial derivative: the (n+1)-st solution derivative has exactly radius ε⁻ⁿ.