High-contrast homogenization: Provider.Transport.CellDomination

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

Domination of an adapted response by a reference block

The well-definedness paragraph of p.two.grid.transport reads one pathwise inequality — the coarse response of an adapted cell lies below a multiple of the reference block 𝐄 — and extracts from it everything the printed quantities need in order to denote. Two extractions are needed, and both are recorded here in the generality in which the transport uses them, with no probability in sight.

The first is entrywise: a symmetric doubled block whose quadratic form is caught between zero and that of c𝐄 has all its entries bounded by 2|c| times the entry scale of 𝐄. That is what makes the annealed block an expectation.

The second is the centered Schatten size at the block's own normalization. Writing G_hat = E^{-1/2}𝐀E^{-1/2} for the normalized response, the centered normalization is G_hat - I; it is above -I for free, since G_hat is positive semidefinite, and it is below tI as soon as tr G_hat ≤ t, a positive semidefinite matrix being below its own trace. The scalar Loewner sandwich -(1+|t|)I ≤ G_hat - I ≤ (1+|t|)I then gives the Schatten size directly. The trace hypothesis is in turn a consequence of the same Loewner bound, the congruence by E^{-1/2} being order preserving and the trace monotone.

The entrywise bound

theorem HCPolySupport.HighContrast.Transport.abs_blockMatEntry_coarseBlock_le_of_blockMatLoewnerLE {d : ℕ} {U : Set (Vec d)} {a : CoeffSpace d} {c : ℝ} {E : BlockMat d} (hle : BlockMatLoewnerLE (coarseBlock U a) (blockScale c E)) (α β : BlockCoord d) : |blockMatEntry (coarseBlock U a) α β| ≤ 2 * (|c| * blockEntrySum E)

The entrywise bound on a dominated coarse response. A coarse response below c𝐄 in the Loewner order has every entry bounded by 2|c| times the entry scale of the reference block; the lower bound comes from the response's own positivity, which needs no hypothesis.

The centered Schatten size

theorem HCPolySupport.HighContrast.Transport.trace_toFullBlockMat_normalizedBlock_le {d : ℕ} {A Em Eref : BlockMat d} (hEmpd : Matrix.PosDef (toFullBlockMat Em)) {c : ℝ} (hle : toFullBlockMat A ≤ c • toFullBlockMat Eref) : Matrix.trace (toFullBlockMat (normalizedBlock A Em)) ≤ c * Matrix.trace (toFullBlockMat (normalizedBlock Eref Em))

The trace of a normalized block is monotone in the block. The congruence by E^{-1/2} preserves the Loewner order and the trace is monotone, so a Loewner bound 𝐀 ≤ c𝐄 becomes the scalar bound tr(E^{-1/2}𝐀E^{-1/2}) ≤ c·tr(E^{-1/2}𝐄E^{-1/2}).

theorem HCPolySupport.HighContrast.Transport.schattenSize_blockSub_le_of_trace_le {d : ℕ} {Q : ℝ} (hQ : 0 < Q) {A Em : BlockMat d} (hA : IsSymmetricBlockMat A) (hApsd : Matrix.PosSemidef (toFullBlockMat A)) (hEm : IsSymmetricBlockMat Em) (hEmpd : Matrix.PosDef (toFullBlockMat Em)) {t : ℝ} (ht : Matrix.trace (toFullBlockMat (normalizedBlock A Em)) ≤ t) : schattenSize Q (blockSub A Em) Em ≤ (2 * ↑d) ^ Q⁻¹ * (1 + |t|)

The centered Schatten size from a trace bound. The normalized response G_hat = E^{-1/2}𝐀E^{-1/2} is positive semidefinite, hence below (tr G_hat)I; if its trace is at most t, the centered normalization G_hat - I is caught between ∓(1+|t|)I, and the Schatten size of a block in such a sandwich is at most (2d)^{1/Q} times the width.