High-contrast homogenization: Provider.Response.LoadCalibrationClosure

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

The terminal defects, the energy chain, and the absolute closure

The remaining displays of the response-load calibration:

• the energy chain 0 ≤ 𝔼[J_t^±] = ½(L_t^±)² - 1 ≤ ½(L_t^±)² ≤ 2√θ, proved through the Schur form e.annealed.schur;
• the terminal defects 0 ≤ τ_{t,s}^± ≤ 2(ϱ^d - 1)√θ;
• the two consequences of terminal-profile compatibility, 𝒲_t^⋄ ≤ (ℛ_t^⋄)² and ℒ_s^⋄ ≤ 2Γ𝒬_s^⋄ ≤ 16Γc_εβ√κ_s(√κ_t+1)√θ, proved from the Loewner sandwich produced by a determinant loss;
• the norm identity |S_*^{-1/2}BS_*^{-1/2} - Id| = θ - 1;
• the factor-12d chain κ_t - 1 ≤ 6(θ-1) ≤ 12d sup(...);
• the absolute closure: under sup(...) ≤ ωκ_s and the strict numerical inequality 12dωϱ^{2d}(1 + δ_ad⁻¹) < 1, the imbalance closes at κ_t - 1 ≤ δ_ad.

The three probabilistic inputs — the annealed energy identity 𝔼[J_t^±] = ½(L_t^±)² - p·q^±, its nonnegativity, and the corrected absolute response estimate θ - 1 ≤ 2d sup(...) — belong to the corrected-response and profile layers and are carried here in their printed shapes. Everything else is proved.

There are no definitions in this file.

The terminal variational energies

theorem HCPolySupport.HighContrast.Response.energy_chain {EJ Lsq theta : ℝ} (hEJ : 0 ≤ EJ) (hid : EJ = 2⁻¹ * Lsq - 1) (hL : Lsq ≤ 4 * √theta) : 0 ≤ EJ ∧ EJ ≤ 2⁻¹ * Lsq ∧ 2⁻¹ * Lsq ≤ 2 * √theta

The energy chain 0 ≤ 𝔼[J_t^±] = ½(L_t^±)² - 1 ≤ ½(L_t^±)² ≤ 2√θ. The identity and the nonnegativity are the printed annealed inputs; the final bound is the load bound.

The congruent terminal defects

theorem HCPolySupport.HighContrast.Response.defect_bounds {d : ℕ} {Ethat Eshat : FullBlockMat d} (hEt : Matrix.PosSemidef Ethat) (hts : Ethat ≤ Eshat) {rd theta : ℝ} (hrd : 1 ≤ rd) (hup : Eshat ≤ rd • Ethat) (x : FullBlockVec d) (hx : x ⬝ᵥ Matrix.mulVec Ethat x ≤ 4 * √theta) : 0 ≤ 2⁻¹ * (x ⬝ᵥ Matrix.mulVec Eshat x - x ⬝ᵥ Matrix.mulVec Ethat x) ∧ 2⁻¹ * (x ⬝ᵥ Matrix.mulVec Eshat x - x ⬝ᵥ Matrix.mulVec Ethat x) ≤ 2 * (rd - 1) * √theta

The terminal defects 0 ≤ τ_{t,s}^± ≤ 2(ϱ^d - 1)√θ. The two hypotheses are the congruated forms of E_t ≤ E_s and of the determinant-loss comparison E_s ≤ ϱ^d E_t.

The two terminal-profile consequences

theorem HCPolySupport.HighContrast.Response.row_from_profile {L Gam Q ceps beta kappaS kappaT theta : ℝ} (hGam : 0 ≤ Gam) (hin : L ≤ 2 * Gam * Q) (hQ : Q ≤ 8 * ceps * beta * √kappaS * (√kappaT + 1) * √theta) : L ≤ 16 * Gam * ceps * beta * √kappaS * (√kappaT + 1) * √theta

ℒ_s^⋄ ≤ 2Γ𝒬_s^⋄ ≤ 16Γc_εβ√κ_s(√κ_t + 1)√θ: insert the calibrated row-load bound into the profile row hypothesis.

The normalized response block above the identity

theorem HCPolySupport.HighContrast.Response.norm_normalized_sub_one {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) : ‖matSqrt SStar⁻¹ * B * matSqrt SStar⁻¹ - 1‖ = relSize B SStar - 1

|S_*^{-1/2}BS_*^{-1/2} - Id| = θ - 1. The normalized response block is above the identity because B ≥ S ≥ S_*.

The factor-12d chain and the absolute closure

theorem HCPolySupport.HighContrast.Response.twelve_d_chain {d : ℕ} {kappaT theta Ssup : ℝ} (hkappa : kappaT ≤ 1 + 6 * (theta - 1)) (habs : theta - 1 ≤ 2 * ↑d * Ssup) : kappaT - 1 ≤ 12 * ↑d * Ssup

The factor-12d chain κ_t - 1 ≤ 6(θ - 1) ≤ 12d sup(...). The second link is the corrected absolute response estimate, carried in its printed shape.