High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.C1EquivariantPullbackEliminator
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Canonical pullback data for an equivariant corrector family #
The physical family records the normalized joint corrector from which its gradient is obtained. This is the identification needed to transport a simultaneous-slope estimate from normalized cubes to physical coordinates.
structure
HCPolySupport.HighContrast.Root.CanonicalPullbackCorrectorFamily
{d : ℕ}
[NeZero d]
(GoodScale : Mat d → CoeffSpace d → ℝ → Prop)
(abar : Mat d)
(Phi : Vec d → CoeffSpace d → Vec d → ℝ)
(gradPhi : Vec d → CoeffSpace d → Vec d → Vec d)
:
A physical corrector family retains, at every certified sample, one small-order normalized reference family and the exact normalized-root pullback identity for the canonical joint corrector.
- weakGradient (a : CoeffSpace d) (x : ℝ) : GoodScale abar a x → ∀ (e : Vec d), HasWeakGradientOn Set.univ (Phi e a) (gradPhi e a)
- normalizedJoint (a : CoeffSpace d) (x : ℝ) : GoodScale abar a x → ∃ (hS : Matrix.PosDef (symmPart abar)) (s : ℝ) (tolerance : ℝ) (aRef : Book.Ch03.CoeffFamily d) (L : ℕ) (hCauchy : FiniteAffineCorrectionLocalCauchy aRef), 0 < s ∧ s < 1 / 2 ∧ (∀ (Q : TriadicCube d), (aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) ∧ ScalarIdentityGoodTail aRef s tolerance ↑(Quenched.triadicCeilingIndex x + L) ∧ IsFiniteAffineCorrectionJointLocalEquation aRef (finiteAffineCorrectionJointLocalLimit aRef hCauchy) ∧ ∀ (e : Vec d), (∃ (c₀ : ℝ), (fun (y : Vec d) => Phi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y)) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => (finiteAffineCorrectionJointLocalLimit aRef hCauchy (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalValueRepresentative y + c₀) ∧ (fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (e + gradPhi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y))) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) e + (finiteAffineCorrectionJointLocalLimit aRef hCauchy (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalGradientRepresentative y