Iterates Actual First Commuted Current

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_actual_first_commuted_current_material_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hNstar : 1 ≤ Nstar β) {m : ℕ} {κm κ : ℝ} (hm : 1 ≤ m) (hκm : 0 < κm) (hκ : 0 < κ) {θprev : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol (streamVel (Φ (m - 1))) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) u₀ θprev) {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κ u₀ θprev T) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => streamVel (Φ (m - 1)) z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) {B N r L C Ccoef D ρ q s : ℝ} (hB : 0 ≤ B) (hN : 0 ≤ N) (hr : 0 ≤ r) (hC : 0 ≤ C) (hD : 0 ≤ D) (hq : 0 < q) (hρ : 0 ≤ ρ) (hρq : ρ ≤ q) (hL : 0 < L) (hs : 0 ≤ s) (hs1 : s ≤ 1) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hscale : B * r ≤ C * κ * L ^ 2) (hQb : ∀ (t : ℝ) (j k : Fin 2), |iterateKmatPrimitive I κm m t j k| ≤ D) (hQscale : D * L ^ 2 ≤ C * q) (hjet : ∀ (j k : Fin 2) (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length)) (iterateSpatialSplits (j :: k :: w)), ∀ (a : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y a) x| ≤ B * ↑p.1.length.factorial * r ^ p.1.length) (hE : ∀ (v : List (Fin 2)), v.length ≤ w.length + 3 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord v (θprev t))) ≤ (N / √κ) ^ 2 * (↑v.length.factorial * L ^ v.length) ^ 2) (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) - κ • 1 + I.sMat hΦ m κm t y) v x j k| ≤ κ * (Ccoef * ρ) * ↑v.length.factorial * r ^ v.length) (hTE : ∀ (j k : Fin 2), l2NormSq (iterateSpatialWord (j :: k :: w) (θprev s)) ≤ (N * ↑(w.length + 2).factorial * L ^ (w.length + 2)) ^ 2) {Gcur : ℝ} (hGc : 0 ≤ Gcur) (d : ℕ → ℝ) (hd : ∀ (n : ℕ), 0 ≤ d n) (hvel : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w), ∀ (j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => streamVel (Φ (m - 1)) t y j) x| ≤ B * ↑p.1.length.factorial * r ^ p.1.length) (hcur : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (iterateIncrement T 1 t))) ≤ (Gcur * ↑(p.2.length + 2).factorial * L ^ p.2.length * d p.2.length) ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (amnrMaterial (streamVel (Φ (m - 1))) (fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T 1 t)) z.1) z.2) ((iterateKmatPrimitive I κm m z.1).mulVec (spaceGrad (iterateSpatialWord w (θprev z.1)) z.2))| ≤ (κ / 24 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (iterateIncrement T 1 t))) + (96 * C ^ 2 + (8 + 32 * √(8 + 64 * C ^ 2)) * C ^ 2 + 1 + 128 * C ^ 2 * Ccoef ^ 2) * q ^ 2 * (N * ↑(w.length + 2).factorial * L ^ w.length) ^ 2 + 8 * D * B * (N / √κ) * Gcur * r * (↑(w.length + 2).factorial * L ^ w.length) ^ 2 * ∑ k ∈ Finset.range w.length, (1 / 2) ^ k * d (w.length - 1 - k)