High-contrast homogenization: Provider.Response.DiagonalWeakNormScaleClosure

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

Centered single-scale closure for the diagonal weak estimate

The centered child increment is bounded by finite-variance contraction and the uncentered response estimate at the same scale.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_scale_energy_bound {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho : ℝ} {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r) - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ √2 * diagonalWeakMetricFactor m E * (1 + √(diagonalWeakMaximum rho q t E a).toReal * 3 ^ (rho * (↑t - ↑k) / 2)) * diagonalWeakEnergy hq t a p r

The normalized metric square sum of the centered child averages obeys the response-maximum scale estimate.