All spatial jets of actual transported shear profiles.

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

One finite constant for every transported profile spatial order.

Equations

• AVenhance.Infra.Section4.amnrTransportSpatialConstant N = ↑N.factorial * (2 * Real.pi) ^ N * AVenhance.Infra.Section4.amnrFlowSpatialSourceConstant N ^ N

theorem AVenhance.Infra.Section4.amnrTransportSpatialConstant_pos (N : ℕ) : 0 < amnrTransportSpatialConstant N

theorem AVenhance.Infra.Section4.amnr_transportProfile_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k l : ℤ) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => psi β I.Λ m k (I.xFlowInv hΦ m l z.1 z.2)

The actual inverse-flow profile is jointly smooth at all times.

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

Every actual transported profile derivative retains the fine spatial radius. Coarse flow derivatives are absorbed by the actual scale separation.