The actual material commutator in analytic norm weights.

theorem AVenhance.Infra.Section4.iterate_terminal_analytic_material_error_bound {s : ℝ} (hs1 : s ≤ 1) {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} {a : AmnrSpace → ℝ} (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)) (ha : ContinuousOn a (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (i : ℕ) {B H G r L : ℝ} (hB : 0 ≤ B) (hH : 0 ≤ H) (hG : 0 ≤ G) (hr : 0 ≤ r) (hL : 0 < L) (hgain : r / L ≤ 1 / 2) (D : ℕ → ℝ) (hD : ∀ (n : ℕ), 0 ≤ D n) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w), ∀ (j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ B * ↑p.1.length.factorial * r ^ p.1.length) (hEa : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, a z ^ 2 ≤ (H * ↑(w.length + 2 * i - 1).factorial * L ^ (w.length + 1)) ^ 2) (hEv : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ (G * ↑(p.2.length + 2 * i).factorial * L ^ p.2.length * D p.2.length) ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, a z * iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) z| ≤ 2 * H * B * G * r * (↑(w.length + 2 * i).factorial * L ^ w.length) ^ 2 * ∑ k ∈ Finset.range w.length, (1 / 2) ^ k * D (w.length - 1 - k)

Analytic velocity jets and strictly lower scalar gradient energies give the geometric linear norm recurrence for the actual material error.