Iterates Boundary Squared Gain

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_word_boundary_squared_gain {u v : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) (w : List (Fin 2)) (a : ℕ) (Q : Matrix (Fin 2) (Fin 2) ℝ) {D L Cs q B : ℝ} (hD : 0 ≤ D) (hL : 0 < L) (hCs : 0 ≤ Cs) (hq : 0 ≤ q) (hQ : ∀ (j k : Fin 2), |Q j k| ≤ D) (hscale : D * L ^ 2 ≤ Cs * q) (hE : ∀ (j k : Fin 2), l2NormSq (iterateSpatialWord (j :: k :: w) v) ≤ B ^ 2 * (↑(w.length + 2 + a).factorial * L ^ (w.length + 2)) ^ 2) : |∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (iterateSpatialWord w u) x) (Q.mulVec (spaceGrad (iterateSpatialWord w v) x))| ≤ l2NormSq (iterateSpatialWord w u) / 4 + 16 * Cs ^ 2 * q ^ 2 * B ^ 2 * (↑(w.length + 2 + a).factorial * L ^ w.length) ^ 2

The terminal boundary pairing has a quarter of the current scalar energy and a squared primitive gain on the preceding two-higher scalar order.