Quantitative finite-product estimates for actual correction monomials.

theorem AVenhance.Infra.Section4.amnrWeight_counts (S H : ℝ) (w : List (Option (Fin 2))) : amnrWeight S H w = S ^ amnrSpatialCount w * H ^ amnrMaterialCount w

theorem AVenhance.Infra.Section4.amnrAdvectionProduct_abs_le {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {S H V C : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hC : 0 ≤ C) (A : List AmnrAdvectionFactor) (z : AmnrSpace) (hA : ∀ a ∈ A, |amnrWord c a.2 (v a.1) z| ≤ C * V * amnrWeight S H a.2) : |amnrAdvectionProduct c v A z| ≤ (C * V) ^ A.length * S ^ (List.map (fun (a : AmnrAdvectionFactor) => amnrSpatialCount a.2) A).sum * H ^ (List.map (fun (a : AmnrAdvectionFactor) => amnrMaterialCount a.2) A).sum

A product of actual velocity jets is bounded by its exact count powers.

theorem AVenhance.Infra.Section4.amnrAdvectionTermValue_abs_le {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {f : AmnrSpace → ℝ} {S H V C F : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hC : 0 ≤ C) (t : AmnrAdvectionTerm) (z : AmnrSpace) (hA : ∀ a ∈ t.factors, |amnrWord c a.2 (v a.1) z| ≤ C * V * amnrWeight S H a.2) (hf : |amnrWord c t.scalarWord f z| ≤ F * V * amnrWeight S H t.scalarWord) : |amnrAdvectionTermValue c v f t z| ≤ C ^ t.factors.length * F * V ^ (t.factors.length + 1) * S ^ amnrTermSpatialCount t * H ^ amnrTermMaterialCount t

One scalar jet and its fast factors give the exact total-count bound.