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

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

Fractional Poincare estimate from the exact overlap norm

The depth-zero term of the exact overlapping p = q = 2 Besov seminorm is the normalized L² fluctuation on the root cube. Combining this observation coordinatewise with the Hilbert-valued L² triangle inequality proves the fractional Poincare estimate directly, without importing a Sobolev embedding.

theorem HCPolySupport.exactOverlapEuclideanIntegrable_of_euclidean_memLp {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) 2 (normalizedCubeMeasure Q)) : ExactOverlapEuclideanIntegrable Q F

A concrete Euclidean L² fact on a triadic cube supplies all coordinate integrability certificates required by the exact overlap kernel.

noncomputable def HCPolySupport.exactOverlapRootMeanVec {d : ℕ} (Q : TriadicCube d) (F : Vec d → Vec d) (hF : ExactOverlapEuclideanIntegrable Q F) : Vec d

The vector of certified normalized coordinate means of F on the root cube Q.

Equations

• HCPolySupport.exactOverlapRootMeanVec Q F hF i = HCPolySupport.exactOverlapRootMean Q (fun (x : HCPolySupport.Vec d) => F x i) ⋯

theorem HCPolySupport.exactOverlapRootWeight_mul_eLpNorm_le_exactOverlapEuclideanNormTwo {d : ℕ} (s : ↑(Set.Ioo 0 1)) (Q : TriadicCube d) (F : Vec d → Vec d) (hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) 2 (normalizedCubeMeasure Q)) : have hI := ⋯; exactOverlapRootWeight Q ↑s * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (F x)) 2 (normalizedCubeMeasure Q) ≤ exactOverlapEuclideanNormTwo s Q F hI

The root-weighted normalized Euclidean L² norm is controlled by the exact Euclidean overlap full norm.

theorem HCPolySupport.UnitCubeEuclideanL2Field.exactOverlapEuclideanIntegrable {d : ℕ} (F : UnitCubeEuclideanL2Field d) : ExactOverlapEuclideanIntegrable (originCube d 0) F.toField

The canonical exact-overlap integrability certificate carried by a Euclidean L² field on the centered unit cube.

theorem HCPolySupport.unitCube_normalizedEuclideanLpENorm_le_exactOverlapEuclideanNormTwo {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ≤ exactOverlapEuclideanNormTwo s (originCube d 0) F.toField ⋯

On the centered unit cube, the exact overlap full norm controls the source-facing normalized Euclidean L² norm with constant exactly one.