High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.FixedGapNegOneRestriction

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

noncomputable def HCPolySupport.HighContrast.gapThreeNegOneRestrictionConstant (d : ℕ) : ENNReal

The fixed three-generation restriction cost.

Equations

• HCPolySupport.HighContrast.gapThreeNegOneRestrictionConstant d = ENNReal.ofReal (27 * √((3 ^ 3) ^ d))

theorem HCPolySupport.HighContrast.gapThreeNegOneRestrictionConstant_lt_top (d : ℕ) : gapThreeNegOneRestrictionConstant d < ⊤

theorem HCPolySupport.HighContrast.triadicScaledNegOne_restrict_gap_three_le {d : ℕ} [NeZero d] (q : ℤ) (F : ↥(HilbertVectorL2 (openCubeSet (originCube d (q + 3))))) : have hsub := ⋯; triadicScaledNegOneNorm q ((localHilbertVectorL2Restrict hsub) F) ≤ gapThreeNegOneRestrictionConstant d * triadicScaledNegOneNorm (q + 3) F

Restricting a local L² class across the fixed three-generation gap costs a dimension-only factor after inverse-side-length normalization.