High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentBound

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

The averaged term on recent scales

The energy map and the factor-two response identity control the cell averages of the optimizer differences. On the good branch, the all-scale maximum reduces the remaining response factor to the printed geometric weight.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_difference_energy_nonneg {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) : 0 ≤ 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))

Each recent optimizer-difference energy is nonnegative.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_average_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) fun (x : Vec d) => diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x)) ≤ √2 * diagonalWeakMetricFactor m E * (1 + √(diagonalWeakMaximum rho q t E a).toReal * 3 ^ (rho * (↑t - ↑k) / 2)) * diagonalWeakLoadMinus E p r * √(blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d))

Before imposing the good-event threshold, the recent averaged term is controlled by the square-root response maximum and averaged defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_average_good_le {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 delta : ℝ} (hrho : 0 < rho) (hdelta1 : delta ≤ 1) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) fun (x : Vec d) => diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x)) ≤ 4 * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * 3 ^ (rho * (↑t - ↑k) / 2) * √(blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d))

On the good branch, the recent averaged term has the geometric factor 3^{rho(t-k)/2} and no remaining maximum.

The released split level

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_average_good_at_level_le {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 delta : ℝ} (hrho : 0 < rho) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) fun (x : Vec d) => diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x)) ≤ √2 * (1 + √delta) * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * 3 ^ (rho * (↑t - ↑k) / 2) * √(blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d))

The recent averaged term at a released split level: the printed Step 4 constant √2(1+√δ), which is 2√2 at the fixed level.