Iterates Actual Terminal Inequality

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_increment_terminal_word_energy_inequality {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t)) (hm : 1 ≤ m) (hκm : 0 < κm) (i : ℕ) (hi : i + 1 ≤ Nstar β) (w : List (Fin 2)) {s : ℝ} (hs : 0 ≤ s) : l2NormSq (iterateSpatialWord w (iterateIncrement T (i + 1) s)) / 2 + κprev * ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) z.1)) z.2) ≤ |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) z.1)) z.2) (iterateWordFlux (fun (y : Homogenization.Vec 2) => I.Kmat κm m z.1 - κprev • 1 + I.sMat hΦ m κm z.1 y) (iterateIncrement T i z.1) w z.2)| + |∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (iterateIncrement T (i + 1) z.1)) z.2) (iterateWordFlux (fun (y : Homogenization.Vec 2) => Φ (m - 1) z.1 y • sigmaMat) (iterateIncrement T (i + 1) z.1) w z.2)|