Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.SeminormComparison

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

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

Convention-neutral comparison of continuous interpolation seminorms #

This module takes half-powers of the all-dimensional energy comparisons. It keeps the directional seminorm bounds separate for use by the approved source-facing full norm.

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

The finite constant in the continuous K-seminorm to Euclidean H^s-seminorm direction.

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

    The continuous K-to-Euclidean-H^s seminorm constant is finite.

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

    The finite constant in the Euclidean H^s-seminorm to continuous K-seminorm direction, including the normalized L² root-scale term.

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

      The Euclidean-H^s-to-continuous-K seminorm constant is finite.

      source
      theorem HCPolySupport.continuousKSeminorm_le_mul_euclideanHsESeminorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      continuousKSeminorm s F ≤ continuousKToEuclideanHsSeminormConstant s d * euclideanHsESeminorm s F

      In every dimension, the exact Euclidean fractional seminorm controls the continuous K-seminorm through an explicit finite constant.

      source
      theorem HCPolySupport.euclideanHsESeminorm_le_mul_normalizedEuclideanLpENorm_add_continuousKSeminorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      euclideanHsESeminorm s F ≤ euclideanHsToContinuousKSeminormConstant s d * ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField + continuousKSeminorm s F)

      In every dimension, the continuous K-seminorm and normalized Euclidean L² norm control the exact Euclidean fractional seminorm through an explicit finite constant.

      source
      theorem HCPolySupport.continuousKSeminorm_lt_top_iff_euclideanHsESeminorm_lt_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      continuousKSeminorm s F < ⊤ ↔ euclideanHsESeminorm s F < ⊤

      The exact Euclidean fractional seminorm is finite exactly when the continuous K-seminorm is finite.

      source
      theorem HCPolySupport.memEuclideanHs_iff_continuousKSeminorm_lt_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
      MemEuclideanHs s F ↔ continuousKSeminorm s F < ⊤

      Exact Euclidean fractional membership is equivalent to finiteness of the continuous K-seminorm, with no measurable-representative or dimension hypothesis.