Documentation

LeanPool.HighContrastHomogenization.Provider.Bridge.ComparisonMatrixRows

High-contrast homogenization: Provider.Bridge.ComparisonMatrixRows #

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

Matrix rows for two-grid comparison #

Each positive increment is measured by its trace in the terminal geometry. The scalar boundary-row estimate then lifts directly to a Loewner estimate for the corresponding weighted row of adapted means.

source
theorem HCPolySupport.HighContrast.Bridge.posSemidef_le_trace_inv_smul {d : ℕ} {A G : FullBlockMat d} (hA : Matrix.PosDef A) (hG : Matrix.PosSemidef G) :
G ≤ (A⁻¹ * G).trace • A

A positive semidefinite matrix is bounded by its trace in any positive terminal geometry.

source
theorem HCPolySupport.HighContrast.Bridge.matrix_le_terminal_trace_sub {d : ℕ} {A B : FullBlockMat d} (hB : Matrix.PosDef B) (hBA : B ≤ A) :
A ≤ (1 + (B⁻¹ * (A - B)).trace) • B

An earlier positive mean is bounded by the terminal mean and the trace of their positive difference in the terminal geometry.