Stream-regularity velocity jets in the factorial profile of the linear recurrence.

theorem AVenhance.Infra.Section4.iterate_velocity_factorial_profile {a e : ℝ} (ha : 0 ≤ a) (he : 0 < e) (n : ℕ) : 32 * a * e ^ 2 * ↑(n + 1).factorial * (256 * e⁻¹) ^ (n + 1) / (↑n + 2) ^ 2 ≤ 8192 * a * e * ↑n.factorial * (256 * e⁻¹) ^ n

The extra velocity factorial is absorbed by the printed denominator.

theorem AVenhance.Infra.Section4.iterate_velocity_analytic_profile_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (t : ℝ) (w : List (Fin 2)) (hw : 1 ≤ w.length) (x : Homogenization.Vec 2) (j : Fin 2) : |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y j) x| ≤ 8192 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) * ↑w.length.factorial * (256 * (epsilon β I.Λ (m - 1))⁻¹) ^ w.length

Every positive-order actual velocity jet has the source factorial-radius profile needed in the binomially grouped material error estimate.