RelativeError: Euclidean transport bounds without coordinate losses #
theorem
AVenhance.Infra.Section5.RelativeError.TraceEuclideanTransport.inverseFlow_derivative_short_euclidean_bound
{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)
{B T : ℝ}
(hB : 0 ≤ B)
(hBT : B * T ≤ 1)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
(x z : Homogenization.Vec 2)
:
Homogenization.vecNormSq ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X 0 y t) x) z) ≤ Real.exp 1 ^ 2 * Homogenization.vecNormSq z
theorem
AVenhance.Infra.Section5.RelativeError.TraceEuclideanTransport.forwardFlow_derivative_short_euclidean_bound
{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)
{B T : ℝ}
(hB : 0 ≤ B)
(hBT : B * T ≤ 1)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
(x z : Homogenization.Vec 2)
:
Homogenization.vecNormSq ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y 0) x) z) ≤ Real.exp 1 ^ 2 * Homogenization.vecNormSq z
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_transportedGradient_euclidean_pointwise_le
{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)
{B T : ℝ}
(hB : 0 ≤ B)
(hBT : B * T ≤ 1)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
{h₀ : Homogenization.Vec 2 → ℝ}
(hh₀ : ContDiff ℝ (↑⊤) h₀)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
(x : Homogenization.Vec 2)
:
Homogenization.vecNormSq (spaceGrad (inverseFlowTransportTest X t) x) ≤ Real.exp 1 ^ 2 * Homogenization.vecNormSq (spaceGrad h₀ (X 0 x t))
The gradient of the inverse-flow transported test has its exact Euclidean operator bound, with no coordinatewise matrix estimate.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_transportedGradient_euclidean_cellL2_bound
{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)
{B T : ℝ}
(hB : 0 ≤ B)
(hBT : B * T ≤ 1)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
{h₀ : Homogenization.Vec 2 → ℝ}
(hh₀ : ContDiff ℝ (↑⊤) h₀)
(hper : IsZ2Periodic h₀)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
:
∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad (inverseFlowTransportTest X t) x) ≤ Real.exp 1 ^ 2 * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad h₀ x)
Cell L² version of the Euclidean transported-gradient estimate.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_piolaVector_euclideanCellEnergy_sharp_bound
{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)
{B T : ℝ}
(hB : 0 ≤ B)
(hBT : B * T ≤ 1)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
{f : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ 3 f)
(hper : IsZ2Periodic f)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
:
∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq
(Matrix.mulVec
(FaaDiBruno.flowMatrixCofactorTranspose
(FaaDiBruno.spatialGradientMatrix (fun (y : Homogenization.Vec 2) => X 0 y t) x))
(spaceGrad f (X 0 x t))) ≤ Real.exp 1 ^ 2 * ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad f x)
The Piola vector has the same exact Euclidean cell-energy bound. Its cofactor representation equals the forward flow derivative applied to the initial gradient, and Liouville unfolds the cell integral.
theorem
AVenhance.Infra.Section5.RelativeError.inverseFlow_laplacian_pairing_abs_le_euclidean
{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)
{B T : ℝ}
(hB : 0 ≤ B)
(hBT : B * T ≤ 1)
(hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B)
{f u₀ : Homogenization.Vec 2 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(hfper : IsZ2Periodic f)
(hu : ContDiff ℝ 1 u₀)
(huper : IsZ2Periodic u₀)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
:
|∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, u₀ x * inverseFlowTransportTest X t x| ≤ √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad u₀ x)) * (Real.exp 1 * √(∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, Homogenization.vecNormSq (spaceGrad f x)))
Pairing u with the transported -Δf costs exactly e in Euclidean
gradient energy.