RelativeError: periodic integration by parts for the Piola vector

theorem AVenhance.Infra.Section5.RelativeError.integral_unitCell_scalar_mul_vecDiv {f : Homogenization.Vec 2 → ℝ} {W : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContDiff ℝ 1 f) (hW : ContDiff ℝ 1 W) (hfp : IsZ2Periodic f) (hWp : ∀ (i : Fin 2), IsZ2Periodic fun (x : Homogenization.Vec 2) => W x i) : ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, f x * vecDiv W x = -∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad f x) (W x)

Periodic integration by parts transfers divergence from a smooth vector field to a smooth scalar function on the unit cell.