Iterates Gradient Material Cross

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_flow_gradient_matrix_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (z : AmnrSpace) => gradMatrix (b z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

A smooth actual vector field has a jointly continuous spatial matrix gradient on the closed nonnegative-time domain.

theorem AVenhance.Infra.Section4.iterate_gradient_material_cross_timeCube_integrable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u v : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (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 ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (j : Fin 2) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => u z.1 z.2 * spaceGrad (amnrMaterial b v z.1) z.2 j) timeCube MeasureTheory.volume

Pairings with the actual gradient of a material derivative inherit integrability from the C1 material representative and the exact drift term.