Natural continuity and integrability of actual matrix pairings.

theorem AVenhance.Infra.Section4.iterate_matrix_pairing_continuousOn {a b : AmnrSpace → Homogenization.Vec 2} {A : AmnrSpace → Matrix (Fin 2) (Fin 2) ℝ} {S : Set AmnrSpace} (ha : ContinuousOn a S) (hb : ContinuousOn b S) (hA : ContinuousOn A S) : ContinuousOn (fun (z : AmnrSpace) => Homogenization.vecDot (a z) ((A z).mulVec (b z))) S

Actual vector and matrix continuity give joint pairing continuity.

theorem AVenhance.Infra.Section4.iterate_matrix_pairing_integrable {a b : AmnrSpace → Homogenization.Vec 2} {A : AmnrSpace → Matrix (Fin 2) (Fin 2) ℝ} (ha : ContinuousOn a (Set.Ici 0 ×ˢ Set.univ)) (hb : ContinuousOn b (Set.Ici 0 ×ˢ Set.univ)) (hA : ContinuousOn A (Set.Ici 0 ×ˢ Set.univ)) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => Homogenization.vecDot (a z) ((A z).mulVec (b z))) timeCube MeasureTheory.volume

Natural timeCube integrability requires no quantitative pairing bound.