Iterates Matrix Material Pairing

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_matrix_material_pairing_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hQ : ∀ (j k : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => Q z.1 j k) (Set.Ici 0 ×ˢ Set.univ)) (hH : ∀ (j k : Fin 2), ContDiffOn ℝ 1 (fun (z : AmnrSpace) => H z.1 z.2 j k) (Set.Ici 0 ×ˢ Set.univ)) {D G M 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 b (fun (t : ℝ) (x : Homogenization.Vec 2) => H t x j k) z.1 z.2 ^ 2 ≤ M ^ 2) : |∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ j : Fin 2, ∑ k : Fin 2, Q t j k * amnrMaterial b (fun (r : ℝ) (y : Homogenization.Vec 2) => H r y j k) t x) * ∑ j : Fin 2, ∑ k : Fin 2, Q t j k * H t x j k| ≤ 16 * D ^ 2 * M * G

The material contraction pairs linearly with the Hessian contraction on every terminal cell, using full nonnegative component energies.