High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1CanonicalProjectionInverseControl
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Quantitative inverse control for the canonical projection #
The coefficient-weighted projection is fixed at one inner and outer cube. Its quantitative distance from the identity gives both bijectivity and a uniform bound on the inverse slope.
theorem
HCPolySupport.HighContrast.Root.exists_canonicalFiniteCorrectorProjectionInverseControlThreshold
(d : ℕ)
[NeZero d]
(s : ℝ)
(hs : 0 < s)
(hs_lt : s < 1 / 2)
:
∃ c ∈ Set.Ioo 0 1,
∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n0 : ℤ),
delta ∈ Set.Ioc 0 c →
ScalarIdentityGoodTail a s delta n0 →
∀ (hCauchy : FiniteAffineCorrectionLocalCauchy a) (Phi : Vec d → NormalizedLocalH1Carrier d),
IsFiniteAffineCorrectionJointLocalEquation a Phi →
∀ (q m : ℕ),
n0 ≤ ↑q →
∀ (hqm2 : q + 2 ≤ m),
∃ (hT : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a ⋯)),
have P := finiteCorrectorWeightedProjection a hCauchy ⋯ hT;
Function.Bijective ⇑P ∧ ∀ (e : Vec d), euclideanNorm e ≤ 2 * euclideanNorm (P e)
Below a dimension-only tail threshold, the canonical weighted projection is bijective and its inverse has norm at most two.