RelativeError: periodicity of the transported Piola vector

theorem AVenhance.Infra.Section5.RelativeError.inverseFlow_piolaVector_periodic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {f : Homogenization.Vec 2 → ℝ} (hper : IsZ2Periodic f) (t : ℝ) : IsZ2Periodic fun (x : Homogenization.Vec 2) => Matrix.mulVec (FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X 0 y t) x)) (spaceGrad f (X 0 x t))

The Piola vector formed from an inverse-flow Jacobian and a periodic gradient remains lattice-periodic.