Iterates Terminal Previous Material

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_previous_material_pairing_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u v : ℝ → Homogenization.Vec 2 → ℝ} {v₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F 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)) (hFc : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (F z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ)) {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hQc : ContinuousOn (fun (z : AmnrSpace) => Q z.1) (Set.Ici 0 ×ˢ Set.univ)) {D s : ℝ} (hQ : ∀ (t : ℝ) (j k : Fin 2), |Q t j k| ≤ D) (hκ : 0 < κ) (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 * D ^ 2 / κ * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (amnrMaterial b (fun (s : ℝ) => iterateSpatialWord w (v s)) t)

The previous material-gradient term receives current dissipation by Young's inequality. Its natural integrability follows from the actual PDE.