High-contrast homogenization: Provider.Response.DiagonalWeakNormCellEnergy

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

Cell energies for the diagonal weak estimate

The parent optimizer restricts to every aligned child after transport to one everywhere-elliptic representative. This permits the coarse energy map to be applied on each child without changing the canonical optimizer state. The child energies then average exactly to twice the squared parent energy.

theorem HCPolySupport.HighContrast.Response.metricBlockNormSq_blockCellAverage_diagonalWeakState_le {d : ℕ} [NeZero 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) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : metricBlockNormSq m (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r)) ≤ diagonalWeakMetricFactor m E ^ 2 * blockSize (adaptedResponse q k w a) E * Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakState hq t a p r x))

The metric square of the canonical state's average on one child is controlled by the child's response size and the actual state energy there.

theorem HCPolySupport.HighContrast.Response.avsum_diagonalWeakState_energy_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) (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 (diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakState hq t a p r x))) = 2 * diagonalWeakEnergy hq t a p r ^ 2

The normalized average of the canonical state energies on an aligned subdivision is exactly twice the squared parent energy.

theorem HCPolySupport.HighContrast.Response.diagonalWeakState_cellEnergy_nonneg {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) (p r : Vec d) : 0 ≤ Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (diagonalWeakState hq t a p r x) (blockMatVecMul (blockMatrixOfCoeff (↑↑a x)) (diagonalWeakState hq t a p r x))

Every child contribution in the canonical state-energy partition is nonnegative.