Linear L2 pairing estimates for actual commutator coefficient terms.

theorem AVenhance.Infra.Section4.iterate_truncated_coefficient_linear_pairing_bound {a g q : AmnrSpace → ℝ} {A G D s : ℝ} (hs1 : s ≤ 1) (ha : ContinuousOn a (Set.Ici 0 ×ˢ Set.univ)) (hg : ContinuousOn g (Set.Ici 0 ×ˢ Set.univ)) (hq : ContinuousOn q (Set.Ici 0 ×ˢ Set.univ)) (hA : 0 ≤ A) (hG : 0 ≤ G) (hD : 0 ≤ D) (hb : ∀ (z : AmnrSpace), |q z| ≤ D) (hEa : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, a z ^ 2 ≤ A ^ 2) (hEg : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, g z ^ 2 ≤ G ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, a z * (q z * g z)| ≤ D * A * G

Bounded coefficient multiplication preserves the linear product of the two L2 bounds. All natural integrability follows from actual continuity.