Actual higher fast-velocity jets from strictly lower coarse gradient levels.

theorem AVenhance.Infra.Section4.amnr_fastVelocity_mixed_abs_le_of_lower_gradient_bounds {β C Cb : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (hCb : 0 ≤ Cb) (α : List (Fin 2)) (n : ℕ) (hbudget : α.length + 1 + 2 * n ≤ Nstar β) (i : Fin 2) (z : AmnrSpace) (hBb : ∀ (p q : Fin 2) (η : List (Fin 2)), ∀ r < n, η.length + 2 * r + 2 ≤ Nstar β → |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord η r) (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) p q) z| ≤ Cb * AVenhance.a β I.Λ m * (epsilon β I.Λ m)⁻¹ ^ η.length * AVenhance.a β I.Λ m ^ r) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α n) (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2 i - streamVel (Φ (m - 1)) y.1 y.2 i) z| ≤ (1 + 2 ^ (Nstar β + 1) * Cb) ^ n * amnrStreamMixedCurrentConstant I * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ α.length * a β I.Λ m ^ n

The actual fast velocity has every mixed jet from lower material levels of the coarse gradient. The input remains explicit in this conditional induction step; its transported scalar and every commutator are proved.