Integrability of the actual energy pairings, including the initial boundary.

theorem AVenhance.Infra.Section4.amnr_time_cell_product_integrable {g : AmnrSpace → ℝ} (hg : ContinuousOn g (Set.Ici 0 ×ˢ Set.univ)) {T : ℝ} (hT : 0 ≤ T) : MeasureTheory.Integrable g ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))

A field continuous up to the initial time is integrable on every bounded physical time-cell product. The actual open spatial cell is retained.