Iterates Cross Cell

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_material_cross_timeCube_integrable {u v : ℝ → 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 : ContinuousOn (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ 1 (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => u z.1 z.2 * amnrMaterial b v z.1 z.2) timeCube MeasureTheory.volume

The actual material cross pairing is integrable on the full open time cell.