High-contrast homogenization: Provider.Response.ProfileWeakPointwise

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

Pointwise weak-profile estimates

The diagonal weak estimate is separated into its recent, bad-energy, and good-energy terms. The maximum is assumed finite only at the sample under consideration; the probabilistic argument supplies this almost everywhere.

theorem HCPolySupport.HighContrast.Response.profilePrimalWeakRoot_randomCentered_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (halpha : alpha = (1 - rho) / 2) (a : CoeffSpace d) (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) : profilePrimalWeakRoot m hq t id p r (blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r)) a ≤ ENNReal.ofReal (16 * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r) * (ENNReal.ofReal (diagonalWeakCellSum q t H (1 / 2) E a) + ENNReal.ofReal (diagonalWeakAverageSum q t H (1 / 2) rho E a)) + ENNReal.ofReal (16 * diagonalWeakMetricFactor m E / (2 * alpha)) * if 1 < diagonalWeakMaximum rho q t E a then diagonalWeakMaximum rho q t E a ^ (1 / 2) * ENNReal.ofReal (diagonalWeakEnergy hq t a p r) else ENNReal.ofReal (3 ^ (-alpha * ↑H)) * ENNReal.ofReal (diagonalWeakEnergy hq t a p r)

The primal random-centered weak root splits pointwise into the recent terms and the two optimizer-energy events.

theorem HCPolySupport.HighContrast.Response.profileAdjointWeakRoot_randomCentered_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (halpha : alpha = (1 - rho) / 2) (a : CoeffSpace d) (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) : profileAdjointWeakRoot m hq t id p r (blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t a p r)) a ≤ ENNReal.ofReal (16 * diagonalWeakMetricFactor m E * diagonalWeakLoadPlus E p r) * (ENNReal.ofReal (diagonalWeakCellSum q t H (1 / 2) E a) + ENNReal.ofReal (diagonalWeakAverageSum q t H (1 / 2) rho E a)) + ENNReal.ofReal (16 * diagonalWeakMetricFactor m E / (2 * alpha)) * if 1 < diagonalWeakMaximum rho q t E a then diagonalWeakMaximum rho q t E a ^ (1 / 2) * ENNReal.ofReal (diagonalWeakAdjointEnergy hq t a p r) else ENNReal.ofReal (3 ^ (-alpha * ↑H)) * ENNReal.ofReal (diagonalWeakAdjointEnergy hq t a p r)

The coefficient-transpose optimizer has the same pointwise split with its independent plus load and adjoint energy.

The released split level

theorem HCPolySupport.HighContrast.Response.profilePrimalWeakRoot_randomCentered_at_level_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha lev : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (hlev : 0 < lev) (halpha : alpha = (1 - rho) / 2) (a : CoeffSpace d) (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) : profilePrimalWeakRoot m hq t id p r (blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r)) a ≤ ENNReal.ofReal (recentConstantAtLevel lev * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r) * (ENNReal.ofReal (diagonalWeakCellSum q t H (1 / 2) E a) + ENNReal.ofReal (diagonalWeakAverageSum q t H (1 / 2) rho E a)) + ENNReal.ofReal (maxGroupConstantAtLevel lev * diagonalWeakMetricFactor m E / (2 * alpha)) * if ENNReal.ofReal lev < diagonalWeakMaximum rho q t E a then diagonalWeakMaximum rho q t E a ^ (1 / 2) * ENNReal.ofReal (diagonalWeakEnergy hq t a p r) else ENNReal.ofReal (3 ^ (-alpha * ↑H)) * ENNReal.ofReal (diagonalWeakEnergy hq t a p r)

The primal random-centered weak root at a released split level.

theorem HCPolySupport.HighContrast.Response.profileAdjointWeakRoot_randomCentered_at_level_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho alpha lev : ℝ} (hrho : 0 < rho) (hrho1 : rho < 1) (hlev : 0 < lev) (halpha : alpha = (1 - rho) / 2) (a : CoeffSpace d) (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) : profileAdjointWeakRoot m hq t id p r (blockCellAverage (adaptedCell q t) (diagonalWeakAdjointState hq t a p r)) a ≤ ENNReal.ofReal (recentConstantAtLevel lev * diagonalWeakMetricFactor m E * diagonalWeakLoadPlus E p r) * (ENNReal.ofReal (diagonalWeakCellSum q t H (1 / 2) E a) + ENNReal.ofReal (diagonalWeakAverageSum q t H (1 / 2) rho E a)) + ENNReal.ofReal (maxGroupConstantAtLevel lev * diagonalWeakMetricFactor m E / (2 * alpha)) * if ENNReal.ofReal lev < diagonalWeakMaximum rho q t E a then diagonalWeakMaximum rho q t E a ^ (1 / 2) * ENNReal.ofReal (diagonalWeakAdjointEnergy hq t a p r) else ENNReal.ofReal (3 ^ (-alpha * ↑H)) * ENNReal.ofReal (diagonalWeakAdjointEnergy hq t a p r)

The adjoint random-centered weak root at a released split level.