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

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

Exact Euclidean overlap full-norm comparison on centered cubes

This module compares the source-facing exact overlap B^s_{2,2} full norm with the approved physical Euclidean H^s full norm on every centered triadic cube. Both objects use their canonical L² certificates, so the public API has no integrability, measurability, or certificate binder.

Main definitions

• centeredCubeExactOverlapEuclideanSeminormTwo: the canonical physical exact-overlap seminorm.
• centeredCubeExactOverlapEuclideanNormTwo: the canonical physical exact-overlap full norm.

Main results

• centeredCubeExactOverlapEuclideanRootMeanENorm_le_normalizedEuclideanLpENorm: the Euclidean root mean is bounded by the normalized Euclidean L² norm.
• exists_centeredCubeEuclideanHs_exactOverlapEuclideanNormTwo_comparison: one finite constant, fixed before scale and field, controls both full-norm comparison directions.

noncomputable def HCPolySupport.centeredCubeExactOverlapEuclideanSeminormTwo {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : ENNReal

The canonical exact Euclidean overlap seminorm on a centered cube.

Equations

• HCPolySupport.centeredCubeExactOverlapEuclideanSeminormTwo s F = HCPolySupport.exactOverlapEuclideanSeminormTwo s (HCPolySupport.originCube d m) F.toField ⋯

noncomputable def HCPolySupport.centeredCubeExactOverlapEuclideanNormTwo {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : ENNReal

The canonical exact Euclidean overlap full norm on a centered cube.

Equations

• HCPolySupport.centeredCubeExactOverlapEuclideanNormTwo s F = HCPolySupport.exactOverlapEuclideanNormTwo s (HCPolySupport.originCube d m) F.toField ⋯

theorem HCPolySupport.centeredCubeExactOverlapEuclideanSeminormTwo_eq {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeExactOverlapEuclideanSeminormTwo s F = exactOverlapEuclideanSeminormTwo s (originCube d m) F.toField ⋯

Evaluation of the canonical exact Euclidean overlap seminorm.

theorem HCPolySupport.centeredCubeExactOverlapEuclideanNormTwo_eq {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeExactOverlapEuclideanNormTwo s F = exactOverlapEuclideanNormTwo s (originCube d m) F.toField ⋯

Evaluation of the canonical exact Euclidean overlap full norm.

theorem HCPolySupport.centeredCubeExactOverlapEuclideanRootMeanENorm_le_normalizedEuclideanLpENorm {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) : exactOverlapEuclideanRootMeanENorm (originCube d m) F.toField ⋯ ≤ (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 F.toField

The Euclidean magnitude of the normalized root mean is bounded by the normalized Euclidean L² norm carried by the centered-cube field.

theorem HCPolySupport.centeredCubeRootWeight_mul_normalizedEuclideanLpENorm_le_exactOverlapNormTwo {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : exactOverlapRootWeight (originCube d m) ↑s * (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 F.toField ≤ centeredCubeExactOverlapEuclideanNormTwo s F

The root-weighted normalized Euclidean L² norm is controlled by the canonical exact-overlap full norm on every centered cube.

noncomputable def HCPolySupport.centeredCubeExactOverlapEuclideanFullComparisonConstant (d : ℕ) (s : ↑FractionalOrder) : ENNReal

One scale-independent constant for both directions of the exact-overlap and physical Euclidean fractional full-norm comparison.

Equations

• HCPolySupport.centeredCubeExactOverlapEuclideanFullComparisonConstant d s = 1 + HCPolySupport.centeredCubeExactOverlapEuclideanComparisonConstant d s

theorem HCPolySupport.centeredCubeExactOverlapEuclideanFullComparisonConstant_lt_top (d : ℕ) (s : ↑FractionalOrder) : centeredCubeExactOverlapEuclideanFullComparisonConstant d s < ⊤

The common exact-overlap/physical full-norm comparison constant is finite.

theorem HCPolySupport.centeredCubeExactOverlapEuclideanNormTwo_le_mul_centeredCubeEuclideanHsFullENorm {d : ℕ} {m : ℤ} [NeZero d] (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeExactOverlapEuclideanNormTwo s F ≤ centeredCubeExactOverlapEuclideanFullComparisonConstant d s * centeredCubeEuclideanHsFullENorm s F

The exact-overlap Euclidean full norm is bounded by the approved physical Euclidean fractional full norm, uniformly in the centered-cube scale.

theorem HCPolySupport.centeredCubeEuclideanHsFullENorm_le_mul_centeredCubeExactOverlapEuclideanNormTwo {d : ℕ} {m : ℤ} [NeZero d] (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsFullENorm s F ≤ centeredCubeExactOverlapEuclideanFullComparisonConstant d s * centeredCubeExactOverlapEuclideanNormTwo s F

The approved physical Euclidean fractional full norm is bounded by the exact-overlap Euclidean full norm, uniformly in the centered-cube scale.

theorem HCPolySupport.exists_centeredCubeEuclideanHs_exactOverlapEuclideanNormTwo_comparison (d : ℕ) [NeZero d] (s : ↑FractionalOrder) : ∃ C < ⊤, ∀ (m : ℤ) (F : CenteredCubeEuclideanL2Field d m), centeredCubeExactOverlapEuclideanNormTwo s F ≤ C * centeredCubeEuclideanHsFullENorm s F ∧ centeredCubeEuclideanHsFullENorm s F ≤ C * centeredCubeExactOverlapEuclideanNormTwo s F

Uniform source-facing equivalence between the exact-overlap Euclidean B^s_{2,2} full norm and the approved physical Euclidean H^s full norm on every centered triadic cube. The finite constant is chosen before scale and field, and all integrability and comparison obligations are internal.