High-contrast homogenization: Provider.Regularity.LiouvilleExcessRigidityPrep #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Finite-excess preparation for reverse Liouville rigidity #
This module records the zero-slope terminal bound and the elementary choice of an excess-decay exponent strictly above the frozen growth exponent.
theorem
HCPolySupport.HighContrast.finiteAffineGradientExcess_self_le_solutionEnergy
{d : ℕ}
[NeZero d]
(a : Book.Ch02.TriadicCoeffFamily d)
(m : ℤ)
(u : Book.Ch03.CubeSolution (originCube d m) a)
:
finiteAffineGradientExcess a m m u ≤ ENNReal.ofReal (Book.Ch03.h1EnergyNormOnCube (originCube d m) a u.toH1)
At the outer scale, the finite affine gradient excess is bounded by the energy of the solution itself; the zero-boundary affine solution has zero gradient a.e. by homogeneity.
theorem
HCPolySupport.HighContrast.exists_excessDecayExponent_gt_max_half
{theta : ℝ}
(htheta : theta < 1)
:
Every frozen exponent in (0,1) admits a decay exponent strictly above
both it and 1/2, as required by the source-level reverse-Liouville argument.