Positivity and finite spatial uniformity of the higher source-step constants.

theorem AVenhance.Infra.Section4.amnrHigherVelocityStepConstant_nonneg {β K : ℝ} (I : Ingredients β) (hK : 0 ≤ K) (n k : ℕ) : 0 ≤ amnrHigherVelocityStepConstant I K n k

theorem AVenhance.Infra.Section4.amnrHigherVelocityStepConstant_mono_spatial {β K : ℝ} (I : Ingredients β) (hK : 0 ≤ K) (n : ℕ) {k l : ℕ} (hkl : k ≤ l) : amnrHigherVelocityStepConstant I K n k ≤ amnrHigherVelocityStepConstant I K n l