Exact mixed jets of the actual transported stream summands.

theorem AVenhance.Infra.Section4.amnr_nextStreamTerm_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.nextStreamTerm m (Φ (m - 1)) ⋯ z.1 z.2 k

The actual stream summand is jointly smooth, with no quantitative premise.

theorem AVenhance.Infra.Section4.amnr_nextStreamTerm_word_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (w : List (Option (Fin 2))) : ContDiff ℝ (↑⊤) (amnrWord (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w fun (z : AmnrSpace) => I.nextStreamTerm m (Φ (m - 1)) ⋯ z.1 z.2 k)

Every actual differential word is smooth; regularity is proved before identifying its material cancellations.

theorem AVenhance.Infra.Section4.amnr_nextStreamTerm_mixed_word {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (α : List (Fin 2)) (ℓ : ℕ) (z : AmnrSpace) : amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α ++ List.replicate ℓ none) (fun (y : AmnrSpace) => I.nextStreamTerm m (Φ (m - 1)) ⋯ y.1 y.2 k) z = iteratedDeriv ℓ (I.hatZetaML m (lIdx β I.Λ m k) * I.zetaMK m k) z.1 * amnrSpaceWord α (fun (y : Homogenization.Vec 2) => psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) z.1 y)) z.2

Material derivatives hit only the actual time cutoff, at every spatial order.

theorem AVenhance.Infra.Section4.amnr_transportProfile_spatialWord_abs_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (α : List (Fin 2)) (hbudget : α.length ≤ Nstar β) (z : AmnrSpace) (ht : |z.1 - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) : |amnrSpaceWord α (fun (y : Homogenization.Vec 2) => psi β I.Λ m k (I.xFlowInv hΦ m (lIdx β I.Λ m k) z.1 y)) z.2| ≤ amnrTransportSpatialConstant (Nstar β) * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length

Ordered spatial profile derivatives inherit the actual operator-norm bound.

theorem AVenhance.Infra.Section4.amnr_nextStreamTerm_mixed_abs_le_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (α : List (Fin 2)) (ℓ : ℕ) (hbudget : α.length + 2 * ℓ ≤ Nstar β) (z : AmnrSpace) : |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α ++ List.replicate ℓ none) (fun (y : AmnrSpace) => I.nextStreamTerm m (Φ (m - 1)) ⋯ y.1 y.2 k) z| ≤ 2 ^ ℓ * I.Chat * I.Czeta * (amnrTransportSpatialConstant (Nstar β) * a β I.Λ m * epsilon β I.Λ m ^ 2 * (epsilon β I.Λ m)⁻¹ ^ α.length) * (tau β I.Λ m)⁻¹ ^ ℓ

All actual mixed summand jets have the fine spatial and cutoff-time rates. The paper's weighted budget is checked before either primitive bound.