Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.FullNormEquivalence

Coarse-graining support: Support.Sobolev.Fractional.ContinuousInterpolation.FullNormEquivalence #

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

Additive full-norm equivalence for continuous interpolation #

This module packages the approved source-facing convention: the normalized Euclidean L² norm plus either the continuum interpolation seminorm or the exact Euclidean fractional Sobolev seminorm. The two resulting extended-valued full norms are equivalent with one finite constant depending only on the fractional order and the dimension.

source
noncomputable def HCPolySupport.continuousKFullENorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
ENNReal

The source-facing continuum interpolation full norm: normalized Euclidean L² plus the continuous K-seminorm.

Equations
Instances For
    source
    noncomputable def HCPolySupport.euclideanHsFullENorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
    ENNReal

    The source-facing exact Euclidean fractional full norm: normalized Euclidean L² plus the Euclidean H^s seminorm.

    Equations
    Instances For
      source
      theorem HCPolySupport.continuousKFullENorm_eq {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      continuousKFullENorm s F = (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField + continuousKSeminorm s F

      Evaluation formula for the continuous interpolation full norm.

      source
      theorem HCPolySupport.euclideanHsFullENorm_eq {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      euclideanHsFullENorm s F = (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField + euclideanHsESeminorm s F

      Evaluation formula for the exact Euclidean fractional full norm.

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

      A single constant that controls both directions of the additive full-norm comparison.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.continuousKEuclideanHsFullENormConstant_lt_top (s : ↑FractionalOrder) (d : ℕ) :
        continuousKEuclideanHsFullENormConstant s d < ⊤

        The common full-norm comparison constant is finite.

        source
        theorem HCPolySupport.euclideanHsFullENorm_le_mul_continuousKFullENorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
        euclideanHsFullENorm s F ≤ continuousKEuclideanHsFullENormConstant s d * continuousKFullENorm s F

        The continuum interpolation full norm controls the exact Euclidean fractional full norm with the common finite constant.

        source
        theorem HCPolySupport.continuousKFullENorm_le_mul_euclideanHsFullENorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
        continuousKFullENorm s F ≤ continuousKEuclideanHsFullENormConstant s d * euclideanHsFullENorm s F

        The exact Euclidean fractional full norm controls the continuum interpolation full norm with the same common finite constant.

        source
        theorem HCPolySupport.exists_continuousKFullENorm_euclideanHsFullENorm_equivalence (d : ℕ) (s : ↑FractionalOrder) :
        ∃ C < ⊤, ∀ (F : UnitCubeEuclideanL2Field d), (MemEuclideanHs s F ↔ continuousKSeminorm s F < ⊤) ∧ euclideanHsFullENorm s F ≤ C * continuousKFullENorm s F ∧ continuousKFullENorm s F ≤ C * euclideanHsFullENorm s F

        Source-facing all-dimensional equivalence between the approved additive continuous interpolation and exact Euclidean fractional full norms.