High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.NormalizedDualToScaledNegOne

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

theorem HCPolySupport.HighContrast.exists_scaledNegOne_pair_le_normalizedDualRows (d : ℕ) [NeZero d] (s : ↑FractionalOrder) (hsHalf : ↑s < 1 / 2) : ∃ C < ⊤, 0 < C ∧ ∀ (n : ℤ) (F G : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))) (B : ℝ), (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d n) ↑s fun (x : Vec d) => (↑↑F x).toVec) ≤ B → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d n) ↑s fun (x : Vec d) => (↑↑G x).toVec) ≤ B → triadicScaledNegOneNorm n F + triadicScaledNegOneNorm n G ≤ C * ENNReal.ofReal B