High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.FormulaicRowLevelWindowTailComposition
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Row-level order conversion in the epsilon frame #
The stochastic row is transported first. The midpoint-order converter is then applied to that transported row, before any all-depth observation aggregation.
theorem
HCPolySupport.HighContrast.RowSupply.RowRetainingPrintOrderGoodScale.exists_formulaicScaledResponseWindowTail
{d : ℕ}
[NeZero d]
{g c kappaRate : ℝ}
{abar : Mat d}
{a : CoeffSpace d}
{x epsilon : ℝ}
(h : RowRetainingPrintOrderGoodScale d g c kappaRate abar a x)
(hS : Matrix.PosDef (symmPart abar))
(hg : g ∈ Set.Ico 0 1)
(hkappa : 0 < kappaRate)
(hx : 1 ≤ x)
(hepsilon : 0 < epsilon)
(hscale : x ≤ epsilon⁻¹)
:
∃ (N : ℕ) (G : ℕ) (lambda : ℝ) (deltaScaled : ℝ) (aScaled : CoeffSpace d) (aRef : Book.Ch03.CoeffFamily d) (L : ℕ),
lambda = epsilon * 3 ^ N ∧ lambda ∈ Set.Icc 1 3 ∧ aScaled = Quenched.physicalScaleCoefficient N a ∧ deltaScaled = triadicallyScaledRowAmplitude h.delta (h.activationScale a) N (2 * kappaRate) ∧ witnessEccentricity (symmPart abar) * √↑d ≤ 3 ^ ↑G ∧ 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d) ∧ L = Certificate.formulaicNormalizedReferenceTailShift d (responseWindowOrder g)
(Certificate.printRowOrder g) (2 * kappaRate) G ∧ ↑L < max 0
(Real.logb 3
(Certificate.shiftedTailAbsorptionPrefactor d (responseWindowOrder g)
(Certificate.printRowOrder g) G) / (2 * kappaRate)) + 1 ∧ (∀ (Q : TriadicCube d),
(aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯
↑↑(normalizedCenteredCoeff aScaled abar hS)) ∧ ScalarIdentityPowerTail aRef (responseWindowOrder g) (√deltaScaled) kappaRate (3 ^ ↑L)
The row-retaining root interface gives a response-window reference tail in the triadically scaled frame.