Actual lower source levels expressed at the current fine scale.

theorem AVenhance.Infra.Section4.amnrSourceJetLevels_coarse_gradient {β K : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {cut m : ℕ} (hlevels : AmnrSourceJetLevels I Φ K cut) (hK : 0 ≤ K) (hm : 1 ≤ m) (η : List (Fin 2)) (r : ℕ) (hr : r ≤ cut) (hbudget : η.length + 2 * r + 2 ≤ Nstar β) (i p : Fin 2) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord η r) (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) i p) z| ≤ K * a β I.Λ m * (epsilon β I.Λ m)⁻¹ ^ η.length * a β I.Λ m ^ r

theorem AVenhance.Infra.Section4.amnrSourceJetLevels_coarse_velocity {β K : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {cut m : ℕ} (hlevels : AmnrSourceJetLevels I Φ K cut) (hK : 0 ≤ K) (hm : 1 ≤ m) (η : List (Fin 2)) (r : ℕ) (hr : r ≤ cut) (hne : amnrMixedWord η r ≠ []) (hbudget : η.length + 2 * r + 1 ≤ Nstar β) (i : Fin 2) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord η r) (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2 i) z| ≤ K * epsilon β I.Λ m ^ (β - 1) * (epsilon β I.Λ m)⁻¹ ^ η.length * a β I.Λ m ^ r