High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.CorrectorWeakGradientRow

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

The weak corrector row at a good scale

The public quantitative datum of the anchored corrector is its weak norm: the scale-normalized negative Besov norm of the affine-plus-corrector gradient on a centered triadic cube. At a good scale the coarse-Poincare gradient row bounds that norm by the coefficient energy of the cube solution, and the energy is bounded by the Euclidean slope through the joint weighted gradient row. Both inputs are law-free: the multiplier carries only the dimension and the multiscale order, and no pointwise ellipticity constant appears anywhere.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailCorrectorWeakGradientRowConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ c ∈ Set.Ioo 0 1, ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d), ∃ (N : ℝ), 0 ≤ N ∧ ∀ (q : ℕ), n.toNat ≤ q → (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d ↑q) s fun (x : Vec d) => e + (finiteAffineCorrectionJointLocalLimit a hCauchy e).globalGradientRepresentative x) ≤ N

The weak corrector row. At a good scale the scale-normalized negative Besov norm of the affine-plus-corrector gradient on a centered triadic cube is bounded by the Euclidean slope, with a constant depending only on the dimension and the multiscale order.