Actual all-order spatial flow estimates from primitive field jets.

theorem AVenhance.Infra.Section4.amnrStateDerivative_uncurry_eq (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : amnrStateDerivative (Function.uncurry b) (t, x) = Flow.jointSpatialFDeriv b t x

The actual state restriction equals the actual spatial field Jacobian.

theorem AVenhance.Infra.Section4.amnrFlowCurve_iteratedFDeriv_norm_le_of_primitive_jets {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M B C ε : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) {s a c : ℝ} (hac : a ≤ c) (hs : s ∈ Set.Icc a c) (hsmall : (c - a) * M ≤ 1 / 2) (hscale : (c - a) * B ≤ C) {N : ℕ} (hprimitive : ∀ i ≤ N, ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖iteratedFDeriv ℝ i (fun (y : Homogenization.Vec 2) => Flow.jointSpatialFDeriv b t y) x‖ ≤ B * ε⁻¹ ^ i) (n : ℕ) (hbudget : n ≤ N) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ (n + 1) (amnrFlowCurve hX s a c) x‖ ≤ amnrJacobianJetConstant C n * ε⁻¹ ^ n

All spatial derivatives of the actual flow curve follow from the actual Volterra equation and primitive field estimates. No higher flow derivative or flow variation estimate is supplied as a hypothesis.

theorem AVenhance.Infra.Section4.amnr_flow_iteratedFDeriv_norm_le_of_primitive_jets {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M B C ε : ℝ} (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) {s a c t : ℝ} (hac : a ≤ c) (hs : s ∈ Set.Icc a c) (ht : t ∈ Set.Icc a c) (hsmall : (c - a) * M ≤ 1 / 2) (hscale : (c - a) * B ≤ C) {N : ℕ} (hprimitive : ∀ i ≤ N, ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖iteratedFDeriv ℝ i (fun (y : Homogenization.Vec 2) => Flow.jointSpatialFDeriv b t y) x‖ ≤ B * ε⁻¹ ^ i) (n : ℕ) (hbudget : n ≤ N) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ (n + 1) (fun (y : Homogenization.Vec 2) => X t y s) x‖ ≤ amnrJacobianJetConstant C n * ε⁻¹ ^ n

Evaluating the actual curve estimate gives the same spatial radius for every fixed-time flow operator.