Natural energy integrability follows from actual smoothness up to time zero. Within derivatives provide continuous representatives at the initial boundary.

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

Continuous fields on the closed nonnegative-time domain are integrable on every bounded time interval times the torus cell.

theorem AVenhance.Infra.Section4.iterate_smooth_energy_integrability {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) {T : ℝ} (hT : 0 ≤ T) : MeasureTheory.Integrable (fun (p : AmnrSpace) => u p.1 p.2 * deriv (fun (s : ℝ) => u s p.2) p.1) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube)) ∧ IntervalIntegrable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (spaceGrad (u t) x)) MeasureTheory.volume 0 T

Both the actual time-energy pairing and Dirichlet energy are integrable. The ordinary time derivative is only identified at positive times, which suffices on uIoc(0,T); no ambient derivative at zero is required.