All-order forcing-gradient energy from preceding L2 gradient energies.

theorem AVenhance.Infra.Section4.iterate_word_forcing_energy_bound {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hA : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (A t)) (hcoef : ∀ (r : List (Fin 2)), ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (A z.1) r z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (D E : ℕ → ℝ) (hD : ∀ (t : ℝ) (x : Homogenization.Vec 2) (r : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (A t) r x j k| ≤ D r.length) (hE : ∀ (r : List (Fin 2)), r.length ≤ w.length + 2 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord r (v t))) ≤ E r.length) (hFI : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A z.1 y).mulVec (spaceGrad (v z.1) y))) z.2)) timeCube MeasureTheory.volume) : (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A t y).mulVec (spaceGrad (v t) y)))) ≤ 64 * ∑ j ∈ Finset.range (w.length + 3), ↑((w.length + 2).choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length + 2 - j)

Integrate the explicit forcing-gradient expansion. The only quantitative scalar premise concerns the preceding field's actual gradient energies.