Uniform Taylor estimates for Banach-valued primitive fields.

theorem AVenhance.Infra.Section4.amnr_field_quadratic_remainder {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (hf : ContDiff ℝ (↑⊤) f) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (x : E), ‖iteratedFDeriv ℝ 2 f x‖ ≤ C) (x h : E) : ‖f (x + h) - f x - (fderiv ℝ f x) h‖ ≤ C * ‖h‖ * ‖h‖

A primitive second derivative bound gives a uniform quadratic Taylor remainder in any real normed domain and target. The target may itself be a higher derivative operator space.

theorem AVenhance.Infra.Section4.amnr_joint_field_state_quadratic_remainder {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ × E → F} (hf : ContDiff ℝ (↑⊤) f) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ (z : ℝ × E), ‖iteratedFDeriv ℝ 2 f z‖ ≤ C) (t : ℝ) (x h : E) : ‖f (t, x + h) - f (t, x) - (fderiv ℝ f (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ E) h‖ ≤ C * ‖h‖ * ‖h‖

Joint primitive Taylor control restricts to state perturbations at a fixed time, with no extra norm cost from the time coordinate.