Matrix Young allocation on each actual terminal-time cell.

theorem AVenhance.Infra.Section4.iterate_spacetime_matrix_absolute_integral_bound {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {ρ D : ℝ} (hρ : 0 < ρ) (hA : ∀ (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2), |A t x i j| ≤ D) (ha : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (a p.1 p.2)) timeCube MeasureTheory.volume) (hb : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (b p.1 p.2)) timeCube MeasureTheory.volume) (hp : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (a p.1 p.2) ((A p.1 p.2).mulVec (b p.1 p.2))) timeCube MeasureTheory.volume) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, |Homogenization.vecDot (a p.1 p.2) ((A p.1 p.2).mulVec (b p.1 p.2))| ≤ ρ * spaceTimeGradNormSq a + D ^ 2 / ρ * spaceTimeGradNormSq b

Matrix Young control on the space-time cell.

theorem AVenhance.Infra.Section4.iterate_truncated_matrix_pairing_bound {s : ℝ} (hs1 : s ≤ 1) {A : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {a b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {ρ D : ℝ} (hρ : 0 < ρ) (hA : ∀ (t : ℝ) (x : Homogenization.Vec 2) (i j : Fin 2), |A t x i j| ≤ D) (ha : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (a p.1 p.2)) timeCube MeasureTheory.volume) (hb : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (b p.1 p.2)) timeCube MeasureTheory.volume) (hp : MeasureTheory.IntegrableOn (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (a p.1 p.2) ((A p.1 p.2).mulVec (b p.1 p.2))) timeCube MeasureTheory.volume) : |∫ (p : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (a p.1 p.2) ((A p.1 p.2).mulVec (b p.1 p.2))| ≤ ρ * spaceTimeGradNormSq a + D ^ 2 / ρ * spaceTimeGradNormSq b

Every terminal signed matrix pairing has the full nonnegative Young budget.