RelativeError: divergence of the transported gradient potential

theorem AVenhance.Infra.Section5.RelativeError.TransportPiolaDivergence.spatialGradientMatrix_contDiff_one {Y : Homogenization.Vec 2 → Homogenization.Vec 2} (hY : ContDiff ℝ 2 Y) : ContDiff ℝ 1 (FaaDiBruno.spatialGradientMatrix Y)

theorem AVenhance.Infra.Section5.RelativeError.inverseFlow_cofactor_divergence_transform {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) {g : Homogenization.Vec 2 → Homogenization.Vec 2} (hg : ContDiff ℝ 1 g) (t : ℝ) (x : Homogenization.Vec 2) : have Y := fun (z : Homogenization.Vec 2) => X 0 z t; have Q := fun (z : Homogenization.Vec 2) => FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix Y z); vecDiv (fun (z : Homogenization.Vec 2) => Matrix.mulVec (Q z) (g (Y z))) x = vecDiv g (Y x)

The Piola vector built from the inverse-flow cofactor has divergence equal to the divergence of the original vector field at the inverse point.

theorem AVenhance.Infra.Section5.RelativeError.inverseFlow_transportLaplacian {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 3 f) (t : ℝ) (x : Homogenization.Vec 2) : have Y := fun (z : Homogenization.Vec 2) => X 0 z t; have Q := fun (z : Homogenization.Vec 2) => FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix Y z); vecDiv (fun (z : Homogenization.Vec 2) => Matrix.mulVec (Q z) (spaceGrad f (Y z))) x = spaceLap f (Y x)

For a scalar potential, the transported cofactor vector is a Piola representation of the pulled-back Laplacian.