Actual velocity induction through the next material level.

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

Constant controlling the velocity source when advancing the derivative cutoff.

Equations

• AVenhance.Infra.Section4.amnrSourceVelocityAdvanceConstant I K cut = K + 2 * AVenhance.Infra.Section4.amnrHigherVelocityStepConstant I K (cut + 1) (AVenhance.Nstar β)

theorem AVenhance.Infra.Section4.amnrSourceVelocityAdvanceConstant_ge {β K : ℝ} (I : Ingredients β) (hK : 0 ≤ K) (cut : ℕ) : K ≤ amnrSourceVelocityAdvanceConstant I K cut

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

All actual velocity levels up to the next material order follow from the lower source invariant, with one scale-independent constant.