Iterates Actual Half Square Bound

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_actual_hessian_half_square_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm : ℝ} (hm : 1 ≤ m) (hκm : 0 < κm) {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t)) (w : List (Fin 2)) {D G M T s : ℝ} (hD : 0 ≤ D) (hG : 0 ≤ G) (hM : 0 ≤ M) (hs : 0 ≤ s) (hs1 : s ≤ 1) (hQb : ∀ (t : ℝ) (j k : Fin 2), |iterateKmatPrimitive I κm m t j k| ≤ D) (hE : ∀ (j k : Fin 2), ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, iterateSpatialWord (j :: k :: w) (u z.1) z.2 ^ 2 ≤ G ^ 2) (hME : ∀ (j k : Fin 2), ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, amnrMaterial (streamVel (Φ (m - 1))) (fun (t : ℝ) => iterateSpatialWord (j :: k :: w) (u t)) z.1 z.2 ^ 2 ≤ M ^ 2) (hTE : ∀ (j k : Fin 2), l2NormSq (iterateSpatialWord (j :: k :: w) (u s)) ≤ T ^ 2) : |∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ j : Fin 2, ∑ k : Fin 2, (I.Kmat κm m t j k - timeAvgMat (I.Kmat κm m) j k) * iterateSpatialWord (j :: k :: w) (u t) x) * ∑ j : Fin 2, ∑ k : Fin 2, iterateKmatPrimitive I κm m t j k * iterateSpatialWord (j :: k :: w) (u t) x| ≤ 8 * D ^ 2 * T ^ 2 + 16 * D ^ 2 * M * G

The first-increment oscillatory pairing uses the actual K primitive and actual Hessian, with both material and terminal energies explicitly retained.