Cross temporal pairings inherit integrability from the actual C1 carrier.

theorem AVenhance.Infra.Section4.iterate_time_cross_pairing_integrable {u v : ℝ → Homogenization.Vec 2 → ℝ} (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)) {T : ℝ} (hT : 0 ≤ T) : MeasureTheory.Integrable (fun (z : AmnrSpace) => u z.1 z.2 * deriv (fun (s : ℝ) => v s z.2) z.1) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))

Natural temporal cross-pairing integrability requires only continuity of the first factor and C1 up to zero of the differentiated factor.

theorem AVenhance.Infra.Section4.iterate_material_cross_pairing_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)) {T : ℝ} (hT : 0 ≤ T) : MeasureTheory.Integrable (fun (z : AmnrSpace) => u z.1 z.2 * amnrMaterial b v z.1 z.2) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod (MeasureTheory.volume.restrict unitCube))

Material cross-pairing integrability follows from the same within-derivative representative and the actual continuous drift.