High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.ExactFiniteResponse

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

theorem HCPolySupport.HighContrast.exists_identityFiniteResponseConstant (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : Book.Ch03.CoeffFamily d) (m : ℤ) (e : Vec d), scalarIdentityWeakError a (printCertificateOrder g) m ≤ 1 → have u := (finiteAffineSolution a m e).toH1; have E := scalarIdentityWeakError a (printCertificateOrder g) m; (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) (printCertificateOrder g) fun (x : Vec d) => u.grad x - e) ≤ C * E * euclideanNorm e ∧ (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d m) (printCertificateOrder g) fun (x : Vec d) => matVecMul (Book.Ch03.publicCoeffField (originCube d m) a x) (u.grad x) - e) ≤ C * E * euclideanNorm e ∧ cubeBesovScaleWeight 1 (originCube d m) * cubeLpNorm (originCube d (m - 1)) 2 (finiteAffineCorrection a m e).toFun ≤ C * E * euclideanNorm e

At exact identity reference, the two actual finite affine response rows are controlled at the same printed order as the scalar identity weak error.