All spatial orders in the first material fast-velocity estimate.

theorem AVenhance.Infra.Section4.amnr_epsilon_inverse_prev_le_current {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : (epsilon β I.Λ (m - 1))⁻¹ ≤ (epsilon β I.Λ m)⁻¹

The previous spatial radius is no larger than the current one.

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

Uniform transported spatial amplitude through the finite source budget.

Equations

• AVenhance.Infra.Section4.amnrFastSpatialConstant I = 3 * I.Chat * I.Czeta * AVenhance.Infra.Section4.amnrTransportSpatialConstant (AVenhance.Nstar β)

theorem AVenhance.Infra.Section4.amnrFastSpatialConstant_pos {β : ℝ} (I : Ingredients β) : 0 < amnrFastSpatialConstant I

theorem AVenhance.Infra.Section4.amnr_stream_amplitude_spatial_cancel {E A β : ℝ} (hE : 0 < E) (hA : A * E = E ^ (β - 1)) (n : ℕ) : A * E ^ 2 * E⁻¹ ^ (n + 1) = E ^ (β - 1) * E⁻¹ ^ n

Abstract radius cancellation converts the stream amplitude into the actual fast-velocity amplitude without changing its spatial derivative order.