Scalar matrix-contraction energies with exact four-component accounting.

theorem AVenhance.Infra.Section4.iterate_matrix_contraction_l2_bound (Q : Matrix (Fin 2) (Fin 2) ℝ) {H : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hH : ∀ (j k : Fin 2), Continuous fun (x : Homogenization.Vec 2) => H x j k) {D G : ℝ} (hD : 0 ≤ D) (hQ : ∀ (j k : Fin 2), |Q j k| ≤ D) (hE : ∀ (j k : Fin 2), (l2NormSq fun (x : Homogenization.Vec 2) => H x j k) ≤ G ^ 2) : (l2NormSq fun (x : Homogenization.Vec 2) => ∑ j : Fin 2, ∑ k : Fin 2, Q j k * H x j k) ≤ (4 * D * G) ^ 2

Actual continuous matrix entries have a terminal contraction energy bound.

theorem AVenhance.Infra.Section4.iterate_matrix_contraction_spacetime_energy_bound {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} {H : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hQ : ∀ (j k : Fin 2), ContinuousOn (fun (z : AmnrSpace) => Q z.1 j k) (Set.Ici 0 ×ˢ Set.univ)) (hH : ∀ (j k : Fin 2), ContinuousOn (fun (z : AmnrSpace) => H z.1 z.2 j k) (Set.Ici 0 ×ˢ Set.univ)) {D G : ℝ} (hD : 0 ≤ D) (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) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, (∑ j : Fin 2, ∑ k : Fin 2, Q z.1 j k * H z.1 z.2 j k) ^ 2 ≤ (4 * D * G) ^ 2

The same entrywise accounting applies to the actual full time cell.