Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.DiscreteKOverlapEnergy

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

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

Extended discrete K-functional energy and concrete overlap comparison #

The discrete K-functional energy is the ℝ≥0∞ supremum of its finite squared partial seminorms. Both comparison directions below are lifted directly from proved finite-depth averaging and overlap-Poincare estimates.

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

The extended internal discrete K-functional energy on the centered unit cube, defined only through finite partial sums.

Equations
Instances For
    source
    theorem HCPolySupport.ofReal_sq_cubeKPartialSeminorm_le_extendedDiscreteKFunctionalEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (N : ℕ) :
    ENNReal.ofReal (cubeKBesovVectorPartialSeminormTwo (originCube d 0) (↑s) N F.toField ^ 2) ≤ extendedDiscreteKFunctionalEnergy s F

    Every finite squared discrete K-functional partial seminorm is bounded by the extended discrete energy.

    source
    noncomputable def HCPolySupport.discreteKOverlapAveragingConstant (d : ℕ) :
    ℝ

    The concrete overlap-averaging constant after combining residual and gradient contributions.

    Equations
    Instances For
      source
      theorem HCPolySupport.discreteKOverlapAveragingConstant_nonneg (d : ℕ) :
      0 ≤ discreteKOverlapAveragingConstant d
      source
      theorem HCPolySupport.discreteKOverlapAveragingConstant_sq_lt_top (d : ℕ) :
      ENNReal.ofReal (discreteKOverlapAveragingConstant d ^ 2) < ⊤

      The squared concrete averaging factor remains finite after promotion to extended nonnegative values.

      source
      noncomputable def HCPolySupport.overlapDiscreteKConstant (d : ℕ) :
      ℝ

      The concrete overlap-Poincare constant after assembling one K-functional competitor value.

      Equations
      Instances For
        source
        theorem HCPolySupport.overlapDiscreteKConstant_nonneg (d : ℕ) :
        0 ≤ overlapDiscreteKConstant d
        source
        theorem HCPolySupport.overlapDiscreteKConstant_sq_lt_top (d : ℕ) :
        ENNReal.ofReal (overlapDiscreteKConstant d ^ 2) < ⊤

        The squared concrete overlap-Poincare factor remains finite after promotion to extended nonnegative values.

        source
        theorem HCPolySupport.extendedDiscreteKFunctionalEnergy_le_mul_extendedVectorOverlapBesovEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
        extendedDiscreteKFunctionalEnergy s F ≤ ENNReal.ofReal (discreteKOverlapAveragingConstant d ^ 2) * extendedVectorOverlapBesovEnergy s F

        The extended discrete K-functional energy is controlled by the extended overlap energy using only the concrete overlap-averaging producer.

        source
        theorem HCPolySupport.extendedVectorOverlapBesovEnergy_le_mul_extendedDiscreteKFunctionalEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
        extendedVectorOverlapBesovEnergy s F ≤ ENNReal.ofReal (overlapDiscreteKConstant d ^ 2) * extendedDiscreteKFunctionalEnergy s F

        The extended overlap energy is controlled by the extended discrete K-functional energy using only the proved overlap-Poincare producer.