High-contrast homogenization: Provider.Response.LoadCalibrationQuadratic

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

Quadratic forms in Schur coordinates

The load displays of the response-load calibration are quadratic forms of the terminal block at the two signed profile vectors, so they need the Schur factorization read on vectors rather than on matrices. This file supplies that reading, once:

(X, Y) ⬝ schurBlock s s_* k (X, Y) = ⟨sX, X⟩ + ⟨s_*⁻¹(Y - kX), Y - kX⟩,

together with the elementary facts the recentering step uses: the shear acts on a doubled vector by G_c (X, Y) = (X, cX + Y), a skew matrix annihilates its own quadratic form, and ⟨m^{-1/2}e, m^{1/2}e⟩ = ⟨e, e⟩.

There are no definitions in this file.

Doubled vectors

theorem HCPolySupport.HighContrast.Response.quadratic_fromBlocks_diag {d : ℕ} (A C : Mat d) (X Y : Vec d) : Sum.elim X Y ⬝ᵥ (Matrix.fromBlocks A 0 0 C).mulVec (Sum.elim X Y) = X ⬝ᵥ Matrix.mulVec A X + Y ⬝ᵥ Matrix.mulVec C Y

The quadratic form of a diagonal doubled block.

theorem HCPolySupport.HighContrast.Response.fullBlockShear_mulVec {d : ℕ} (c : Mat d) (X Y : Vec d) : Matrix.mulVec (fullBlockShear c) (Sum.elim X Y) = Sum.elim X (Matrix.mulVec c X + Y)

The shear acts on a doubled vector by G_c (X, Y) = (X, cX + Y).

theorem HCPolySupport.HighContrast.Response.quadratic_schurBlock {d : ℕ} (s sStar k : Mat d) (X Y : Vec d) : Sum.elim X Y ⬝ᵥ Matrix.mulVec (schurBlock s sStar k) (Sum.elim X Y) = X ⬝ᵥ Matrix.mulVec s X + (Y - Matrix.mulVec k X) ⬝ᵥ sStar⁻¹.mulVec (Y - Matrix.mulVec k X)

The quadratic form of the Schur factorization.

Pairings

theorem HCPolySupport.HighContrast.Response.dotProduct_mulVec_pair {d : ℕ} (A B : Mat d) (x y : Vec d) : Matrix.mulVec A x ⬝ᵥ Matrix.mulVec B y = x ⬝ᵥ (Matrix.transpose A * B).mulVec y

The pairing of two matrix images, moved onto one side.

theorem HCPolySupport.HighContrast.Response.dotProduct_mulVec_of_skew {d : ℕ} {W : Mat d} (hW : Matrix.conjTranspose W = -W) (x : Vec d) : x ⬝ᵥ Matrix.mulVec W x = 0

A skew matrix annihilates its own quadratic form.

theorem HCPolySupport.HighContrast.Response.polarization {n : Type u_1} [Fintype n] (T : Matrix n n ℝ) (u v : n → ℝ) : (u + v) ⬝ᵥ T.mulVec (u + v) + (u - v) ⬝ᵥ T.mulVec (u - v) = 2 * u ⬝ᵥ T.mulVec u + 2 * v ⬝ᵥ T.mulVec v

Polarization: the two cross terms cancel.

theorem HCPolySupport.HighContrast.Response.dotProduct_load_pair {d : ℕ} {m : Mat d} (hm : Matrix.PosDef m) (e : Vec d) : (matSqrt m⁻¹).mulVec e ⬝ᵥ (matSqrt m).mulVec e = e ⬝ᵥ e

The load pairing is the Euclidean pairing: ⟨m^{-1/2}e, m^{1/2}e⟩ = ⟨e, e⟩.