Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapEuclideanComparison

Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapEuclideanComparison #

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

Exact Euclidean overlap Besov--Gagliardo comparison on centered cubes #

This module compares the source-facing Euclidean overlap seminorm with the literal physical Gagliardo seminorm on every centered triadic cube. The physical coordinate energy is kept over the physical product measure; scale uniformity follows because all comparison constants are dimension/order constants and do not depend on the centered-cube scale.

source
theorem HCPolySupport.CenteredCubeEuclideanL2Field.exactOverlapEuclideanIntegrable {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) :
ExactOverlapEuclideanIntegrable (originCube d m) F.toField

The canonical exact-overlap integrability certificate carried by a Euclidean L² field on an arbitrary centered triadic cube.

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

The physical finite-coordinate family of scalar ambient-distance Gagliardo seminorms, squared before summation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.centeredCubeEuclideanHs_numerator_eq_sum_coordinates {d : ℕ} {m : ℤ} (F : CenteredCubeEuclideanL2Field d m) (z : Vec d × Vec d) :
    ‖HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 = ∑ i : Fin d, (F.toField z.1 i - F.toField z.2 i) ^ 2

    The squared Euclidean numerator is the sum of the squared coordinate differences on every centered cube.

    source
    theorem HCPolySupport.centeredCubeEuclideanHsEnergy_zero_dim {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field 0 m) :
    centeredCubeEuclideanHsEnergy s F = 0

    Both physical energies vanish in dimension zero.

    source
    theorem HCPolySupport.centeredCubeCoordinateGagliardoEnergy_zero_dim {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field 0 m) :
    centeredCubeCoordinateGagliardoEnergy s F = 0

    The physical coordinate energy vanishes in dimension zero.

    source
    theorem HCPolySupport.centeredCubeEuclideanHsESeminorm_le_mul_exactOverlapEuclideanSeminormTwo {d : ℕ} {m : ℤ} [NeZero d] (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) :
    centeredCubeEuclideanHsESeminorm s F ≤ Gagliardo.gagliardoBesovLowerConstant d * exactOverlapEuclideanSeminormTwo s (originCube d m) F.toField ⋯

    The physical Euclidean Gagliardo seminorm is controlled by the exact Euclidean overlap seminorm, with no representative or integrability binder.

    source
    theorem HCPolySupport.exactOverlapEuclideanSeminormTwo_le_mul_centeredCubeEuclideanHsESeminorm {d : ℕ} {m : ℤ} [NeZero d] (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) :
    exactOverlapEuclideanSeminormTwo s (originCube d m) F.toField ⋯ ≤ (2 * 3 ^ d * ENNReal.ofReal (↑d ^ (↑d + 2 * ↑s))) ^ 2⁻¹ * centeredCubeEuclideanHsESeminorm s F

    The exact Euclidean overlap seminorm is controlled by the physical Euclidean Gagliardo seminorm. The explicit constant contains both the scalar overlap factor and the Euclidean/product-metric factor.

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

    One scale-independent constant for both directions of the physical Euclidean Gagliardo/exact-overlap comparison.

    Equations
    Instances For
      source
      theorem HCPolySupport.centeredCubeExactOverlapEuclideanComparisonConstant_lt_top (d : ℕ) (s : ↑FractionalOrder) :
      centeredCubeExactOverlapEuclideanComparisonConstant d s < ⊤

      The common physical comparison constant is finite.

      source
      theorem HCPolySupport.exists_centeredCubeEuclideanHs_exactOverlapEuclideanSeminormTwo_comparison (d : ℕ) [NeZero d] (s : ↑FractionalOrder) :
      ∃ C < ⊤, ∀ (m : ℤ) (F : CenteredCubeEuclideanL2Field d m), centeredCubeEuclideanHsESeminorm s F ≤ C * exactOverlapEuclideanSeminormTwo s (originCube d m) F.toField ⋯ ∧ exactOverlapEuclideanSeminormTwo s (originCube d m) F.toField ⋯ ≤ C * centeredCubeEuclideanHsESeminorm s F

      Uniform source-facing equivalence between the exact physical Euclidean Gagliardo seminorm and the exact Euclidean overlap Besov seminorm on every centered triadic cube. The finite constant is chosen before the scale and field, and all measurability, L², representative, and scalar-comparison obligations are discharged internally.