Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.ConvexFractionalChainScaleNormalization

High-contrast homogenization: #

Provider.PolynomialHomogenization.ConvexFractionalChainScaleNormalization

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Dyadic scale normalization of fractional chain jumps #

source
noncomputable def HCPolySupport.HighContrast.convexFractionalChainJumpConstant (d : ℕ) (rho Rad s : ℝ) :
ENNReal

The scale-free coefficient in the consecutive fractional-chain jump.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.convexFractionalChainLowerCoefficient_eq {d : ℕ} (hd : 1 ≤ d) {rho Rad s : ℝ} (hrho : 0 < rho) (hRad : 0 ≤ Rad) (n : ℕ) :
    convexFractionalChainLowerCoefficient d rho Rad s n = convexFractionalChainJumpConstant d rho Rad s * ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d))

    The lower-volume-normalized chain coefficient has exactly the dyadic homogeneity scale^(s-d).

    source
    theorem HCPolySupport.HighContrast.convexFractionalChainExactCoefficient_le_scale {d : ℕ} (hd : 1 ≤ d) (c x : Vec d) {rho Rad s : ℝ} (hrho : 0 < rho) (hRad : 0 ≤ Rad) (n : ℕ) :
    convexFractionalChainExactCoefficient c x rho Rad s n ≤ convexFractionalChainJumpConstant d rho Rad s * ENNReal.ofReal (convexFractionalChainScale n ^ (s - ↑d))

    The exact consecutive-ball coefficient is bounded by the scale-free structural constant times scale^(s-d).