Iterates Analytic Matrix Forcing

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_analytic_matrix_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)) (a : ℕ) {κ C B b L : ℝ} (hL : 0 < L) (hg : 2 * (b / L) ^ 2 ≤ 1 / 2) (hD : ∀ (t : ℝ) (x : Homogenization.Vec 2) (r : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (A t) r x j k| ≤ κ * C * ↑r.length.factorial * b ^ r.length) (hE : ∀ (r : List (Fin 2)), r.length ≤ w.length + 2 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord r (v t))) ≤ B ^ 2 * (↑(r.length + a).factorial * L ^ r.length) ^ 2) : (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A t y).mulVec (spaceGrad (v t) y)))) ≤ 128 * κ ^ 2 * C ^ 2 * B ^ 2 * (↑(w.length + 2 + a).factorial * L ^ (w.length + 2)) ^ 2

An actual smooth matrix forcing has an analytic gradient budget from its literal coefficient jets and the preceding scalar gradient energies.