High-contrast homogenization: Provider.Quenched.UnitRangeNormalizedLocality

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

The normalized block: locality, entry bounds, positivity

The renormalization argument applies the concentration estimate to the entries of the normalized coarse block. Three properties of that block are needed before the estimate can be used, and all three follow from the flattening toFullBlockMat (normalizedBlock H E) = E'^{-1/2} · toFullBlockMat H · E'^{-1/2}.

Locality: each entry of the normalized block is a fixed finite linear combination of the entries of the block itself, so it is measurable for the local sigma-field of the cell. Positivity: conjugation by an invertible symmetric matrix preserves positive definiteness. Entry bounds: a positive block below the scaled identity has entries bounded by the scale, which is what makes the cutoff of the previous file inactive on the burnt-in event.

The entries of the normalized block

theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_normalizedBlock_eq_sum {d : ℕ} (H E : BlockMat d) (α β : BlockCoord d) : blockMatEntry (normalizedBlock H E) α β = ∑ delta : BlockCoord d, ∑ gamma : BlockCoord d, matSqrt (toFullBlockMat E)⁻¹ α gamma * (blockMatEntry H gamma delta * matSqrt (toFullBlockMat E)⁻¹ delta β)

Each entry of the normalized block is a fixed finite linear combination of the entries of the block.

theorem HCPolySupport.HighContrast.Quenched.measurable_blockMatEntry_normalizedBlock_coarseBlock_standardCell {d : ℕ} (E : BlockMat d) (k : ℤ) (w : Fin d → ℤ) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (normalizedBlock (coarseBlock (standardCell d k w) a) E) α β

Locality of the normalized coarse block. Every entry of the normalized coarse block of a standard aligned cube is measurable for the local sigma-field of that cube.

Positivity of the normalized block

theorem HCPolySupport.HighContrast.Quenched.blockPosDef_normalizedBlock {d : ℕ} {H E : BlockMat d} (hH : IsSymmetricBlockMat H) (hHpd : Book.Ch02.BlockPosDef H) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : Book.Ch02.BlockPosDef (normalizedBlock H E)

Conjugation preserves positivity. The normalized block of a positive block is positive.

Entry bounds from a Loewner bound

theorem HCPolySupport.HighContrast.Quenched.blockEntrySum_scaledBlockIdentity {d : ℕ} (c : ℝ) : blockEntrySum (scaledBlockIdentity d c) = 2 * ↑d * |c|

theorem HCPolySupport.HighContrast.Quenched.abs_blockMatEntry_le_of_blockMatLoewnerLE_scaledBlockIdentity {d : ℕ} {M : BlockMat d} {c : ℝ} (hsymm : IsSymmetricBlockMat M) (hnn : ∀ (X : BlockVec d), 0 ≤ blockVecDot X (blockMatVecMul M X)) (hle : BlockMatLoewnerLE M (scaledBlockIdentity d c)) (α β : BlockCoord d) : |blockMatEntry M α β| ≤ 4 * ↑d * |c|

Entry bounds for a positive block below the scaled identity.

The converse transfer

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

The converse of the normalized transfer. A bound of the block against the scaled reference block is a bound of the normalized block against the scaled identity. This is what makes the cutoff inactive on the burnt-in event.

Locality of the cutoff of a local block family

theorem HCPolySupport.HighContrast.Quenched.measurable_blockMatEntry_blockCutoff_of_local {d : ℕ} {U : Set (Vec d)} (B : ℝ) {H : CoeffSpace d → BlockMat d} (hH : ∀ (alpha beta : BlockCoord d), Measurable fun (a : CoeffSpace d) => blockMatEntry (H a) alpha beta) (α β : BlockCoord d) : Measurable fun (a : CoeffSpace d) => blockMatEntry (blockCutoff B (H a)) α β

The cutoff of a local block family is local. The branch condition is a finite conjunction of conditions on entries that are local.