High-contrast homogenization: Provider.Response.LoadCalibrationSchur

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

Schur coordinates of the terminal response block

The first layer of the response-load calibration. The printed calibration writes the unrecentered terminal block in its unique Schur form

E_t = (S + KᵗS_*⁻¹K, -KᵗS_*⁻¹; -S_*⁻¹K, S_*⁻¹),   S, S_* > 0,

and then works with the response, rather than canonical, coordinates h = ½(K - Kᵗ), r = ½(K + Kᵗ), B = S + rᵗS_*⁻¹r, m = B # S_*, and the response ratio θ = |S_*^{-1/2}BS_*^{-1/2}|.

This file supplies the two Schur orderings that the proof reads off the sharp ordering E_t^♯ ≤ E_t and the imbalance ordering E_t ≤ κ_t E_t^♯, in a form free of any vector manipulation: conjugating by the shear G_{-Kᵗ} sends both E_t and E_t^♯ to blocks whose upper-left corners are exactly the two sides of the wanted scalar comparison. Writing 𝐊 = K + Kᵗ = 2r,

G_{-Kᵗ}ᵗ E_t^♯ G_{-Kᵗ} = diag(S_*, S⁻¹),
G_{-Kᵗ}ᵗ E_t  G_{-Kᵗ} = schurBlock S S_* 𝐊,

so the sharp ordering gives S_* ≤ S (through the lower-right corners, where the two blocks are S⁻¹ and S_*⁻¹) and the imbalance ordering gives S + 𝐊ᵗS_*⁻¹𝐊 ≤ κ_t S_* (through the upper-left corners). Since 𝐊ᵗS_*⁻¹𝐊 = 4 rᵗS_*⁻¹r this is a fourfold strengthening of B ≤ κ_t S_*, which is the response-ratio bound θ ≤ κ_t of the printed chain 1 ≤ θ ≤ (3κ_t-1)/2.

Route note. The printed derivation of θ ≤ (3κ_t-1)/2 runs through [Armstrong–Kuusi, (2.81)] and the upper half of [Armstrong–Kuusi, (2.82)], both of which are false as printed (the counterexample at Schur data σ_* = 1, σ = 9, k = 4 exceeds both). The route here does not use them: it reads the imbalance ordering once, at the vector whose second Schur coordinate vanishes, and yields the strictly stronger θ ≤ κ_t; the printed (3κ_t-1)/2 then follows from 1 ≤ κ_t.

There are no definitions in this file.

Shear conjugation of the Schur form

theorem HCPolySupport.HighContrast.Response.schurBlock_conj_shear {d : ℕ} (s sStar k c : Mat d) : Matrix.conjTranspose (fullBlockShear c) * schurBlock s sStar k * fullBlockShear c = schurBlock s sStar (k - c)

Conjugation by a shear translates the skew coordinate. The Schur form is G_{-k}ᵗ diag(s, s_*⁻¹) G_{-k}, and shears compose additively.

theorem HCPolySupport.HighContrast.Response.schurBlock_zero {d : ℕ} (s sStar : Mat d) : schurBlock s sStar 0 = Matrix.fromBlocks s 0 0 sStar⁻¹

The Schur form at a vanishing skew coordinate is the diagonal block.

theorem HCPolySupport.HighContrast.Response.conj_smul {d : ℕ} (C X : Matrix (BlockCoord d) (BlockCoord d) ℝ) (c : ℝ) : C.conjTranspose * c • X * C = c • (C.conjTranspose * X * C)

Conjugation commutes with the scalar dilation.

The two Schur orderings

theorem HCPolySupport.HighContrast.Response.schurBlock_doubled_le_smul_diag {d : ℕ} {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) {c : ℝ} (h : schurBlock S SStar K ≤ c • fullBlockSharp (schurBlock S SStar K)) : schurBlock S SStar (K + Matrix.conjTranspose K) ≤ c • Matrix.fromBlocks SStar 0 0 S⁻¹

The imbalance ordering in doubled Schur coordinates.

The two scalar consequences

theorem HCPolySupport.HighContrast.Response.schurStar_le_schur {d : ℕ} {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hsharp : fullBlockSharp (schurBlock S SStar K) ≤ schurBlock S SStar K) : SStar ≤ S

The Schur ordering S_* ≤ S, from the lower-right corners of the sharp ordering: there they are S⁻¹ ≤ S_*⁻¹.

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

The fourfold upper-left bound. From E_t ≤ c E_t^♯ the upper-left corners of the conjugated blocks give S + 𝐊ᵗS_*⁻¹𝐊 ≤ c S_*, with 𝐊 = K + Kᵗ.