Actual material-error energy from positive velocity jets and scalar energies.

theorem AVenhance.Infra.Section4.iterate_material_error_energy_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (D E : ℕ → ℝ) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length)) (iterateSpatialSplits w), ∀ (j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ D p.1.length) (hE : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length)) (iterateSpatialSplits w), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ E p.2.length) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) z ^ 2 ≤ 8 * ∑ j ∈ Finset.range (w.length + 1), if 1 ≤ j then ↑(w.length.choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length - j) else 0

The actual material error has an all-order squared-energy bound involving only positive velocity orders and strictly lower scalar gradient orders.