High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.GaugeFrameTerminalAtCertificate

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

The corrector-decay terminal at an arbitrary certificate

The corrector-decay terminal is stated here with the certificate as a parameter. A version whose corrector-family premise and good-scale premise are both fixed at PrintOrderRateBearingCommonAffineGoodScale would force the corrector family's corrector-family hypothesis to be supplied at the print certificate, a per-sample predicate carrying no translation-invariant block-row event, which the event-carrying certificate of the root cannot discharge.

The proof uses the corrector-family hypothesis in exactly one place, hfamily.normalizedJoint a x hGood, at the sample the theorem is applied to. The corrector-family hypothesis is therefore taken at an arbitrary GoodScale, together with the projection GoodScale abar a x → PrintOrderRateBearing… abar a x that every consumer has. Taking GoodScale := PrintOrderRateBearing… and hproj := fun _ _ h ↦ h recovers the statement at the print certificate.

theorem HCPolySupport.HighContrast.CorrectorComposition.exists_gaugeFrameCorrectorDecayConstant_atCertificate (d : ℕ) [NeZero d] (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (C : ℝ), 0 < C ∧ have c := canonicalCorrectorSmallness d g hg; ∀ (GoodScale : Mat d → CoeffSpace d → ℝ → Prop) (kappa : ℝ) (abar : Mat d) (Phi : Vec d → CoeffSpace d → Vec d → ℝ) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d), (∀ (a : CoeffSpace d) (x : ℝ), GoodScale abar a x → PrintOrderRateBearingCommonAffineGoodScale d g c kappa abar a x) → Root.CanonicalPullbackCorrectorFamily GoodScale abar Phi gradPhi → ∀ (a : CoeffSpace d) (x : ℝ), 1 ≤ x → GoodScale abar a x → ∀ (e : Vec d) (r : ℝ), x ≤ r → ((ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (gradPhi e a y)) + ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (↑↑a y - skewPart abar) (e + gradPhi e a y) - matVecMul (symmPart abar) e)) ≤ ENNReal.ofReal (C * √(vecDot e (matVecMul (symmPart abar) e)) * (r / x) ^ (-kappa))

The corrector-decay terminal at an arbitrary certificate the reconciled-smallness certificate. The corrector-decay terminal closes in the exact square-root gauge. The identity response estimate is run at the targeted certificate scale; the single affine multiplier already present in the exposed common scale pays for transport back to the physical ellipsoid.

The corrector-family hypothesis and the good scale are read at a given certificate GoodScale that projects to the printed one; the statement is the case GoodScale := PrintOrderRateBearingCommonAffineGoodScale d g c kappa.