Coarse-graining support: Support.Sobolev.CubeEmbedding.FoldNormFiniteP #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Finite-p norm transport under the even fold #
This module upgrades the exact L² transport in FoldNorm to every finite
exponent used by the W^{1,p} development. The measure transport itself
remains lintegral_foldComp; only the outer p-th root is new here.
theorem
HCPolySupport.eLpNorm_foldComp_finiteLp
{d : ℕ}
{v : Vec d → ℝ}
(p : FiniteLpExponent)
(hv : Measurable v)
(lo hi : Vec d)
(hlt : ∀ (k : Fin d), lo k < hi k)
:
MeasureTheory.eLpNorm (fun (x : Vec d) => v (Fold lo hi x)) p.exponent (MeasureTheory.volume.restrict (Box3 lo hi)) = (3 ^ d) ^ (1 / p.exponent.toReal) * MeasureTheory.eLpNorm v p.exponent (MeasureTheory.volume.restrict (Box lo hi))
Exact finite-p norm transport for composition with the coordinatewise
even fold.
theorem
HCPolySupport.eLpNorm_foldComp_mul_foldSign_le_finiteLp
{d : ℕ}
{D : Vec d → ℝ}
(p : FiniteLpExponent)
(hD : Measurable D)
(lo hi : Vec d)
(hlt : ∀ (k : Fin d), lo k < hi k)
(i : Fin d)
:
A coordinate derivative transported by the fold, including its reflection
sign, has no larger finite-p norm than the exactly scaled original field.