Lemma U: time slices of space-time integrable functions

Fubini bookkeeping for the space-time cell (0,1) × (0,1)²: integrals over timeCube are iterated interval/cell integrals, the slice integral is interval integrable, and a.e. time slice of an integrable function is integrable.

theorem AVenhance.Infra.FullTheorem.LemmaU.timeCube_measure_eq_product : MeasureTheory.volume.restrict timeCube = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.FullTheorem.LemmaU.timeMeasure_Ioo_eq_Ioc : MeasureTheory.volume.restrict (Set.Ioo 0 1) = MeasureTheory.volume.restrict (Set.Ioc 0 1)

theorem AVenhance.Infra.FullTheorem.LemmaU.integral_timeCube_eq_interval_cell {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, F p = ∫ (t : ℝ) in 0..1, ∫ (x : Homogenization.Vec 2) in unitCube, F (t, x)

theorem AVenhance.Infra.FullTheorem.LemmaU.intervalIntegrable_cell_of_timeCube {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : IntervalIntegrable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, F (t, x)) MeasureTheory.volume 0 1

theorem AVenhance.Infra.FullTheorem.LemmaU.section_integrable_ae {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc 0 1), MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => F (t, x)) (MeasureTheory.volume.restrict unitCube)

A.e. time slice of a space-time integrable function is integrable on the cell.