Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileEnergyPointwise

High-contrast homogenization: Provider.Response.ProfileEnergyPointwise #

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

Pointwise optimizer-energy bounds from the complete maximum #

The terminal cell is one of the terms of the all-scale maximum. Its response block is consequently below (1 + M_t) E_t in quadratic form, which controls the canonical optimizer energy. The coefficient-transpose assertion follows from the signed block congruence and retains its independent load.

source
theorem HCPolySupport.HighContrast.Response.sq_profileEnergyLoad {d : ℕ} {L : ℝ} {p q : Vec d} :
profileEnergyLoad L p q ^ 2 = L ^ 2 + |vecDot p q|

The square of the response-energy load.

source
theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakEnergy_le_maximum {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) :
diagonalWeakEnergy hq t a p r ^ 2 ≤ (1 + (diagonalWeakMaximum rho q t E a).toReal) * diagonalWeakLoadMinus E p r ^ 2 + 2 * |vecDot p r|

The terminal maximum controls the primal optimizer energy.

source
theorem HCPolySupport.HighContrast.Response.sq_diagonalWeakAdjointEnergy_le_maximum {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) :
diagonalWeakAdjointEnergy hq t a p r ^ 2 ≤ (1 + (diagonalWeakMaximum rho q t E a).toReal) * diagonalWeakLoadPlus E p r ^ 2 + 2 * |vecDot p r|

The same terminal maximum controls the coefficient-transpose optimizer energy with its separate plus load.

source
theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_le_sqrt_two_mul_bad {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hbad : 1 < diagonalWeakMaximum rho q t E a) :
diagonalWeakEnergy hq t a p r ≤ √2 * √(diagonalWeakMaximum rho q t E a).toReal * profileEnergyLoad (diagonalWeakLoadMinus E p r) p r

On the bad event the primal energy costs one square root of the maximum.

source
theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_le_sqrt_two_mul_good {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hgood : diagonalWeakMaximum rho q t E a ≤ 1) :
diagonalWeakEnergy hq t a p r ≤ √2 * profileEnergyLoad (diagonalWeakLoadMinus E p r) p r

On the good event the primal energy is bounded by its deterministic load.

source
theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy_le_sqrt_two_mul_bad {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hbad : 1 < diagonalWeakMaximum rho q t E a) :
diagonalWeakAdjointEnergy hq t a p r ≤ √2 * √(diagonalWeakMaximum rho q t E a).toReal * profileEnergyLoad (diagonalWeakLoadPlus E p r) p r

On the bad event the adjoint energy costs one square root of the same maximum, with its independent plus load.

source
theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy_le_sqrt_two_mul_good {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hgood : diagonalWeakMaximum rho q t E a ≤ 1) :
diagonalWeakAdjointEnergy hq t a p r ≤ √2 * profileEnergyLoad (diagonalWeakLoadPlus E p r) p r

On the good event the adjoint energy is bounded by its deterministic plus load.

The released split level #

source
noncomputable def HCPolySupport.HighContrast.Response.energyGoodConstantAtLevel (lev : ℝ) :
ℝ

The good-event energy coefficient at a released split level.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_le_sqrt_two_mul_bad_at_level {d : ℕ} {rho lev : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hlev : 1 ≤ lev) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hbad : ENNReal.ofReal lev < diagonalWeakMaximum rho q t E a) :
    diagonalWeakEnergy hq t a p r ≤ √2 * √(diagonalWeakMaximum rho q t E a).toReal * profileEnergyLoad (diagonalWeakLoadMinus E p r) p r

    On the released bad event the primal energy costs one square root of the maximum, with the fixed-level constant.

    source
    theorem HCPolySupport.HighContrast.Response.diagonalWeakEnergy_le_sqrt_two_mul_good_at_level {d : ℕ} {rho lev : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hlev : 1 ≤ lev) (hgood : diagonalWeakMaximum rho q t E a ≤ ENNReal.ofReal lev) :
    diagonalWeakEnergy hq t a p r ≤ energyGoodConstantAtLevel lev * profileEnergyLoad (diagonalWeakLoadMinus E p r) p r

    On the released good event the primal energy is bounded by its deterministic load, at the coefficient √(1+lev).

    source
    theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy_le_sqrt_two_mul_bad_at_level {d : ℕ} {rho lev : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hlev : 1 ≤ lev) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hbad : ENNReal.ofReal lev < diagonalWeakMaximum rho q t E a) :
    diagonalWeakAdjointEnergy hq t a p r ≤ √2 * √(diagonalWeakMaximum rho q t E a).toReal * profileEnergyLoad (diagonalWeakLoadPlus E p r) p r

    The adjoint mirror on the released bad event.

    source
    theorem HCPolySupport.HighContrast.Response.diagonalWeakAdjointEnergy_le_sqrt_two_mul_good_at_level {d : ℕ} {rho lev : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (p r : Vec d) (hlev : 1 ≤ lev) (hgood : diagonalWeakMaximum rho q t E a ≤ ENNReal.ofReal lev) :
    diagonalWeakAdjointEnergy hq t a p r ≤ energyGoodConstantAtLevel lev * profileEnergyLoad (diagonalWeakLoadPlus E p r) p r

    The adjoint mirror on the released good event.