High-contrast homogenization: Provider.Regularity.PrintOrderRoundedResponseRows #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Rounded response rows at the printed-order common scale #
The stochastic certificate and every rounded weak-error row use the order
selected after g. The common scale contains the exact boundary-layer loss
for that order.
noncomputable def
HCPolySupport.HighContrast.printOrderCommonQuantitativeAffineScale
(d : ℕ)
(g sourceAmplitude target kappa : ℝ)
(abar : Mat d)
(X : CoeffSpace d → ℝ)
(a : CoeffSpace d)
:
The common quantitative scale with the printed-order response loss.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.HighContrast.PrintOrderQuantitativeNormalizedReferenceCertificate.exists_targetedRoundedReferenceCoeffFamily
{d : ℕ}
[NeZero d]
{a : CoeffSpace d}
{abar : Mat d}
{g sourceAmplitude target kappa : ℝ}
{X : CoeffSpace d → ℝ}
(h : PrintOrderQuantitativeNormalizedReferenceCertificate abar g sourceAmplitude kappa (X a) a)
(hTarget : 0 < target)
(t : ℤ)
:
∃ (hS : Matrix.PosDef (symmPart abar)) (aRef : Book.Ch03.CoeffFamily d),
0 < printCertificateOrder g ∧ printCertificateOrder g < 1 / 2 ∧ 0 ≤ target ∧ 0 < kappa ∧ 1 ≤ X a ∧ (∀ (R : TriadicCube d),
(aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯
((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField) ∧ ScalarIdentityPowerTail aRef (printCertificateOrder g) target kappa
(targetedQuantitativeEffectiveScale sourceAmplitude target kappa X a)
Targeting preserves the printed reference family on every adapted cell.