Spatial periodicity of the actual pulled flow Jacobian.

theorem AVenhance.Infra.Section4.amnr_fderiv_periodic_of_equivariant {X : Homogenization.Vec 2 → Homogenization.Vec 2} (hX : Differentiable ℝ X) (he : ∀ (k : Fin 2 → ℤ) (x : Homogenization.Vec 2), X (x + latticeShift k) = X x + latticeShift k) : IsZ2Periodic (fderiv ℝ X)

Differentiating lattice equivariance makes the derivative periodic.

theorem AVenhance.Infra.Section4.amnr_xFlow_lattice_equivariant {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (k : Fin 2 → ℤ) (x : Homogenization.Vec 2) : I.xFlow hΦ m l t (x + latticeShift k) = I.xFlow hΦ m l t x + latticeShift k

Both actual flow maps are lattice equivariant by uniqueness of their integral curves; the inverse uses the reversed time arguments.

theorem AVenhance.Infra.Section4.amnr_xFlowInv_lattice_equivariant {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (k : Fin 2 → ℤ) (x : Homogenization.Vec 2) : I.xFlowInv hΦ m l t (x + latticeShift k) = I.xFlowInv hΦ m l t x + latticeShift k

theorem AVenhance.Infra.Section4.amnr_flowGrad_spatial_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (i j : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => I.flowGrad hΦ m l t x i j

Pulling the periodic derivative through the equivariant inverse preserves periodicity, with the row/column convention.