Iterates Hessian Component Energy

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_hessian_word_component_energy_bound {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (j k : Fin 2) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, iterateSpatialWord (j :: k :: w) (u z.1) z.2 ^ 2 ≤ spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord (k :: w) (u t))

An actual Hessian word uses the gradient energy of a one-shorter word.