High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.AffineAdaptedCellResponseFilling

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Normalized-reference response on an affine adapted target

The inverse physical loads attached to a unit normalized-reference load work on every exact normalized-root cell. Combining that available cell estimate with the general maximal filling carries the response to any positive- definite adapted target, including targets produced by a bounded scalar dilation and a matrix gauge.

theorem HCPolySupport.HighContrast.RowSupply.exists_normalizedRootLoads_adaptedTarget_doubledResponse_le_tsum {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 : ℤ) (y : Vec d) (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) ∧ ∀ (B : ℤ → ℝ), (∀ (r : ℤ), 0 ≤ B r) → (∀ (u : ℕ), ∀ w ∈ Z (n - ↑u), Book.Ch02.normalizedBlockResponseMax (translateCube w (originCube d (n - ↑u))) aRef 1 ≤ B (n - ↑u)) → (Summable fun (u : ℕ) => (if u = 0 then 1 else 6 * ↑d * √↑d * ‖p⁻¹ * Selection.normalizedRoot (symmPart abar)‖ * 3 ^ (n - ↑u - j)) * B (n - ↑u)) → 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)) * B (n - ↑u)

A unit identity-reference load admits physical inverse loads whose doubled response on an arbitrary adapted target is controlled by any summable row-majorant for the exact normalized-root response maxima. The target grid p is unrestricted apart from positive definiteness; hence residual scalar dilations and the square-root gauge enter only through ‖p⁻¹ q‖.