Quantitative material estimates for the actual transported stream summands.

theorem AVenhance.Infra.Section4.amnr_iteratedDeriv_product_abs_le {f g : ℝ → ℝ} {N n : ℕ} (hf : ContDiff ℝ (↑N) f) (hg : ContDiff ℝ (↑N) g) (hn : n ≤ N) {F G R : ℝ} (hF : 0 ≤ F) (_hG : 0 ≤ G) (hR : 0 ≤ R) (hfb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ F * R ^ j) (hgb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j g t| ≤ G * R ^ j) (t : ℝ) : |iteratedDeriv n (f * g) t| ≤ 2 ^ n * F * G * R ^ n

Time Leibniz estimates with one common derivative radius.

theorem AVenhance.Infra.Section4.amnr_inverse_tauP_le_inverse_tau {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : (tauP β I.Λ m)⁻¹ ≤ (tau β I.Λ m)⁻¹

The fine time-cutoff rate dominates the large-cutoff rate.

theorem AVenhance.Infra.Section4.amnr_psi_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (x : Homogenization.Vec 2) : |psi β I.Λ m k x| ≤ a β I.Λ m * epsilon β I.Λ m ^ 2

Exact amplitude bound of the prescribed shear profile.

theorem AVenhance.Infra.Section4.amnr_hatZeta_derivative_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : |iteratedDeriv j (I.hatZetaML m l) t| ≤ I.Chat * (tau β I.Λ m)⁻¹ ^ j

Actual large-cutoff derivatives in the fine time radius used by the stream-recursion material estimates.

theorem AVenhance.Infra.Section4.amnr_zeta_derivative_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : |iteratedDeriv j (I.zetaMK m k) t| ≤ I.Czeta * (tau β I.Λ m)⁻¹ ^ j

Fine-cutoff derivatives follow from the literal profile derivative data.