Actual increment material-error gradient energy under the stream-regularity estimates.

theorem AVenhance.Infra.Section4.iterate_increment_error_gradient_energy_bound_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hm : 2 ≤ m) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (i : ℕ) (hi : i ≤ Nstar β) (w : List (Fin 2)) {G L : ℝ} (hL : 0 < L) (hg : 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹ / L) ^ 2 ≤ 1 / 2) (hE : ∀ (q : List (Fin 2)), q.length ≤ w.length → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (iterateIncrement T i t))) ≤ G ^ 2 * (↑(q.length + 2 * i).factorial * L ^ q.length) ^ 2) : (spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => iterateWordMaterialError (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) w (fun (z : AmnrSpace) => iterateIncrement T i z.1 z.2) (t, y)) x) ≤ 136 * (8192 * a β I.Λ (m - 1) * epsilon β I.Λ (m - 1)) ^ 2 * (256 * (epsilon β I.Λ (m - 1))⁻¹) ^ 2 * G ^ 2 * (↑(w.length + 1 + 2 * i).factorial * L ^ w.length) ^ 2

The stream-regularity estimates and actual lower increment gradients imply the all-order material-error gradient estimate. No material energy estimate is assumed.