High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.AffineAdaptedCellResponseParentRow
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Adapted-target response priced by one reference parent row #
An enclosing exact normalized-root parent turns every response maximum in the general filling into the corresponding descendant maximum of that one parent. Thus the only series left at this level is the certificate's own reference response row multiplied by the explicit filling weights.
theorem
HCPolySupport.HighContrast.RowSupply.exists_normalizedRootLoads_adaptedTarget_le_enclosingParentRow
{d : ℕ}
[NeZero d]
(a : CoeffSpace d)
(abar : Mat d)
(hS : Matrix.PosDef (symmPart abar))
(t : ℤ)
(aRef : Book.Ch03.CoeffFamily d)
(haRef :
∀ (R : TriadicCube d),
(aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯
((normalizedCenteredCoeff a abar hS).coeffOn (Response.adaptedDomain ⋯ t)).toCoeffField)
{p : Mat d}
(hp : Matrix.PosDef p)
(n j M : ℤ)
(hnM : n ≤ M)
(y : Vec d)
(hEnclose : adaptedCellTranslate p j y ⊆ adaptedCell (Selection.normalizedRoot (symmPart abar)) M)
(e : FullBlockVec d)
(he : Book.Ch02.fullBlockVecNormSq e = 1)
:
∃ (P : BlockVec d) (Q : BlockVec d) (Z : ℤ → Finset (Fin d → ℤ)),
normalizedReferencePrimalLoad abar P = ofFullBlockVec e ∧ normalizedReferenceDualLoad abar Q = ofFullBlockVec e ∧ (∀ (r : ℤ),
↑(Z r) = Transport.fillingIndex (Selection.normalizedRoot (symmPart abar)) n (adaptedCellTranslate p j y) r) ∧ ((Summable fun (u : ℕ) =>
(if u = 0 then 1 else 6 * ↑d * √↑d * ‖p⁻¹ * Selection.normalizedRoot (symmPart abar)‖ * 3 ^ (n - ↑u - j)) * Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d M) (n - ↑u) aRef 1) →
Transport.coeffSpaceDoubledResponse (adaptedCellTranslate p j y) a P Q ≤ ∑' (u : ℕ), (if u = 0 then 1
else 6 * ↑d * √↑d * ‖p⁻¹ * Selection.normalizedRoot (symmPart abar)‖ * 3 ^ (n - ↑u - j)) * Book.Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d M) (n - ↑u) aRef 1)
The doubled response on an arbitrary adapted target is controlled by the descendant-response row of one enclosing exact normalized-root parent.