High-contrast homogenization: Provider.Response.LoadCalibrationTheta

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

The response ratio against the canonical imbalance

The response-ratio calibration of the response loads, read through the canonical imbalance e.response.canonical.imbalance:

1 ≤ θ ≤ (3κ_t - 1)/2,      κ_t - 1 ≤ 6(θ - 1),

for θ = |S_*^{-1/2}BS_*^{-1/2}|, B = S + rᵗS_*⁻¹r, r = ½(K + Kᵗ), and κ_t = 𝔡(E_t) the canonical imbalance of the terminal block.

The two halves go in opposite directions and are proved by different routes.

• θ ≤ κ_t (hence θ ≤ (3κ_t-1)/2, since 1 ≤ κ_t) is read directly off the imbalance ordering E_t ≤ κ_t E_t^♯ at the vector whose second Schur coordinate vanishes: this is the fourfold bound S + 𝐊ᵗS_*⁻¹𝐊 ≤ κ_t S_* of LoadCalibrationSchur, and B is smaller than its left side because 𝐊ᵗS_*⁻¹𝐊 = 4rᵗS_*⁻¹r.

• κ_t ≤ 1 + 6(θ - 1) is the repaired reference intermediate Initialization.kappaRef_le_of_matLoewnerLE_skewCorrectedForm, applied at the skew h = ½(K - Kᵗ), for which the skew-corrected Schur form is exactly B and the admissible scaling is exactly θ.

Route note. The printed proof obtains both halves from [Armstrong–Kuusi, (2.81),(2.82)] through the uncorrected ratio θ_tilde = |S_*^{-1/2}SS_*^{-1/2}|. Both of those displays are false as printed — the counterexample σ_* = 1, σ = 9, k = 4 gives 64 > 16 in (2.81) and 80 > 48 in the upper half of (2.82) — and neither is used here. The conclusions of the printed lemma are unchanged; only the route is.

There are no definitions in this file.

A norm identity above the identity

theorem HCPolySupport.HighContrast.Response.norm_sub_one_eq_norm_sub_one {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {X : Matrix n n ℝ} (hX : X.PosSemidef) (h1 : 1 ≤ X) : ‖X - 1‖ = ‖X‖ - 1

‖X - I‖ = ‖X‖ - 1 above the identity. If X is positive semidefinite and I ≤ X, then subtracting the identity subtracts one from the spectral norm. This is the display |S_*^{-1/2}BS_*^{-1/2} - Id| = θ - 1.

theorem HCPolySupport.HighContrast.Response.conjTranspose_eq_matTranspose {d : ℕ} (A : Mat d) : Matrix.conjTranspose A = matTranspose A

On real data the ambient transpose is mathlib's conjugate transpose.

The response coordinates

theorem HCPolySupport.HighContrast.Response.conjTranspose_response_sym {d : ℕ} {K r : Mat d} (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) : Matrix.conjTranspose r = r

The symmetric response coordinate r = ½(K + Kᵗ) is symmetric.

theorem HCPolySupport.HighContrast.Response.doubled_eq_four_smul {d : ℕ} {SStar K r : Mat d} (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) : Matrix.conjTranspose (K + Matrix.conjTranspose K) * SStar⁻¹ * (K + Matrix.conjTranspose K) = 4 • (Matrix.conjTranspose r * SStar⁻¹ * r)

The doubled skew coordinate against S_*⁻¹ is four times the response one: 𝐊ᵗS_*⁻¹𝐊 = 4 rᵗS_*⁻¹r.

theorem HCPolySupport.HighContrast.Response.posSemidef_responseBlock {d : ℕ} {S SStar r B : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) : Matrix.PosSemidef B

The response block B = S + rᵗS_*⁻¹r is positive semidefinite.

theorem HCPolySupport.HighContrast.Response.schurStar_le_responseBlock {d : ℕ} {S SStar K r B : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) (hsharp : fullBlockSharp (schurBlock S SStar K) ≤ schurBlock S SStar K) : SStar ≤ B

S_* ≤ B: the response block dominates the Schur block it corrects.

The response ratio is at least one

theorem HCPolySupport.HighContrast.Response.one_le_response_ratio {d : ℕ} {S SStar K r B : Mat d} [NeZero d] (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) (hsharp : fullBlockSharp (schurBlock S SStar K) ≤ schurBlock S SStar K) : 1 ≤ relSize B SStar

1 ≤ θ in the response-load calibration: the printed step B ≥ S ≥ S_*.

The response ratio against the imbalance

theorem HCPolySupport.HighContrast.Response.responseBlock_le_smul {d : ℕ} {S SStar K r B : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) {c : ℝ} (h : schurBlock S SStar K ≤ c • fullBlockSharp (schurBlock S SStar K)) : B ≤ c • SStar

B ≤ c S_* from E_t ≤ c E_t^♯. The fourfold Schur bound with three of its four parts discarded.

theorem HCPolySupport.HighContrast.Response.response_ratio_le_canonImbalance {d : ℕ} {S SStar K r B : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) : relSize B SStar ≤ canonImbalance (schurBlock S SStar K)

θ ≤ κ_t — the strengthened form of the printed θ ≤ (3κ_t - 1)/2.

theorem HCPolySupport.HighContrast.Response.response_ratio_le_printed {d : ℕ} {S SStar K r B : Mat d} [NeZero d] (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) (hsharp : fullBlockSharp (schurBlock S SStar K) ≤ schurBlock S SStar K) : relSize B SStar ≤ (3 * canonImbalance (schurBlock S SStar K) - 1) / 2

The printed upper bound θ ≤ (3κ_t - 1)/2 of the response-load calibration, from θ ≤ κ_t and 1 ≤ κ_t.

The imbalance against the response ratio

theorem HCPolySupport.HighContrast.Response.canonImbalance_le_one_add_six_mul_sub_one {d : ℕ} {S SStar K r B : Mat d} [NeZero d] (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) (hsharp : fullBlockSharp (schurBlock S SStar K) ≤ schurBlock S SStar K) : canonImbalance (schurBlock S SStar K) ≤ 1 + 6 * (relSize B SStar - 1)

κ_t ≤ 1 + 6(θ - 1), through the repaired reference intermediate at the skew h = ½(K - Kᵗ).