High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1QuantitativeCorrectorTail
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Quantitative coefficient-energy tail of finite correctors #
The finite-successor estimate is telescoped in the symmetric coefficient energy itself. The fixed-cube joint limit then retains the same bound, without conversion through a lower ellipticity constant.
theorem
HCPolySupport.HighContrast.Root.sqrt_normalizedEnergy_grad_eq_weightedGradNorm_toReal
{d : ℕ}
{U : Set (Vec d)}
{b : CoeffField d}
{lam Lam : ℝ}
(hEll : IsEllipticFieldOn lam Lam U b)
(u : H1Function U)
:
√(normalizedLocalSymmetricEnergy hEll u.gradToHilbertVectorL2) = (weightedGradNorm b U u.grad).toReal
theorem
HCPolySupport.HighContrast.Root.exists_jointFiniteCorrectorWeightedTailConstants
(d : ℕ)
[NeZero d]
(s : ℝ)
(hs : 0 < s)
(hs_lt : s < 1 / 2)
:
∃ (C : ℝ) (c : ℝ),
0 < C ∧ c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n0 : ℤ),
delta ∈ Set.Ioc 0 c →
ScalarIdentityGoodTail a s delta n0 →
∀ (Phi : Vec d → NormalizedLocalH1Carrier d),
IsFiniteAffineCorrectionJointLocalEquation a Phi →
∀ (e : Vec d) (q m : ℕ),
n0 ≤ ↑q →
q + 2 ≤ m →
√(normalizedLocalSymmetricEnergy ⋯
((have this := constantGradientOnOriginCube e ↑q;
this) + (Phi e).gradientComponent q - finiteAffineInnerGradientClass a e q (m - q))) ≤ C * (1 + delta) * delta * euclideanNorm e
The joint affine corrector is quantitatively close, on every fixed inner cube, to every finite affine corrector at least two generations outside it.