Continuity in time of unit-cell integrals of jointly continuous integrands on (0,∞)

theorem AVenhance.Infra.Section5.Integration.Energy.unitCell_ae_eq_closedCube : Torus.unitCell 2 =ᵐ[MeasureTheory.volume] Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

The unit cell is a null-set perturbation of the closed unit square.

theorem AVenhance.Infra.Section5.Integration.Energy.continuousOn_integral_unitCell_Ioi {H : ℝ → Homogenization.Vec 2 → ℝ} (hH : ContinuousOn (Function.uncurry H) (Set.Ioi 0 ×ˢ Set.univ)) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, H t x) (Set.Ioi 0)

Unit-cell integrals of integrands jointly continuous on (0,∞) × ℝ² are continuous in time on (0,∞).