Documentation

LeanPool.HighContrastHomogenization.Geometry.SchurData

High-contrast homogenization: Geometry.SchurData #

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

Schur data of a positive doubled block #

Every positive 2d-by-2d block has a unique factorization H = G_{-k}^t diag(s, s_*^{-1}) G_{-k} with s, s_* > 0, the triple (s, s_*, k) being its Schur data (e.annealed.schur). Existence and uniqueness are read off the blocks: positivity gives s_*^{-1} = H_{22} > 0, then k = -H_{22}^{-1}H_{21} and s = H_{11} - H_{12}H_{22}^{-1}H_{21} > 0.

The last clause of the canonical balance needs one more fact, also proved here: the sharp involution acts on Schur data by (s, s_*, k) ↦ (s_*, s, -k^t). On a self-dual block this forces s = s_* and k skew, which is the canonical factorization.

source
noncomputable def HCPolySupport.HighContrast.schurBlock {d : ℕ} (s sStar k : Mat d) :
FullBlockMat d

The Schur form G_{-k}^t diag(s, s_*^{-1}) G_{-k} of e.annealed.schur.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.schurBlock_eq {d : ℕ} (s sStar k : Mat d) :
    schurBlock s sStar k = Matrix.fromBlocks (s + Matrix.conjTranspose k * sStar⁻¹ * k) (-(Matrix.conjTranspose k * sStar⁻¹)) (-(sStar⁻¹ * k)) sStar⁻¹

    The Schur form written out.

    source
    @[simp]
    theorem HCPolySupport.HighContrast.toBlocks₁₁_schurBlock {d : ℕ} (s sStar k : Mat d) :
    Matrix.toBlocks₁₁ (schurBlock s sStar k) = s + Matrix.conjTranspose k * sStar⁻¹ * k
    source
    @[simp]
    theorem HCPolySupport.HighContrast.toBlocks₂₁_schurBlock {d : ℕ} (s sStar k : Mat d) :
    Matrix.toBlocks₂₁ (schurBlock s sStar k) = -(sStar⁻¹ * k)
    source
    @[simp]
    theorem HCPolySupport.HighContrast.toBlocks₂₂_schurBlock {d : ℕ} (s sStar k : Mat d) :
    Matrix.toBlocks₂₂ (schurBlock s sStar k) = sStar⁻¹

    Diagonal blocks of a positive block #

    source
    theorem HCPolySupport.HighContrast.posDef_toBlocks₁₁ {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :
    (Matrix.toBlocks₁₁ H).PosDef

    The upper-left block of a positive definite doubled block is positive definite.

    source
    theorem HCPolySupport.HighContrast.posDef_toBlocks₂₂ {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :
    (Matrix.toBlocks₂₂ H).PosDef

    The lower-right block of a positive definite doubled block is positive definite.

    source
    theorem HCPolySupport.HighContrast.toBlocks₁₂_eq_conjTranspose {d : ℕ} {H : FullBlockMat d} (hH : Matrix.IsHermitian H) :
    Matrix.toBlocks₁₂ H = (Matrix.toBlocks₂₁ H).conjTranspose

    The off-diagonal blocks of a Hermitian doubled block are adjoint.

    source
    theorem HCPolySupport.HighContrast.toBlocks₁₁_mono {d : ℕ} {A B : FullBlockMat d} (h : A ≤ B) :
    Matrix.toBlocks₁₁ A ≤ Matrix.toBlocks₁₁ B

    Passing to the upper-left block is monotone for the Loewner order.

    source
    theorem HCPolySupport.HighContrast.toBlocks₂₂_mono {d : ℕ} {A B : FullBlockMat d} (h : A ≤ B) :
    Matrix.toBlocks₂₂ A ≤ Matrix.toBlocks₂₂ B

    Passing to the lower-right block is monotone for the Loewner order. This is the reference text's step "taking the lower-right principal blocks".

    source
    @[simp]
    theorem HCPolySupport.HighContrast.toBlocks₁₁_smul {d : ℕ} (c : ℝ) (A : FullBlockMat d) :
    Matrix.toBlocks₁₁ (c • A) = c • Matrix.toBlocks₁₁ A
    source
    @[simp]
    theorem HCPolySupport.HighContrast.toBlocks₂₂_smul {d : ℕ} (c : ℝ) (A : FullBlockMat d) :
    Matrix.toBlocks₂₂ (c • A) = c • Matrix.toBlocks₂₂ A

    Existence and uniqueness of the Schur data #

    source
    theorem HCPolySupport.HighContrast.posDef_schurBlock {d : ℕ} {s sStar k : Mat d} (hs : Matrix.PosDef s) (hstar : Matrix.PosDef sStar) :
    Matrix.PosDef (schurBlock s sStar k)

    Positivity of the Schur form.

    source
    theorem HCPolySupport.HighContrast.schurBlock_injective {d : ℕ} {s₁ t₁ k₁ s₂ t₂ k₂ : Mat d} (ht₁ : Matrix.PosDef t₁) (ht₂ : Matrix.PosDef t₂) (h : schurBlock s₁ t₁ k₁ = schurBlock s₂ t₂ k₂) :
    s₁ = s₂ ∧ t₁ = t₂ ∧ k₁ = k₂

    Uniqueness of the Schur data (e.annealed.schur).

    source
    theorem HCPolySupport.HighContrast.posDef_of_posDef_schurBlock {d : ℕ} {s sStar k : Mat d} (hstar : Matrix.PosDef sStar) (h : Matrix.PosDef (schurBlock s sStar k)) :
    Matrix.PosDef s

    The upper Schur block of a positive Schur form is positive definite. The quadratic form of schurBlock s s_* k at the sheared state (x, k x) is the quadratic form of s at x.

    source
    theorem HCPolySupport.HighContrast.exists_schurBlock {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :
    ∃ (s : Mat d) (sStar : Mat d) (k : Mat d), Matrix.PosDef s ∧ Matrix.PosDef sStar ∧ H = schurBlock s sStar k

    Existence of the Schur data (e.annealed.schur).

    source
    theorem HCPolySupport.HighContrast.fullBlockSharp_schurBlock {d : ℕ} {s sStar k : Mat d} (hs : Matrix.PosDef s) (hstar : Matrix.PosDef sStar) :
    fullBlockSharp (schurBlock s sStar k) = schurBlock sStar s (-Matrix.conjTranspose k)

    The Schur data of the sharp. Inverting the Schur form shows that H^♯ has Schur data (s_*, s, -k^t).