High-contrast homogenization: Provider.Quenched.SmallContrastSchurExtraction

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

Schur data extraction

A doubled block in Schur form has its intrinsic Schur data equal to the form's data, and the good-quadratics norm gap converts into the σ*-quadratic of the skew difference against the σ-form.

theorem HCPolySupport.HighContrast.Quenched.schurData_of_form {d : ℕ} {H : BlockMat d} {S SStar K : Mat d} (hStar : Matrix.PosDef SStar) (hform : toFullBlockMat H = schurBlock S SStar K) : H.lowerRight = SStar⁻¹ ∧ schurSigmaStar H = SStar ∧ schurSkew H = K ∧ schurSigma H = S

Schur data extraction.

theorem HCPolySupport.HighContrast.Quenched.inv_smul_posDef {d : ℕ} {A : Mat d} (hA : Matrix.PosDef A) {c : ℝ} (hc : 0 < c) : (c • A)⁻¹ = c⁻¹ • A⁻¹

The inverse of a positive scalar multiple.

theorem HCPolySupport.HighContrast.Quenched.quad_le_of_norm_normalized_le {d : ℕ} {W Sp SStarp : Mat d} (hSp : Matrix.PosDef Sp) (hStarp : Matrix.PosDef SStarp) {c : ℝ} (hnorm : ‖matSqrt SStarp⁻¹ * W * matSqrt Sp⁻¹‖ ≤ c) (x : Vec d) : Matrix.mulVec W x ⬝ᵥ SStarp⁻¹.mulVec (Matrix.mulVec W x) ≤ c ^ 2 * x ⬝ᵥ Matrix.mulVec Sp x

A spectral bound on the mixed-normalized matrix gives the quadratic comparison of the images.