High-contrast homogenization: Provider.Regularity.CorrectorRealRadiusNegOneScale

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

Running-scale normalization for centered-cube negative-one norms

This module compares inverse-side-length normalizations on a centered cube of real side length and its canonical enclosing triadic origin cube. The only analytic input is the quotient-safe centered-cube restriction estimate.

noncomputable def HCPolySupport.HighContrast.realRadiusScaledNegOneNorm {d : ℕ} (R : ℝ) (F : ↥(HilbertVectorL2 (centeredOpenCube d R))) : ENNReal

The inverse-side-length normalized negative-one norm on a centered cube of real side length.

Equations

• HCPolySupport.HighContrast.realRadiusScaledNegOneNorm R F = ENNReal.ofReal R⁻¹ * HCPolySupport.HighContrast.localNegOneNorm (HCPolySupport.HighContrast.centeredOpenCube d R) F

noncomputable def HCPolySupport.HighContrast.triadicScaledNegOneNorm {d : ℕ} (n : ℤ) (F : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))) : ENNReal

The inverse-side-length normalized negative-one norm on an origin cube of integer triadic generation.

Equations

• HCPolySupport.HighContrast.triadicScaledNegOneNorm n F = ENNReal.ofReal (3 ^ n)⁻¹ * HCPolySupport.HighContrast.localNegOneNorm (HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) F