RelativeError: the transported Laplacian pairing as a Piola pairing #
theorem
AVenhance.Infra.Section5.RelativeError.classicalSpaceLap_contDiff_three
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ 3 f)
:
theorem
AVenhance.Infra.Section5.RelativeError.classicalSpaceLap_periodic
{f : Homogenization.Vec 2 → ℝ}
(hper : IsZ2Periodic f)
:
IsZ2Periodic (spaceLap f)
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_piolaVector_contDiff_infty
{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 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(t : ℝ)
:
ContDiff ℝ ↑⊤ 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 inverse-flow Piola vector made from a smooth potential is smooth in space.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_piolaVector_continuous
{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 → ℝ}
(hf : ContDiff ℝ 3 f)
(t : ℝ)
:
Continuous 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))
Continuity of the Piola vector only needs three derivatives of the scalar potential; the full smoothness theorem above is used when the potential is smooth.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_laplacian_pairing_eq_piola
{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)
{u₀ f : Homogenization.Vec 2 → ℝ}
(hu : ContDiff ℝ 1 u₀)
(huper : IsZ2Periodic u₀)
(hf : ContDiff ℝ (↑⊤) f)
(hfper : IsZ2Periodic f)
(t : ℝ)
:
∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u₀ x * inverseFlowTransportTest X t x = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (spaceGrad u₀ x)
(Matrix.mulVec
(FaaDiBruno.flowMatrixCofactorTranspose
(FaaDiBruno.spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X 0 y t) x))
(spaceGrad f (X 0 x t)))
The transported test with initial value -Δf is the negative divergence
of the inverse-flow Piola vector. Pairing it against a periodic scalar and
integrating by parts gives an exact gradient pairing.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_laplacianTransport_contDiff_infty
{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 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
:
ContDiff ℝ (↑⊤) (Function.uncurry (inverseFlowTransportTest X))
The transported Laplacian test is jointly smooth when its datum is smooth; the periodicity of its initial datum follows from the periodic Laplacian.
theorem
AVenhance.Infra.Section5.RelativeError.integral_unitCell_vecDot_abs_le
{F G : Homogenization.Vec 2 → Homogenization.Vec 2}
(hF : Continuous F)
(hG : Continuous G)
:
|∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecDot (F x) (G x)| ≤ √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (F x)) * √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (G x))
Cauchy--Schwarz on the periodic cell for the Euclidean vector energy
vecNormSq, despite Vec itself carrying the coordinate sup norm.