Iterates Actual Small Remainder Flux

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_mean_correction_small_flux_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 v : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (a : ℕ) {C B ρ r L s : ℝ} (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hs1 : s ≤ 1) (hcoef : ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : 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) p x j k| ≤ κprev * C * ρ * ↑p.length.factorial * r ^ p.length) (hE : ∀ p ∈ iterateSpatialSplits w, (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ B ^ 2 * (↑(p.2.length + a).factorial * L ^ p.2.length) ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateWordFlux (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm z.1 y) (v z.1) w z.2)| ≤ (κprev / 8 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) + 32 * κprev * C ^ 2 * ρ ^ 2 * B ^ 2 * (↑(w.length + a).factorial * L ^ w.length) ^ 2

Actual mean and flow coefficient jets yield the uniformly small terminal remainder flux. No bound on the forcing pairing is assumed.