High-contrast homogenization: Provider.SourceControl.SchurHelpers

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

Schur-form helpers for the reference intermediate

The endpoint κ_𝐄 ≤ 6 Π of the factor-six reference-block comparison and the intermediate κ_𝐄 ≤ 1 + 6(Θ - 1) of HCPoly.Provider.SourceControl.ReferenceIntermediate use the same Schur-form transport lemmas. They live here so both comparison modules can reuse one public implementation.

Two of them are new: dotProduct_mulVec_smul_self and dotProduct_mulVec_smul_add_smul, the expansions of a quadratic form on a scalar multiple and on a two-term combination. They replace the endpoint's Young inequality at weight five, which the intermediate cannot use.

There are no definitions in this file.

Transport between the two Loewner encodings

theorem HCPolySupport.HighContrast.Initialization.quad_conj {n : Type u_1} [Fintype n] (C M : Matrix n n ℝ) (v : n → ℝ) : v ⬝ᵥ (C.conjTranspose * M * C).mulVec v = C.mulVec v ⬝ᵥ M.mulVec (C.mulVec v)

The quadratic form of a congruence.

theorem HCPolySupport.HighContrast.Initialization.elim_comp {d : ℕ} (v : FullBlockVec d) : Sum.elim (v ∘ Sum.inl) (v ∘ Sum.inr) = v

A doubled vector is the elimination of its two halves.

theorem HCPolySupport.HighContrast.Initialization.le_of_dotProduct_mulVec_le {n : Type u_1} [Fintype n] {A B : Matrix n n ℝ} (hA : A.IsHermitian) (hB : B.IsHermitian) (h : ∀ (v : n → ℝ), v ⬝ᵥ A.mulVec v ≤ v ⬝ᵥ B.mulVec v) : A ≤ B

The matrix order from the pointwise comparison of quadratic forms.

theorem HCPolySupport.HighContrast.Initialization.dotProduct_mulVec_le_of_le {n : Type u_1} [Fintype n] {A B : Matrix n n ℝ} (h : A ≤ B) (x : n → ℝ) : x ⬝ᵥ A.mulVec x ≤ x ⬝ᵥ B.mulVec x

The pointwise comparison of quadratic forms from the matrix order.

theorem HCPolySupport.HighContrast.Initialization.matLoewnerLE_of_le {d : ℕ} {A B : Mat d} (h : A ≤ B) : MatLoewnerLE A B

The MatLoewnerLE encoding from the matrix order.

theorem HCPolySupport.HighContrast.Initialization.le_of_matLoewnerLE {d : ℕ} {A B : Mat d} (hA : Matrix.IsHermitian A) (hB : Matrix.IsHermitian B) (h : MatLoewnerLE A B) : A ≤ B

The matrix order from the MatLoewnerLE encoding.

Two matrix inequalities

theorem HCPolySupport.HighContrast.Initialization.conj_add_le {d : ℕ} {X : Mat d} (hX : Matrix.PosSemidef X) (a b : Mat d) : Matrix.conjTranspose (a + b) * X * (a + b) ≤ Matrix.conjTranspose a * X * a + Matrix.conjTranspose a * X * a + (Matrix.conjTranspose b * X * b + Matrix.conjTranspose b * X * b)

The parallelogram bound. A sum is squared by a positive semidefinite congruence at the cost of a factor two on each summand.

theorem HCPolySupport.HighContrast.Initialization.conj_transpose_le_of_conj_le {d : ℕ} {X : Mat d} (hX : Matrix.PosDef X) {m : Mat d} {c : ℝ} (hc : 0 ≤ c) (h : Matrix.conjTranspose m * X * m ≤ c • X⁻¹) : m * X * Matrix.conjTranspose m ≤ c • X⁻¹

Transposition preserves a normalized quadratic bound. If mᵗ X m ≤ c X⁻¹ then m X mᵗ ≤ c X⁻¹; the two sides are the squared operator norms of X^{1/2} m X^{1/2} and its transpose.

Expansions of a quadratic form

theorem HCPolySupport.HighContrast.Initialization.dotProduct_mulVec_smul_self {d : ℕ} (X : Mat d) (a : ℝ) (u : Vec d) : a • u ⬝ᵥ Matrix.mulVec X (a • u) = a ^ 2 * u ⬝ᵥ Matrix.mulVec X u

A scalar multiple passes the quadratic form as its square.

theorem HCPolySupport.HighContrast.Initialization.dotProduct_mulVec_smul_add_smul {d : ℕ} {X : Mat d} (hX : Matrix.transpose X = X) (a b : ℝ) (u v : Vec d) : (a • u + b • v) ⬝ᵥ Matrix.mulVec X (a • u + b • v) = a ^ 2 * u ⬝ᵥ Matrix.mulVec X u + 2 * (a * b) * u ⬝ᵥ Matrix.mulVec X v + b ^ 2 * v ⬝ᵥ Matrix.mulVec X v

The bilinear expansion. A symmetric matrix squares a two-term combination into the three scalar products.