High-contrast homogenization: Provider.Regularity.LiouvilleExcessSlopeSelection

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

Approximate slope selection from finite affine excess

The finite affine excess is an ENNReal infimum and need not be attained. This module selects arbitrarily accurate candidates and, when a ruled slope family is available, reparameterizes them by their exact target slope on the fixed inner cube.

theorem HCPolySupport.HighContrast.exists_finiteAffineGradientExcess_candidate_lt_add {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) (epsilon : ENNReal) (hepsilon : epsilon ≠ 0) : ∃ (b : Vec d), (weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m b).toH1.grad x) < finiteAffineGradientExcess a n m u + epsilon

Every positive tolerance admits an affine-boundary candidate strictly below the finite affine excess plus that tolerance. No attainment is used.