High-contrast homogenization: Provider.Regularity.LiouvilleGlobalSlope #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
One global slope from the Liouville finite-excess family #
The exact finite realizations supplied by the fixed-cube excess theorem all represent the same global gradient. Their inner-cube gradient classes are therefore compatible, so the independently compactness-selected slopes agree.
theorem
HCPolySupport.HighContrast.exists_common_jointSlope_of_liouvilleFixedCubeExcess
{d : ℕ}
[NeZero d]
{s : ℝ}
{a : Book.Ch02.TriadicCoeffFamily d}
{delta c : ℝ}
{n : ℤ}
(hthreshold :
c ∈ Set.Ioo 0 1 ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ),
delta ∈ Set.Ioc 0 c →
ScalarIdentityGoodTail a s delta n →
∀ (q t : ℕ),
n ≤ ↑q →
∀ (e : Vec d),
euclideanNorm e ≤ 2 * euclideanNorm
(cubeAverageVec (originCube d ↑q) (finiteAffineSolution a (↑(q + t + 2)) e).toH1.grad))
(hcoercive :
∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (q : ℕ),
n ≤ ↑q →
euclideanNorm e ≤ 2 * euclideanNorm
(localGradientClassAverage
((have this := constantGradientOnOriginCube e ↑q;
this) + (finiteAffineCorrectionJointLocalLimit a hCauchy e).gradientComponent q)))
(hdelta : delta ∈ Set.Ioc 0 c)
(hgood : ScalarIdentityGoodTail a s delta n)
(hCauchy : FiniteAffineCorrectionLocalCauchy a)
(u : (p : ℕ) → Book.Ch03.CubeSolution (originCube d (↑p - 2)) a)
(Dv : Vec d → Vec d)
(huGrad : ∀ (p : ℕ), (u p).toH1.grad = Dv)
(hexcess :
∀ (k : ℤ),
n ≤ k → Filter.Tendsto (fun (p : ℕ) => finiteAffineGradientExcess a k (↑p - 2) (u p)) Filter.atTop (nhds 0))
:
∃ (e : Vec d),
∀ (q : ℕ),
n.toNat ≤ q →
(finiteCubeSolutionRestriction a ⋯ (u (q + 4))).toH1.gradToHilbertVectorL2 = (jointAffineFullGradientLinearMap a hCauchy q) e
A single slope represents the global Liouville gradient on every centered cube beyond the good-tail base.