RelativeError: Piola data for the inverse flow #
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_contDiff_three
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : Flow.SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlow b X)
(t : ℝ)
:
ContDiff ℝ 3 fun (z : Homogenization.Vec 2) => X 0 z t
A fixed inverse-flow map is jointly smooth in its spatial variable to the order needed for the Piola transform.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_cofactorPiolaData
{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)
(t : ℝ)
(x : Homogenization.Vec 2)
:
have Y := fun (z : Homogenization.Vec 2) => X 0 z t;
(∀ (j : Fin 2),
∑ i : Fin 2,
(fderiv ℝ
(fun (z : Homogenization.Vec 2) =>
FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix Y z) i j)
x)
(Homogenization.basisVec i) = 0) ∧ ∀ (j k : Fin 2),
∑ i : Fin 2,
FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix Y x) i j * (fderiv ℝ Y x) (Homogenization.basisVec i) k = if j = k then 1 else 0
The inverse flow Jacobian supplies both Piola identities: its cofactor columns have zero divergence, and the cofactor times the inverse Jacobian is the identity.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_forwardJacobian_eq_cofactor
{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)
(t : ℝ)
(x : Homogenization.Vec 2)
:
FaaDiBruno.spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X t y 0) (X 0 x t) = FaaDiBruno.flowMatrixCofactorTranspose
(FaaDiBruno.spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X 0 y t) x)
The forward Jacobian at the transported point is exactly the cofactor
matrix used in inverseFlow_cofactorPiolaData.