Spatial regularity of the pulled flow-gradient matrices in the Section 4 definitions.

theorem AVenhance.Infra.Section5.FlowGradientRegularity.gradMatrix_contDiff_one_of_contDiff_two {X : Homogenization.Vec 2 → Homogenization.Vec 2} (hX : ContDiff ℝ 2 X) : ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => gradMatrix X x

theorem AVenhance.Infra.Section5.FlowGradientRegularity.gradMatrix_contDiff_two_of_contDiff_three {X : Homogenization.Vec 2 → Homogenization.Vec 2} (hX : ContDiff ℝ 3 X) : ContDiff ℝ 2 fun (x : Homogenization.Vec 2) => gradMatrix X x

theorem AVenhance.Infra.Section5.flowGrad_spatial_contDiff_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => I.flowGrad hΦ m l t x

The pulled gradient matrix ∇X_l ∘ X_l⁻¹ is C¹ in the spatial variable, by the C² spatial regularity of both flow slices.

theorem AVenhance.Infra.Section5.flowGrad_spatial_contDiff_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : ContDiff ℝ 2 fun (x : Homogenization.Vec 2) => I.flowGrad hΦ m l t x

The pulled gradient matrix is C² in space, using C³ regularity of the forward and inverse flow slices.