High-contrast homogenization: Provider.Regularity.CanonicalSlopeLocalCoercivity

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

Local coercivity of the canonical corrector slope

Finite affine average-slope coercivity passes to the canonical joint local limit. Hence a canonical full-gradient class which vanishes on one admissible fixed cube must have zero slope.

theorem HCPolySupport.HighContrast.exists_scalarIdentityGoodTailCanonicalLocalSlopeCoercivityThreshold (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) : ∃ c ∈ Set.Ioo 0 1, ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n : ℤ), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodTail a s delta n → ∀ (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))

Under a sufficiently small scalar good tail, the canonical slope is controlled by its full-gradient average on every cube beyond the starting scale.

theorem HCPolySupport.HighContrast.canonicalSlope_eq_zero_of_localFullGradient_eq_zero {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {n : ℤ} (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))) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e : Vec d) (q : ℕ) (hnq : n ≤ ↑q) (hzero : (have this := constantGradientOnOriginCube e ↑q; this) + (finiteAffineCorrectionJointLocalLimit a hCauchy e).gradientComponent q = 0) : e = 0

Local injectivity: if the canonical full-gradient class vanishes on one admissible cube, then its slope is zero.

theorem HCPolySupport.HighContrast.canonicalSlope_eq_of_localFullGradient_eq {d : ℕ} [NeZero d] {a : Book.Ch02.TriadicCoeffFamily d} {n : ℤ} (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))) (hCauchy : FiniteAffineCorrectionLocalCauchy a) (e e' : Vec d) (q : ℕ) (hnq : n ≤ ↑q) (heq : (jointAffineFullGradientLinearMap a hCauchy q) e = (jointAffineFullGradientLinearMap a hCauchy q) e') : e = e'

Two canonical slopes whose full-gradient classes agree on one admissible cube are equal.