High-contrast homogenization: Provider.Regularity.CorrectorLocalCauchy #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Local Cauchy convergence of finite correctors #
A scalar good tail makes the unshifted finite zero-trace corrections Cauchy
on every fixed centered cube. The proof converts normalized coefficient
energy to the ordinary local Hilbert L² norm using the actual lower
ellipticity constant, then discards finitely many successor differences.
theorem
HCPolySupport.HighContrast.norm_gradToHilbertVectorL2_le_sqrt_cubeVolume_div_lam_mul_of_weightedGradNorm_le
{d : ℕ}
(Q : TriadicCube d)
(a : Book.Ch03.CoeffFamily d)
(u : H1Function (Book.Ch02.cubeDomain Q).carrier)
(B : ℝ)
(hB : 0 ≤ B)
(hweighted : weightedGradNorm (a.coeffOn Q).toCoeffField (openCubeSet Q) u.grad ≤ ENNReal.ofReal B)
:
A normalized weighted-gradient bound gives an ordinary local Hilbert
L² bound, with the exact volume and lower-ellipticity conversion factor.
theorem
HCPolySupport.HighContrast.exists_finiteAffineCorrectionLocalCauchyThreshold
(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 → FiniteAffineCorrectionLocalCauchy a
Small scalar good tails make the literal unshifted finite-corrector sequence locally gradient-Cauchy for every boundary slope.