Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileWeakSplit

High-contrast homogenization: Provider.Response.ProfileWeakSplit #

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

Replacing the random optimizer average by its annealed center #

At every scale, the optimizer state centered at a deterministic vector splits as the state centered at its random parent average plus a fixed field. The scale-average triangle inequality and the exact fixed-field computation give the corresponding normalized seminorm bound.

source
theorem HCPolySupport.HighContrast.Response.blockCellAverage_metricRoot_sub_const_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) (c : BlockVec d) :
(blockCellAverage (adaptedCellAt q k w) fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (diagonalWeakState hq t a p r x - c)) = blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r) - c)

Averaging the metric-root image of a state minus an arbitrary fixed vector commutes with both operations.

source
theorem HCPolySupport.HighContrast.Response.profilePrimalWeakRoot_le_randomCentered_add_constant {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {m : Mat d} (hm : Matrix.PosDef m) (a : CoeffSpace d) (p r : Vec d) (center : BlockVec d) :
profilePrimalWeakRoot m hq t id p r center a ≤ (ENNReal.ofReal (3 ^ (-(1 / 2 * ↑t))) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag (matSqrt m) (matSqrt m)⁻¹) (diagonalWeakState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) + ENNReal.ofReal constantSeminormCoefficient * ENNReal.ofReal √(metricBlockNormSq m (blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r) - center))

The primal normalized weak root splits into its random-centered part and the exact constField correction.

source
theorem HCPolySupport.HighContrast.Response.profileAdjointWeakRoot_le_randomCentered_add_constant {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {m : Mat d} (hm : Matrix.PosDef m) (a : CoeffSpace d) (p r : Vec d) (center : BlockVec d) :
profileAdjointWeakRoot m hq t id p r center a ≤ (ENNReal.ofReal (3 ^ (-(1 / 2 * ↑t))) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag (matSqrt m) (matSqrt m)⁻¹) (diagonalWeakAdjointState hq t a p r x - blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t a p r))) + ENNReal.ofReal constantSeminormCoefficient * ENNReal.ofReal √(metricBlockNormSq m (blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t a p r) - center))

The adjoint normalized weak root has the analogous split.