High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentQuadratic

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

Normalizing the recent quadratic defect

Congruence by the reference square root identifies the unnormalized averaged response defect with D_{k,t}(E). Its positive-semidefinite order bound then controls the load quadratic form by the spectral size of that normalized defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_response_quadratic_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) (p r : Vec d) : blockVecDot (-p, r) (blockMatVecMul (blockSub (ofFullBlockMat ((↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (adaptedResponse q k w a))) (coarseBlock (adaptedCell q t) a)) (-p, r)) ≤ diagonalWeakLoadMinus E p r ^ 2 * blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d)

The response quadratic form is bounded by the squared reference load times the size of the normalized averaged defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_difference_energy_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) (p r : Vec d) : (avsum (alignedIndex q k t) fun (w : Fin d → ℤ) => Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x))) ≤ 2 * diagonalWeakLoadMinus E p r ^ 2 * blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d)

The recent optimizer-difference energy is bounded by twice the squared load times the normalized averaged defect.