High-contrast homogenization: Provider.Quenched.UnitRangeNormalizedTransfer

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

Normalized coordinates and the Loewner order

The concentration estimate bounds the entries of a doubled block, and the reassembly turns entrywise bounds into a Loewner bound against a reference block dominating the identity form. The renormalization argument needs the bound against the reference block of the coarse-ellipticity datum instead, and that block carries no coercivity constant.

The printed argument avoids the difficulty by working in normalized coordinates throughout: it bounds the entries of the normalized block and reads the result against the identity, which un-normalizes to the reference block. This file supplies the missing step, that conjugation by the square root of the reference block preserves the Loewner order, and the entrywise consequence the renormalization argument consumes.

The scaled identity block

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_scaledBlockIdentity {d : ℕ} (c : ℝ) (α β : BlockCoord d) : blockMatEntry (scaledBlockIdentity d c) α β = if α = β then c else 0

theorem HCPolySupport.HighContrast.Quenched.toFullBlockMat_scaledBlockIdentity {d : ℕ} (c : ℝ) : toFullBlockMat (scaledBlockIdentity d c) = c • 1

theorem HCPolySupport.HighContrast.Quenched.blockVecDot_scaledBlockIdentity {d : ℕ} (c : ℝ) (X : BlockVec d) : blockVecDot X (blockMatVecMul (scaledBlockIdentity d c) X) = c * ∑ α : BlockCoord d, toFullBlockVec X α * toFullBlockVec X α

The quadratic form of the scaled identity block.

theorem HCPolySupport.HighContrast.Quenched.isSymmetricBlockMat_scaledBlockIdentity {d : ℕ} (c : ℝ) : IsSymmetricBlockMat (scaledBlockIdentity d c)

Conjugation preserves the Loewner order

theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_blockScale_of_normalizedBlock {d : ℕ} {D E : BlockMat d} (hD : IsSymmetricBlockMat D) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {kappa : ℝ} (h : BlockMatLoewnerLE (normalizedBlock D E) (scaledBlockIdentity d kappa)) : BlockMatLoewnerLE D (blockScale kappa E)

The normalized block transfers the Loewner order. A bound of the normalized block against the scaled identity is a bound of the block itself against the scaled reference block: conjugation by the square root of the reference block preserves the order.

The entrywise consequence