Primitive spatial jets of the actual velocity, extracted from the stream-regularity estimates.

noncomputable def AVenhance.Infra.Section4.amnrStreamSpatialEnvelope (A E : ℝ) (n : ℕ) : ℝ

The exact pointwise envelope obtained by undoing the source stream seminorm.

Equations

• AVenhance.Infra.Section4.amnrStreamSpatialEnvelope A E n = 2 ^ 5 * A * E ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3) * ↑n.factorial * (2 ^ 8 * E⁻¹) ^ n / (↑n + 1) ^ 2

theorem AVenhance.Infra.Section4.amnr_stream_spatialWord_raw_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (hα : 2 ≤ α.length) (t : ℝ) (x : Homogenization.Vec 2) : ‖amnrSpaceWord α (Φ m t) x‖ ≤ amnrStreamSpatialEnvelope (a β I.Λ m) (epsilon β I.Λ m) α.length

Every spatial word of length at least two on the actual stream has the stream-regularity envelope. There is no assumed stream or velocity derivative norm.

theorem AVenhance.Infra.Section4.amnr_velocityGradient_spatialWord_raw_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (α : List (Fin 2)) (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‖ ≤ amnrStreamSpatialEnvelope (a β I.Λ m) (epsilon β I.Λ m) (α.length + 2)

The exact envelope for every spatial derivative of the actual velocity -gradient coefficient. Two additional derivatives fall on the stream.