High-contrast homogenization: Provider.Response.LoadCalibrationMetric

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

The calibrated canonical sandwich

The first two boxed displays of the response-load calibration:

β⁻¹ 𝐌₀ ≤ 𝐆₀ᵗ M(E_t) 𝐆₀ ≤ β 𝐌₀,      κ_t ≤ ϱ^d κ_s,   κ_s ≤ ϱ^{2d} κ_t,

together with the two canonical-balance chains the later displays consume,

β⁻¹ 𝐌₀ ≤ Ê_t ≤ β√κ_t 𝐌₀,            Ê_s ≤ c_ε √κ_s 𝐌₀.

Here E⁰, E_s, E_t are positive doubled blocks with E_t ≤ E_s, E_s^♯ ≤ E_s, E_t^♯ ≤ E_t, and (1-ε_cal)E⁰ ≤ E_s ≤ (1+ε_cal)E⁰; c_ε = ((1+ε_cal)/(1-ε_cal))^{1/2}, ϱ = (det E_s/det E_t)^{1/d}, β = c_ε ϱ^{d/2}, and 𝐆₀ = G_{g(E⁰)}, 𝐌₀ = diag(m(E⁰), m(E⁰)⁻¹).

The proof is the printed one. Sharp order reversal turns the near-isometry hypothesis into a comparison of sharps; joint monotonicity and homogeneity of the metric geometric mean turn that into c_ε⁻¹ M(E⁰) ≤ M(E_s) ≤ c_ε M(E⁰), the comparison of the canonical metrics of two near-isometric blocks. The determinant-loss comparison e.global.selection.metric.loss at the ordered pair (E_s, E_t) supplies ϱ^{-d/2} M(E_t) ≤ M(E_s) ≤ ϱ^{d/2} M(E_t) and the two imbalance clauses. Composing gives the sandwich around M(E⁰), and congruence by 𝐆₀ moves it onto 𝐌₀, because M(E⁰) = G_{-g₀}ᵗ 𝐌₀ G_{-g₀} and G_{-g₀}G_{g₀} = I.

There are no definitions in this file.

Scalar dilation helpers

theorem HCPolySupport.HighContrast.Response.le_of_smul_inv_le {n : Type u_1} {c : ℝ} (hc : 0 < c) {A B : Matrix n n ℝ} (h : c⁻¹ • A ≤ B) : A ≤ c • B

Cancel a positive dilation on the left of a Loewner bound.

The near-isometric mean comparison

theorem HCPolySupport.HighContrast.Response.canonBlock_near_isometry {d : ℕ} {E0 Es : FullBlockMat d} (hE0 : Matrix.PosDef E0) (hEs : Matrix.PosDef Es) {z : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (hlow : (1 - z) • E0 ≤ Es) (hhigh : Es ≤ (1 + z) • E0) : (√((1 + z) / (1 - z)))⁻¹ • canonBlock E0 ≤ canonBlock Es ∧ canonBlock Es ≤ √((1 + z) / (1 - z)) • canonBlock E0

The near-isometric mean comparison of the canonical metrics: c_ε⁻¹ M(E⁰) ≤ M(E_s) ≤ c_ε M(E⁰) with c_ε = ((1+ζ)/(1-ζ))^{1/2}. This is the internal step of e.global.selection.metric.comparison, which reports only the imbalance and projective consequences.

Congruence by the canonical shear

theorem HCPolySupport.HighContrast.Response.shear_conj_canonBlock {d : ℕ} {E0 : FullBlockMat d} (hE0 : Matrix.PosDef E0) : Matrix.conjTranspose (fullBlockShear (canonShear E0)) * canonBlock E0 * fullBlockShear (canonShear E0) = Matrix.fromBlocks (canonMetric E0) 0 0 (canonMetric E0)⁻¹

The canonical block is 𝐌₀ after congruence by 𝐆₀. The canonical factorization reads M(E⁰) = G_{-g₀}ᵗ 𝐌₀ G_{-g₀}, and shears compose additively, so conjugating by G_{g₀} cancels the shear exactly.

The calibrated sandwich

theorem HCPolySupport.HighContrast.Response.canonBlock_sandwich {d : ℕ} {E0 Es Et : FullBlockMat d} (hd : 2 ≤ d) (hE0 : Matrix.PosDef E0) (hEs : Matrix.PosDef Es) (hEt : Matrix.PosDef Et) (hts : Et ≤ Es) {z ceps rho beta : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (hlow : (1 - z) • E0 ≤ Es) (hhigh : Es ≤ (1 + z) • E0) (hceps : ceps = √((1 + z) / (1 - z))) (hrho : rho = canonDetRatio Es Et) (hbeta : beta = ceps * √(rho ^ d)) : beta⁻¹ • canonBlock E0 ≤ canonBlock Et ∧ canonBlock Et ≤ beta • canonBlock E0

The calibrated sandwich around M(E⁰). Composing the near-isometric mean comparison with the determinant-loss mean comparison gives β⁻¹ M(E⁰) ≤ M(E_t) ≤ β M(E⁰) with β = c_ε ϱ^{d/2}.

theorem HCPolySupport.HighContrast.Response.metric_sandwich {d : ℕ} {E0 Es Et : FullBlockMat d} (hd : 2 ≤ d) (hE0 : Matrix.PosDef E0) (hEs : Matrix.PosDef Es) (hEt : Matrix.PosDef Et) (hts : Et ≤ Es) {z ceps rho beta : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (hlow : (1 - z) • E0 ≤ Es) (hhigh : Es ≤ (1 + z) • E0) (hceps : ceps = √((1 + z) / (1 - z))) (hrho : rho = canonDetRatio Es Et) (hbeta : beta = ceps * √(rho ^ d)) {G0 M0 : FullBlockMat d} (hG0 : G0 = fullBlockShear (canonShear E0)) (hM0 : M0 = Matrix.fromBlocks (canonMetric E0) 0 0 (canonMetric E0)⁻¹) : beta⁻¹ • M0 ≤ Matrix.conjTranspose G0 * canonBlock Et * G0 ∧ Matrix.conjTranspose G0 * canonBlock Et * G0 ≤ beta • M0

The first boxed display of the response-load calibration: β⁻¹ 𝐌₀ ≤ 𝐆₀ᵗ M(E_t) 𝐆₀ ≤ β 𝐌₀.

theorem HCPolySupport.HighContrast.Response.imbalance_comparisons {d : ℕ} {Es Et : FullBlockMat d} (hd : 2 ≤ d) (hEs : Matrix.PosDef Es) (hEt : Matrix.PosDef Et) (hts : Et ≤ Es) {rho : ℝ} (hrho : rho = canonDetRatio Es Et) : canonImbalance Et ≤ rho ^ d * canonImbalance Es ∧ canonImbalance Es ≤ rho ^ (2 * d) * canonImbalance Et

The second boxed display of the response-load calibration: the two imbalance comparisons κ_t ≤ ϱ^d κ_s and κ_s ≤ ϱ^{2d} κ_t, at ϱ = (det E_s/det E_t)^{1/d}.

The two balance chains

theorem HCPolySupport.HighContrast.Response.hatE_terminal_sandwich {d : ℕ} {E0 Es Et : FullBlockMat d} (hd : 2 ≤ d) (hE0 : Matrix.PosDef E0) (hEs : Matrix.PosDef Es) (hEt : Matrix.PosDef Et) (hts : Et ≤ Es) (htSharp : fullBlockSharp Et ≤ Et) {z ceps rho beta : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (hlow : (1 - z) • E0 ≤ Es) (hhigh : Es ≤ (1 + z) • E0) (hceps : ceps = √((1 + z) / (1 - z))) (hrho : rho = canonDetRatio Es Et) (hbeta : beta = ceps * √(rho ^ d)) {G0 M0 : FullBlockMat d} (hG0 : G0 = fullBlockShear (canonShear E0)) (hM0 : M0 = Matrix.fromBlocks (canonMetric E0) 0 0 (canonMetric E0)⁻¹) : beta⁻¹ • M0 ≤ Matrix.conjTranspose G0 * Et * G0 ∧ Matrix.conjTranspose G0 * Et * G0 ≤ (beta * √(canonImbalance Et)) • M0

The terminal balance chain: β⁻¹ 𝐌₀ ≤ 𝐆₀ᵗ M(E_t) 𝐆₀ ≤ Ê_t ≤ β√κ_t 𝐌₀.

theorem HCPolySupport.HighContrast.Response.hatE_earlier_bound {d : ℕ} {E0 Es : FullBlockMat d} (hE0 : Matrix.PosDef E0) (hEs : Matrix.PosDef Es) (hsSharp : fullBlockSharp Es ≤ Es) {z ceps : ℝ} (hz0 : 0 ≤ z) (hz1 : z < 1) (hlow : (1 - z) • E0 ≤ Es) (hhigh : Es ≤ (1 + z) • E0) (hceps : ceps = √((1 + z) / (1 - z))) {G0 M0 : FullBlockMat d} (hG0 : G0 = fullBlockShear (canonShear E0)) (hM0 : M0 = Matrix.fromBlocks (canonMetric E0) 0 0 (canonMetric E0)⁻¹) : Matrix.conjTranspose G0 * Es * G0 ≤ (ceps * √(canonImbalance Es)) • M0

The earlier-scale balance chain: Ê_s ≤ √κ_s 𝐆₀ᵗ M(E_s) 𝐆₀ ≤ c_ε √κ_s 𝐌₀.