Natural material-square integrability from actual initial-time carriers.

theorem AVenhance.Infra.Section4.iterate_material_square_time_integrable {u : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ 1 (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs : 0 ≤ s) : MeasureTheory.Integrable (fun (z : AmnrSpace) => amnrMaterial b u z.1 z.2 ^ 2) ((MeasureTheory.volume.restrict (Set.uIoc 0 s)).prod (MeasureTheory.volume.restrict unitCube))

The material square has a continuous within-derivative representative; no two-sided initial-time derivative is assumed.

theorem AVenhance.Infra.Section4.iterate_material_square_integrable {u : ℝ → Homogenization.Vec 2 → ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ 1 (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => amnrMaterial b u z.1 z.2 ^ 2) timeCube MeasureTheory.volume

Actual material squares are naturally integrable on the open cell.