Iterates Actual First Remainder Pairing

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_actual_first_remainder_pairing_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} (hm : 1 ≤ m) (hκm : 0 < κm) (hκ : 0 < κprev) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) {N C Cscale D ρ q r L s : ℝ} (hs1 : s ≤ 1) (hL : 0 < L) (hD : 0 ≤ D) (hCscale : 0 ≤ Cscale) (hρ : 0 ≤ ρ) (hq : 0 < q) (hρq : ρ ≤ q) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hQb : ∀ (t : ℝ) (j k : Fin 2), |iterateKmatPrimitive I κm m t j k| ≤ D) (hQscale : D * L ^ 2 ≤ Cscale * q) (hcoef : ∀ (t : ℝ) (x : Homogenization.Vec 2) (v : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm t y) v x j k| ≤ κprev * (C * ρ) * ↑v.length.factorial * r ^ v.length) (hE : ∀ (v : List (Fin 2)), v.length ≤ w.length + 2 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord v (u t))) ≤ (N / √κprev) ^ 2 * (↑v.length.factorial * L ^ v.length) ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm z.1 y).mulVec (spaceGrad (u z.1) y))) z.2) ((iterateKmatPrimitive I κm m z.1).mulVec (spaceGrad (iterateSpatialWord w (u z.1)) z.2))| ≤ (1 + 128 * Cscale ^ 2 * C ^ 2) * q ^ 2 * (N * ↑(w.length + 2).factorial * L ^ w.length) ^ 2

The actual noncentered first-step forcing pairing has a q-squared budget. Its energy is derived from the literal mean/spatial matrix jets.