High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1CanonicalSameProjectionDecay

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

Same-projection decay for the canonical slope map

The canonical least-squares projection on the base cube is the exact base minimizer. The fixed-base decay theorem can therefore retain that one linear projection while the observation cube ranges through the full finite interval.

theorem HCPolySupport.HighContrast.Root.exists_canonicalFiniteCorrectorSameProjectionDecayConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (hetaHalf : 1 / 2 ≤ eta) (heta1 : eta < 1) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 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 → ∀ (n m : ℕ), n0 ≤ ↑n → ∀ (hnm2 : n + 2 ≤ m) (hT : Function.Injective ⇑(finiteTrialHarmonicGradientLinearMap a ⋯)), have P := finiteCorrectorWeightedProjection a hCauchy ⋯ hT; ∀ (e : Vec d), ∀ q ∈ Finset.Icc n m, (weightedGradNorm (a.coeffOn (originCube d ↑q)).toCoeffField (openCubeSet (originCube d ↑q)) fun (x : Vec d) => e + (Phi e).globalGradientRepresentative x - (finiteAffineSolution a (↑m) (P e)).toH1.grad x) ≤ ENNReal.ofReal (C * Real.rpow 3 (-eta * ↑(m - q))) * weightedGradNorm (a.coeffOn (originCube d ↑m)).toCoeffField (openCubeSet (originCube d ↑m)) fun (x : Vec d) => e + (Phi e).globalGradientRepresentative x - (finiteAffineSolution a (↑m) e).toH1.grad x

The canonical projection chosen on the base cube has the same real-rate decay on every intermediate cube.