High-contrast homogenization: Provider.Quenched.StoppingRadiusCellExcess #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The normalized cell excess below the stopping radius #
Below the stopping radius of a generation the window supplies a discounted
Loewner bound against that generation's reference block. Comparing the
reference block with the homogenized block turns it into a bound on the
normalized excess, which is the quantity the weighted row of
e.random.quenched.row sums. The comparison of the two
blocks is the only input this file does not prove.
theorem
HCPolySupport.HighContrast.Quenched.blockScale_blockScale
{d : ℕ}
(c c' : ℝ)
(A : BlockMat d)
:
Rescaling a doubled block twice is rescaling once by the product.
theorem
HCPolySupport.HighContrast.Quenched.blockExcess_le_of_blockMatLoewnerLE
{d : ℕ}
{H E Abar : BlockMat d}
(hH : IsSymmetricBlockMat H)
(hHps : Matrix.PosSemidef (toFullBlockMat H))
(hAbar : IsSymmetricBlockMat Abar)
(hAbarpd : Book.Ch02.BlockPosDef Abar)
{s c : ℝ}
(hs : 0 ≤ s)
(hc : 0 ≤ c)
(hcell : BlockMatLoewnerLE H (blockScale s E))
(hcomp : BlockMatLoewnerLE E (blockScale c Abar))
:
A discounted Loewner bound against a reference block, together with a comparison of that block with the homogenized one, bounds the normalized excess.