High-contrast homogenization: Provider.Transport.WindowCenteredBound

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

The centered bound for a dominated cell

The centered displays of e.source.adapted.bound — the centered L^Q bound for the early target cells and its source-tail form — rest on one pathwise inequality, the normalized centered bound e.two.grid.whitney.centered.split: if a response and its mean are both below multiples of the reference block, then the Schatten size of the centered response, normalized by any positive block F, is at most (2d)^{1/Q}Λ(F;𝐄) times the sum of the two multiples.

Only two facts enter. A symmetric block caught between ∓tF has normalized Schatten size at most (2d)^{1/Q}t, because the congruence by F^{-1/2} turns the sandwich into a sandwich against the identity and the Schatten norm of such a block is read off its 2d eigenvalues. And a difference of two positive blocks, each below a multiple of F, is caught between the two multiples with opposite signs — the centered block is never larger than either of its parts.

No cancellation is claimed: this is the crude bound, and the constant it produces is the one the printed clause writes as C_{d,Q}.

theorem HCPolySupport.HighContrast.Transport.toFullBlockMat_blockSub {d : ℕ} (A B : BlockMat d) : toFullBlockMat (blockSub A B) = toFullBlockMat A - toFullBlockMat B

Flattening a difference of doubled blocks is the difference of the flattenings.

theorem HCPolySupport.HighContrast.Transport.schattenSize_le_of_sandwich {d : ℕ} {Q : ℝ} (hQ : 0 < Q) {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {t : ℝ} (ht : 0 ≤ t) (hup : toFullBlockMat H ≤ t • toFullBlockMat F) (hlo : -t • toFullBlockMat F ≤ toFullBlockMat H) : schattenSize Q H F ≤ (2 * ↑d) ^ Q⁻¹ * t

A two-sided Loewner sandwich bounds the normalized Schatten size. The congruence by F^{-1/2} carries the sandwich -tF ≤ H ≤ tF onto a sandwich against the identity, where the Schatten norm is at most (2d)^{1/Q}t.

theorem HCPolySupport.HighContrast.Transport.schattenSize_blockSub_le_of_bounds {d : ℕ} {Q : ℝ} (hQ : 0 < Q) {A Am Eref F : BlockMat d} (hA : IsSymmetricBlockMat A) (hAps : Matrix.PosSemidef (toFullBlockMat A)) (hAm : IsSymmetricBlockMat Am) (hAmps : Matrix.PosSemidef (toFullBlockMat Am)) (hEref : IsSymmetricBlockMat Eref) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {s u : ℝ} (hs : 0 ≤ s) (hu : 0 ≤ u) (hAle : BlockMatLoewnerLE A (blockScale s Eref)) (hAmle : BlockMatLoewnerLE Am (blockScale u Eref)) : schattenSize Q (blockSub A Am) F ≤ (2 * ↑d) ^ Q⁻¹ * (blockSize Eref F * (s + u))

The centered cell bound. A response and its mean, each below a multiple of the reference block and each positive, have a centered difference whose normalized Schatten size is at most (2d)^{1/Q}Λ(F;𝐄) times the sum of the two multiples.