Iterates Half Square Bound

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_material_half_square_bound {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hQ : ∀ (j k : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => Q z.1 j k) (Set.Ici 0 ×ˢ Set.univ)) (hQd : ∀ (j k : Fin 2), Continuous fun (t : ℝ) => deriv (fun (r : ℝ) => Q r j k) t) (hH : ∀ (j k : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => H z.1 z.2 j k) (Set.Ici 0 ×ˢ Set.univ)) (hHs : ∀ (t : ℝ), 0 < t → ∀ (j k : Fin 2), ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => H t x j k) (hHp : ∀ (t : ℝ), 0 < t → ∀ (j k : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => H t x j k) (hQ0 : ∀ (j k : Fin 2), Q 0 j k = 0) {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), |Q t j k| ≤ D) (hE : ∀ (j k : Fin 2), ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, H z.1 z.2 j k ^ 2 ≤ G ^ 2) (hME : ∀ (j k : Fin 2), ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, amnrMaterial (streamVel φ) (fun (t : ℝ) (x : Homogenization.Vec 2) => H t x j k) z.1 z.2 ^ 2 ≤ M ^ 2) (hTE : ∀ (j k : Fin 2), (l2NormSq fun (x : Homogenization.Vec 2) => H s x j k) ≤ T ^ 2) : |∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ j : Fin 2, ∑ k : Fin 2, deriv (fun (r : ℝ) => Q r j k) t * H t x j k) * ∑ j : Fin 2, ∑ k : Fin 2, Q t j k * H t x j k| ≤ 8 * D ^ 2 * T ^ 2 + 16 * D ^ 2 * M * G

Quantitative transported half-square with its terminal boundary retained. The primitive bound and actual scalar component energies are the only sizes.