High-contrast homogenization: Provider.Response.DiagonalWeakNormCentering #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Centering the optimizer state inside the weak seminorm #
On every aligned child, averaging commutes with both subtraction of the parent mean and the fixed block-diagonal metric root. This identifies the field in the weak seminorm with the centered scale quantity estimated variationally.
theorem
HCPolySupport.HighContrast.Response.blockCellAverage_metricRoot_centered_diagonalWeakState
{d : ℕ}
{q : Mat d}
(hq : Matrix.PosDef q)
{k t : ℤ}
(hkt : k ≤ t)
{w : Fin d → ℤ}
(hw : w ∈ alignedIndex q k t)
{S : Mat d}
{a : CoeffSpace d}
(p r : Vec d)
:
(blockCellAverage (adaptedCellAt q k w) fun (x : Vec d) =>
blockMatVecMul (Book.Ch02.blockDiag S S⁻¹)
(diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) = 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))
The average on one child of the metric-root image of the centered canonical state is the metric-root image of the difference of averages.
theorem
HCPolySupport.HighContrast.Response.normalized_scaleTerm_metricRoot_centered_diagonalWeakState_le
{d : ℕ}
[NeZero d]
{q : Mat d}
(hq : Matrix.PosDef q)
(t : ℤ)
(s : ℝ)
{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 ≠ ⊤)
(j : ℕ)
:
(3 ^ (-(s * ↑j)) * blockAvsumL2 (alignedIndex q (t - ↑j) t) fun (w : Fin d → ℤ) =>
blockCellAverage (adaptedCellAt q (t - ↑j) w) fun (x : Vec d) =>
blockMatVecMul (Book.Ch02.blockDiag S S⁻¹)
(diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ √2 * diagonalWeakMetricFactor m E * (3 ^ (-(s * ↑j)) + √(diagonalWeakMaximum rho q t E a).toReal * 3 ^ (-((s - rho / 2) * ↑j))) * diagonalWeakEnergy hq t a p r
The normalized inner scale term of the centered metric-root field obeys the variational scale-energy majorant.