High-contrast homogenization: Provider.PolynomialHomogenization.DecoupledRootCertificatePair #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Decoupled certificates at the polynomial-homogenization root #
The deterministic regularity terminals use a privately selected small fractional order. The Dirichlet row uses the printed order selected after the stochastic exponent. Both certificates retain the same selected contrast and rate parameters and the same exposed physical scale.
structure
HCPolySupport.HighContrast.Root.DecoupledRootGoodScale
(d : ℕ)
[NeZero d]
(g c kappa : ℝ)
(abar : Mat d)
(a : CoeffSpace d)
(x : ℝ)
:
The two certificates consumed at the root, with all stochastic and calibration parameters retained in the type.
- privateOrder : NormalizedReferenceGoodScale abar a x
- printOrder : PrintOrderRateBearingCommonAffineGoodScale d g c kappa abar a x
Instances For
theorem
HCPolySupport.HighContrast.Root.DecoupledRootGoodScale.to_printOrder
{d : ℕ}
[NeZero d]
{g c kappa : ℝ}
{abar : Mat d}
{a : CoeffSpace d}
{x : ℝ}
(h : DecoupledRootGoodScale d g c kappa abar a x)
:
PrintOrderRateBearingCommonAffineGoodScale d g c kappa abar a x
The printed-order certificate is available without changing the selected root parameters.
theorem
HCPolySupport.HighContrast.Root.DecoupledRootGoodScale.of_printOrder
{d : ℕ}
[NeZero d]
{g c kappa : ℝ}
{abar : Mat d}
{a : CoeffSpace d}
{x : ℝ}
(h : PrintOrderRateBearingCommonAffineGoodScale d g c kappa abar a x)
:
DecoupledRootGoodScale d g c kappa abar a x
The printed quantitative field can be forgotten to the qualitative field at the same exposed common scale.