High-contrast homogenization: Provider.Quenched.SmallContrastTraceBridge

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

Trace scalarization for the sharp fluctuation

The sharp fluctuation has a normalized trace consisting of the hatted Schur defect and a separate term measuring the symmetric part of the Schur coupling. The latter term is retained explicitly.

theorem HCPolySupport.HighContrast.Quenched.schur_trace_gaps_le_hattedContrast_drop {d : ℕ} [NeZero d] {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) (hCsharp : BlockMatLoewnerLE (blockSharp C) C) : ((schurSigma F - schurSigma C) * (schurSigma C)⁻¹).trace + ((F.lowerRight - C.lowerRight) * C.lowerRight⁻¹).trace ≤ ↑d * (hattedContrast F - hattedContrast C)

The drop of the hatted carrier controls the sum of the two normalized Schur trace gaps. The first gap measures the upper Schur block relative to its coarse value, and the second measures the lower-right block relative to its coarse value.

theorem HCPolySupport.HighContrast.Quenched.normalized_schur_norm_gaps_le_hattedContrast_drop {d : ℕ} [NeZero d] {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) (hCsharp : BlockMatLoewnerLE (blockSharp C) C) : ‖matSqrt (schurSigma C)⁻¹ * schurSigma F * matSqrt (schurSigma C)⁻¹ - 1‖ + ‖matSqrt C.lowerRight⁻¹ * F.lowerRight * matSqrt C.lowerRight⁻¹ - 1‖ ≤ ↑d * (hattedContrast F - hattedContrast C)

Operator-norm form of the two Schur scale gaps. It is the first branch of the good-quadratics estimate: both relative matrices lie above the identity, so their spectral gaps are bounded by their trace gaps.

theorem HCPolySupport.HighContrast.Quenched.schurSkew_diff_shear_inequality {d : ℕ} {C F : BlockMat d} (hCsymm : IsSymmetricBlockMat C) (hCpos : Book.Ch02.BlockPosDef C) (hFsymm : IsSymmetricBlockMat F) (hFpos : Book.Ch02.BlockPosDef F) (hCF : BlockMatLoewnerLE C F) (eta : ℝ) : eta ^ 2 • (Matrix.conjTranspose (schurSkew F - schurSkew C) * C.lowerRight * (schurSkew F - schurSkew C)) ≤ schurSigma F - schurSigma C + (1 - eta) ^ 2 • (Matrix.conjTranspose (schurSkew F - schurSkew C) * F.lowerRight * (schurSkew F - schurSkew C))

A common shear of two ordered Schur blocks gives the quadratic comparison used to control the change of their Schur couplings.