Actual mixed flow-average bounds for the temperature forcing coefficient.

theorem AVenhance.Infra.Section4.amnr_flowAverageA0Plus_mixed_of_flow_bounds {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {X : ℝ} (hX : 0 ≤ X) (hflow : ∀ (m : ℕ), 1 ≤ m → ∀ (l : ℤ) (α : List (Fin 2)) (n : ℕ), α.length + 2 * n ≤ Nstar β → ∀ (z : AmnrSpace), |z.1 - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m → ∀ (i p : Fin 2), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (amnrMixedWord α n) (fun (y : AmnrSpace) => I.flowGrad hΦ m l y.1 y.2 i p) z| ≤ X * (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length * (tauP β I.Λ m)⁻¹ ^ n) (m : ℕ) : 1 ≤ m → ∀ (j k i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w ≤ Nstar β → ∀ (z : AmnrSpace), |amnrWord (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (amnrFlowAverageA0Plus I hΦ m j k i p) z| ≤ 3 * 2 ^ Nstar β * I.Chat * (2 ^ Nstar β * X * X) * amnrWeight (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (tauP β I.Λ m)⁻¹ w

the left-Jacobian form's cutoff average has two flow factors in each summand. The additional factor costs one Leibniz factor at every mixed order and changes no spatial or material exponent.