Iterates Homogeneous Previous Material

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_homogeneous_terminal_previous_material_squared_gain {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} {v₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) v₀ v) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hQc : ContinuousOn (fun (z : AmnrSpace) => Q z.1) (Set.Ici 0 ×ˢ Set.univ)) {B N r L Cv Cs D q s : ℝ} (hB : 0 ≤ B) (hr : 0 ≤ r) (hCv : 0 ≤ Cv) (hκ : 0 < κ) (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hvelocity : B * r ≤ Cv * κ * L ^ 2) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2) (p : List (Fin 2)), 1 ≤ p.length → ∀ (j : Fin 2), |iterateSpatialWord p (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ B * ↑p.length.factorial * r ^ p.length) (hE : ∀ (p : List (Fin 2)), p.length ≤ w.length + 2 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (v t))) ≤ (N / √κ) ^ 2 * (↑p.length.factorial * L ^ p.length) ^ 2) (hD : 0 ≤ D) (hCs : 0 ≤ Cs) (hq : 0 ≤ q) (hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ D) (hscale : D * L ^ 2 ≤ Cs * q) (hs1 : s ≤ 1) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) ((Q z.1).mulVec (spaceGrad (amnrMaterial b (fun (t : ℝ) => iterateSpatialWord w (v t)) z.1) z.2))| ≤ (κ / 24 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))) + 24 * Cs ^ 2 * (8 + 544 * Cv ^ 2) * q ^ 2 * N ^ 2 * (↑(w.length + 2).factorial * L ^ w.length) ^ 2

The actual homogeneous PDE supplies the exceptional first previous-material term at q squared from conditional scalar analytic energies.