Actual transported fast jets with a uniform finite-budget constant.

noncomputable def AVenhance.Infra.Section4.amnrHigherFastConstant {β : ℝ} (I : Ingredients β) (K : ℝ) : ℝ

Uniform constant controlling the higher-order fast velocity estimates.

Equations

• AVenhance.Infra.Section4.amnrHigherFastConstant I K = max 1 ((1 + 2 ^ (AVenhance.Nstar β + 1) * K) ^ AVenhance.Nstar β * AVenhance.Infra.Section4.amnrStreamMixedCurrentConstant I)

theorem AVenhance.Infra.Section4.amnrHigherFastConstant_one_le {β K : ℝ} (I : Ingredients β) : 1 ≤ amnrHigherFastConstant I K

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

The current fast jet is obtained from the actual transported stream; only strictly lower material levels of the coarse gradient are consumed.