High-contrast homogenization: Provider.Response.LoadCalibrationProfile

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

The individual load bounds and the profile factor

The boxed display of the response-load calibration:

(L_t^±)² ≤ 4√θ,     Λ_t^± ≤ √5 θ^{1/4},     K_t ≤ β^{1/2}κ_t^{1/4},

and the signed-load display,

|𝐌₀^{1/2}x^±|² ≤ 4β√θ.

The individual load bounds follow from the exact sum of LoadCalibrationLoads because both summands are nonnegative — each is a quadratic form of the positive block Ê_t. The Λ bound adds the pairing p·q^± = 1, which holds because p·q = e·e = 1 and both g₀ - h and h - g₀ are skew. The K_t bound is the upper canonical comparison Ê_t ≤ β√κ_t 𝐌₀ read as a relative size, and the signed-load bound is the lower one β⁻¹𝐌₀ ≤ Ê_t read at x^±.

Throughout, |𝐌₀^{1/2}x|² is the quadratic form x ⬝ 𝐌₀ x.

There are no definitions in this file.

Elementary facts about the canonical metric block

theorem HCPolySupport.HighContrast.Response.posDef_metricBlock {d : ℕ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) : (Matrix.fromBlocks m0 0 0 m0⁻¹).PosDef

The canonical metric block 𝐌₀ = diag(m₀, m₀⁻¹) is positive definite.

theorem HCPolySupport.HighContrast.Response.quadratic_nonneg {n : Type u_1} [Fintype n] {A : Matrix n n ℝ} (hA : A.PosSemidef) (x : n → ℝ) : 0 ≤ x ⬝ᵥ A.mulVec x

A quadratic form of a positive semidefinite matrix is nonnegative.

theorem HCPolySupport.HighContrast.Response.quadratic_conj_nonneg {d : ℕ} {Et G0 Ehat : FullBlockMat d} (hEt : Matrix.PosSemidef Et) (hEhat : Ehat = Matrix.conjTranspose G0 * Et * G0) (x : FullBlockVec d) : 0 ≤ x ⬝ᵥ Matrix.mulVec Ehat x

The congruence of a positive semidefinite matrix has nonnegative quadratic forms.

theorem HCPolySupport.HighContrast.Response.le_sqrt_of_sq_le {x c : ℝ} (hx : 0 ≤ x) (h : x ^ 2 ≤ c) : x ≤ √c

A nonnegative number below a square root bound.

The pairing of the signed loads

theorem HCPolySupport.HighContrast.Response.dotProduct_signed_load {d : ℕ} {m : Mat d} {e p q : Vec d} {W : Mat d} (hm : Matrix.PosDef m) (hW : Matrix.conjTranspose W = -W) (hp : p = (matSqrt m⁻¹).mulVec e) (hq : q = (matSqrt m).mulVec e) (he : e ⬝ᵥ e = 1) : p ⬝ᵥ (q + Matrix.mulVec W p) = 1

The load pairing is one: p·q^± = 1, because p·q = e·e = 1 and the shift is by a skew matrix.

theorem HCPolySupport.HighContrast.Response.skew_sub {d : ℕ} {A C : Mat d} (hA : Matrix.conjTranspose A = -A) (hC : Matrix.conjTranspose C = -C) : Matrix.conjTranspose (A - C) = -(A - C)

Both g₀ - h and h - g₀ are skew when g₀ and h are.

The individual load bounds

theorem HCPolySupport.HighContrast.Response.load_sq_neg_le {d : ℕ} {S SStar K r B m g0 h : Mat d} {Et Ehat G0 : FullBlockMat d} {e p q : Vec d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hEtpd : Matrix.PosDef Et) (hEt : Et = schurBlock S SStar K) (hG0 : G0 = fullBlockShear g0) (hEhat : Ehat = Matrix.conjTranspose G0 * Et * G0) (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) (hh : h = 2⁻¹ • (K - Matrix.conjTranspose K)) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) (hmdef : m = matGeomMean B SStar) (hp : p = (matSqrt m⁻¹).mulVec e) (hq : q = (matSqrt m).mulVec e) (he : e ⬝ᵥ e = 1) {theta : ℝ} (htheta : 0 < theta) (hBle : B ≤ theta • SStar) : Sum.elim (-p) (q + Matrix.mulVec (g0 - h) p) ⬝ᵥ Matrix.mulVec Ehat (Sum.elim (-p) (q + Matrix.mulVec (g0 - h) p)) ≤ 4 * √theta

(L_t^-)² ≤ 4√θ, from the exact sum and nonnegativity of the other summand.

theorem HCPolySupport.HighContrast.Response.load_sq_pos_le {d : ℕ} {S SStar K r B m g0 h : Mat d} {Et Ehat G0 : FullBlockMat d} {e p q : Vec d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hEtpd : Matrix.PosDef Et) (hEt : Et = schurBlock S SStar K) (hG0 : G0 = fullBlockShear g0) (hEhat : Ehat = Matrix.conjTranspose G0 * Et * G0) (hr : r = 2⁻¹ • (K + Matrix.conjTranspose K)) (hh : h = 2⁻¹ • (K - Matrix.conjTranspose K)) (hB : B = S + Matrix.conjTranspose r * SStar⁻¹ * r) (hmdef : m = matGeomMean B SStar) (hp : p = (matSqrt m⁻¹).mulVec e) (hq : q = (matSqrt m).mulVec e) (he : e ⬝ᵥ e = 1) {theta : ℝ} (htheta : 0 < theta) (hBle : B ≤ theta • SStar) : Sum.elim p (q + Matrix.mulVec (h - g0) p) ⬝ᵥ Matrix.mulVec Ehat (Sum.elim p (q + Matrix.mulVec (h - g0) p)) ≤ 4 * √theta

(L_t^+)² ≤ 4√θ.

The recentered profile factor

theorem HCPolySupport.HighContrast.Response.lambda_le {Lsq Lam theta : ℝ} (hLam : 0 ≤ Lam) (htheta : 1 ≤ theta) (hLamsq : Lam ^ 2 = Lsq + 1) (hLsq : Lsq ≤ 4 * √theta) : Lam ≤ √5 * √√theta

Λ_t^± ≤ √5 θ^{1/4}. The printed Λ is ((L_t^±)² + |p·q^±|)^{1/2}; with the pairing equal to one and θ ≥ 1 the square is at most 5√θ.

theorem HCPolySupport.HighContrast.Response.profile_factor_le {d : ℕ} {m0 : Mat d} {Ehat M0 : FullBlockMat d} {Kt beta kappa : ℝ} (hm0 : Matrix.PosDef m0) (hM0 : M0 = Matrix.fromBlocks m0 0 0 m0⁻¹) (hEhatPsd : Matrix.PosSemidef Ehat) (hKt : 0 ≤ Kt) (hKtsq : Kt ^ 2 = relSize Ehat M0) (hbeta : 0 ≤ beta) (hup : Ehat ≤ (beta * √kappa) • M0) : Kt ≤ √beta * √√kappa

K_t ≤ β^{1/2}κ_t^{1/4} (, proof). The printed K_t is |𝐌₀^{-1/2}Ê_t𝐌₀^{-1/2}|^{1/2}, i.e. the square root of the relative size of Ê_t against 𝐌₀.

theorem HCPolySupport.HighContrast.Response.skew_half_sub {d : ℕ} (K : Mat d) : Matrix.conjTranspose (2⁻¹ • (K - Matrix.conjTranspose K)) = -(2⁻¹ • (K - Matrix.conjTranspose K))

The response skew coordinate h = ½(K - Kᵗ) is skew.

The signed loads in the canonical metric

theorem HCPolySupport.HighContrast.Response.metric_load_le_smul {d : ℕ} {Ehat M0 : FullBlockMat d} {beta : ℝ} (hbeta : 0 < beta) (hlow : beta⁻¹ • M0 ≤ Ehat) (x : FullBlockVec d) : x ⬝ᵥ Matrix.mulVec M0 x ≤ beta * x ⬝ᵥ Matrix.mulVec Ehat x

|𝐌₀^{1/2}x|² ≤ β (L)²: the lower canonical comparison read at a signed profile vector.

theorem HCPolySupport.HighContrast.Response.metric_signed_load_le {d : ℕ} {Ehat M0 : FullBlockMat d} {beta theta : ℝ} (hbeta : 0 < beta) (hlow : beta⁻¹ • M0 ≤ Ehat) {x : FullBlockVec d} (hx : x ⬝ᵥ Matrix.mulVec Ehat x ≤ 4 * √theta) : x ⬝ᵥ Matrix.mulVec M0 x ≤ 4 * beta * √theta

|𝐌₀^{1/2}x^±|² ≤ 4β√θ, the boxed display.