Scale-uniform all-order estimates for the actual source forward and inverse flows.

noncomputable def AVenhance.Infra.Section4.amnrFlowSpatialSourceConstant (N : ℕ) : ℝ

A single finite source constant for all spatial flow jets needed by AMNR.

Equations

• AVenhance.Infra.Section4.amnrFlowSpatialSourceConstant N = AVenhance.Infra.Section4.amnrJacobianJetConstant (2 ^ (-25) * 2 ^ (N + 1) * AVenhance.Infra.Section4.amnrSpatialVelocityConstant N) N

theorem AVenhance.Infra.Section4.amnrFlowSpatialSourceConstant_pos (N : ℕ) : 0 < amnrFlowSpatialSourceConstant N

theorem AVenhance.Infra.Section4.amnr_previous_flow_iteratedFDeriv_norm_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (s t : ℝ) (ht : |t - s| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (n : ℕ) (hbudget : n ≤ Nstar β) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ (n + 1) (fun (y : Homogenization.Vec 2) => flow (streamVel (Φ (m - 1))) ⋯ ⋯ t y s) x‖ ≤ amnrFlowSpatialSourceConstant (Nstar β) * (epsilon β I.Λ (m - 1))⁻¹ ^ n

The stream-regularity estimates and the actual source cutoff length control all actual spatial flow operators by one constant independent of the scale and the starting time.

theorem AVenhance.Infra.Section4.amnr_xFlow_iteratedFDeriv_norm_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (n : ℕ) (hbudget : n ≤ Nstar β) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ (n + 1) (I.xFlow hΦ m l t) x‖ ≤ amnrFlowSpatialSourceConstant (Nstar β) * (epsilon β I.Λ (m - 1))⁻¹ ^ n

Every actual forward-flow spatial jet has the source spatial radius.

theorem AVenhance.Infra.Section4.amnr_xFlowInv_iteratedFDeriv_norm_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (n : ℕ) (hbudget : n ≤ Nstar β) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ (n + 1) (I.xFlowInv hΦ m l t) x‖ ≤ amnrFlowSpatialSourceConstant (Nstar β) * (epsilon β I.Λ (m - 1))⁻¹ ^ n

The inverse flow has the identical all-order rate by exchanging its actual initial and target times.