Higher scale-step estimates from the actual lower source levels.

noncomputable def AVenhance.Infra.Section4.amnrHigherVelocityStepConstant {β : ℝ} (I : Ingredients β) (K : ℝ) (n k : ℕ) : ℝ

Step constant for higher-order velocity derivatives in the material recursion.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.amnr_velocity_higher_source_step {β C K : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {n m : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hlevels : AmnrSourceJetLevels I Φ K (n - 1)) (hK : 1 ≤ K) (α : List (Fin 2)) (hbudget : α.length + 2 * n + 1 ≤ Nstar β) (i : Fin 2) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) ((amnrWord (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) (List.replicate n none) fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2 i) - amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.replicate n none) fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2 i) z| ≤ amnrHigherVelocityStepConstant I K n α.length * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ n

Source scale step: the only inputs are the already established actual lower source levels. Fast jets and every correction are proved from them.