High-contrast homogenization: Provider.Regularity.FiniteAffineGradientExcessDecay #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Iteration of finite affine gradient excess #
This module iterates the ruled fixed-gap contraction and controls the terminal remainder band by normalized centered-cube restriction.
theorem
HCPolySupport.HighContrast.finiteAffineGradientExcess_sub_nat_le
{d : ℕ}
[NeZero d]
(a : Book.Ch02.TriadicCoeffFamily d)
(k m : ℤ)
(hkm : k ≤ m)
(N : ℕ)
(u : Book.Ch03.CubeSolution (originCube d m) a)
:
finiteAffineGradientExcess a (k - ↑N) m u ≤ ENNReal.ofReal ↑((3 ^ d) ^ N) * finiteAffineGradientExcess a k m u
Restricting the gradient excess by N centered scales loses at most the
corresponding normalized-volume factor.