High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.AffineAdaptedCellResponseFillingSummable
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Summability of the adapted-target filling row #
The codimension-one filling weight is summable against the normalized reference response row. This removes the last conditional summability premise from the affine adapted-cell response comparison.
theorem
HCPolySupport.HighContrast.RowSupply.summable_normalizedRoot_adaptedTarget_enclosingParentRow
{d : ℕ}
[NeZero d]
{s : ℝ}
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(abar : Mat d)
(aRef : Book.Ch03.CoeffFamily d)
{p : Mat d}
(n j M : ℤ)
(hnM : n ≤ M)
:
The response row of an enclosing normalized-root parent is summable after multiplication by the general adapted-filling weights.
theorem
HCPolySupport.HighContrast.RowSupply.exists_normalizedRootLoads_adaptedTarget_le_enclosingParentRow_summable
{d : ℕ}
[NeZero d]
{s : ℝ}
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(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) ∧ 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 normalized-reference response comparison on an arbitrary adapted target has no remaining summability premise.