Uniform radius bookkeeping for the primitive spatial velocity jets.

def AVenhance.Infra.Section4.amnrSpatialVelocityConstant (N : ℕ) : ℝ

A finite derivative-budget constant, independent of the scale.

Equations

• AVenhance.Infra.Section4.amnrSpatialVelocityConstant N = 2 ^ 5 * (2 ^ 8) ^ (N + 2) * ↑(N + 2).factorial * (↑N + 4) ^ 2

theorem AVenhance.Infra.Section4.amnrSpatialVelocityConstant_pos (N : ℕ) : 0 < amnrSpatialVelocityConstant N

theorem AVenhance.Infra.Section4.amnrStreamSpatialEnvelope_gradient {A E : ℝ} (hE : 0 < E) (n : ℕ) : amnrStreamSpatialEnvelope A E (n + 2) = 2 ^ 5 * (2 ^ 8) ^ (n + 2) * ↑(n + 2).factorial * ((↑n + 4) ^ 2 / (↑n + 3) ^ 5) * A * E⁻¹ ^ n

Undoing the stream seminorm produces two powers of the spatial radius which cancel its stream-amplitude factor E².

theorem AVenhance.Infra.Section4.amnrStreamSpatialEnvelope_le_uniform {A E : ℝ} (hA : 0 ≤ A) (hE : 0 < E) {n N : ℕ} (hn : n ≤ N) : amnrStreamSpatialEnvelope A E (n + 2) ≤ amnrSpatialVelocityConstant N * A * E⁻¹ ^ n

Every admissible spatial jet has one constant for the entire budget. Only abstract real algebra is used in this scale comparison.

theorem AVenhance.Infra.Section4.amnr_velocityGradient_spatial_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (hbudget : α.length + 2 ≤ Nstar β) (i p : Fin 2) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) (List.map some α) (amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ m) y.1 y.2) i p) z| ≤ amnrSpatialVelocityConstant (Nstar β) * a β I.Λ m * (epsilon β I.Λ m)⁻¹ ^ α.length

Spatial velocity-gradient jets have a single constant over the entire source derivative budget. The extra two stream derivatives are checked here.