Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspCongruence

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Almost-everywhere congruence for Euclidean fractional W^{s,p}

The Euclidean finite-exponent fractional kernel and its associated seminorm, membership predicate, and full power norm depend only on the normalized-cube almost-everywhere representative of the field.

theorem HCPolySupport.cubeEuclideanWspKernel_congr_ae {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F G : Vec d → Vec d} (hFG : F =ᵐ[normalizedCubeMeasure Q] G) : cubeEuclideanWspKernel s p F =ᵐ[Gagliardo.gagliardoCubeMeasure Q] cubeEuclideanWspKernel s p G

Modifying a Euclidean field on a normalized-cube null set modifies its fractional W^{s,p} kernel only on a Gagliardo product-measure null set.

theorem HCPolySupport.cubeEuclideanWspESeminorm_congr_ae {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F G : Vec d → Vec d} (hFG : F =ᵐ[normalizedCubeMeasure Q] G) : cubeEuclideanWspESeminorm Q s p F = cubeEuclideanWspESeminorm Q s p G

The Euclidean fractional W^{s,p} seminorm depends only on the normalized-cube almost-everywhere representative.

theorem HCPolySupport.memCubeEuclideanWsp_congr_ae {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F G : Vec d → Vec d} (hFG : F =ᵐ[normalizedCubeMeasure Q] G) : MemCubeEuclideanWsp Q s p F ↔ MemCubeEuclideanWsp Q s p G

Euclidean fractional W^{s,p} membership is invariant under normalized-cube almost-everywhere replacement.

theorem HCPolySupport.cubeEuclideanNormalizedLpENorm_congr_ae {d : ℕ} (Q : TriadicCube d) (p : ENNReal) {F G : Vec d → Vec d} (hFG : F =ᵐ[normalizedCubeMeasure Q] G) : (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm p F = (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm p G

The normalized Euclidean L^p term on a cube is invariant under normalized-cube almost-everywhere replacement.

theorem HCPolySupport.cubeEuclideanWspFullENorm_congr_ae {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F G : Vec d → Vec d} (hFG : F =ᵐ[normalizedCubeMeasure Q] G) : cubeEuclideanWspFullENorm Q s p F = cubeEuclideanWspFullENorm Q s p G

The Euclidean fractional full power norm depends only on the normalized-cube almost-everywhere representative.