Iterates Gradient Coordinate Material

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_gradient_coordinate_material_pairing_integrable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u v : ℝ → Homogenization.Vec 2 → ℝ} {q : ℝ → ℝ} (hb : ContinuousOn (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hq : ContinuousOn (fun (z : AmnrSpace) => q z.1) (Set.Ici 0 ×ˢ Set.univ)) (j k : Fin 2) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => q z.1 * spaceGrad (u z.1) z.2 j * amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (v t) x k) z.1 z.2) timeCube MeasureTheory.volume

Coordinate material pairings inherit integrability directly from the C1 scalar gradient carriers and the continuous primitive entry.