Higher mixed flow bounds from actual transport and primitive jets.

theorem AVenhance.Infra.Section4.amnr_flow_mixed_abs_le_of_primitive_jets {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (G : Fin 2 → AmnrSpace → ℝ) (hG : ∀ (p : Fin 2), ContDiff ℝ (↑⊤) (G p)) (heq : ∀ (p : Fin 2) (z : AmnrSpace), amnrOp b none (G p) z = ∑ q : Fin 2, G q z * amnrVelocityGradient b p q z) {N : ℕ} {S H Cg Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hCg : 0 ≤ Cg) (hCb : 0 ≤ Cb) (z : AmnrSpace) (hGb : ∀ (p : Fin 2) (η : List (Fin 2)), η.length ≤ N → |amnrWord b (List.map some η) (G p) z| ≤ Cg * S ^ η.length) (hBb : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w + 2 ≤ N → |amnrWord b w (amnrVelocityGradient b i p) z| ≤ Cb * H * amnrWeight S H w) (α : List (Fin 2)) (n : ℕ) (hbudget : α.length + 2 * n ≤ N) (p : Fin 2) : |amnrWord b (amnrMixedWord α n) (G p) z| ≤ 2 ^ (α.length + 1) * Cg * (1 + 2 ^ (N + 1) * Cb) ^ n * S ^ α.length * H ^ n

Exact flow transport and lower gradient jets control every canonical mixed flow word. This helper estimates the actual differentiated products.