Actual higher material velocity bounds by source scale summation.

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

The actual source scale steps telescope with coefficient one on the coarse term. No estimate on the current material velocity level is assumed.