Documentation

LeanPool.HighContrastHomogenization.Provider.Response.CenteredResponseOrder

High-contrast homogenization: Provider.Response.CenteredResponseOrder #

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

Positivity of the centered response matrices #

The annealed sharp order implies SStar ≤ S. Consequently the two matrices whose traces occur in the centered-response estimate are positive semidefinite, and their sum is the normalized corrected response block.

source
noncomputable def HCPolySupport.HighContrast.Response.centeredResponseX {d : ℕ} (S SStar : Mat d) :
Mat d

The normalized excess of the primal Schur block.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.centeredResponseY {d : ℕ} (SStar K : Mat d) :
    Mat d

    The normalized symmetric-coordinate correction.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Response.annealed_schur_sharp_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) :
      fullBlockSharp (schurBlock S SStar K) ≤ schurBlock S SStar K

      The annealed sharp order flattened at its Schur representation.

      source
      theorem HCPolySupport.HighContrast.Response.annealed_schurStar_le_schur {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) :
      SStar ≤ S

      The lower Schur matrix is below the upper one.

      source
      theorem HCPolySupport.HighContrast.Response.responseSymmetric_isHermitian {d : ℕ} (K : Mat d) :
      Matrix.conjTranspose (responseSymmetric K) = responseSymmetric K

      The symmetric response coordinate is Hermitian.

      source
      theorem HCPolySupport.HighContrast.Response.sub_responseSkew {d : ℕ} (K : Mat d) :
      K - responseSkew K = responseSymmetric K

      Removing the skew response coordinate leaves the symmetric coordinate.

      source
      theorem HCPolySupport.HighContrast.Response.two_smul_responseSymmetric {d : ℕ} (K : Mat d) :
      2 • responseSymmetric K = K + Matrix.conjTranspose K

      Doubling the symmetric response coordinate gives K + Kᴴ.

      source
      theorem HCPolySupport.HighContrast.Response.centeredResponseBlock_posDef {d : ℕ} {S SStar : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (K : Mat d) :
      Matrix.PosDef (centeredResponseBlock S SStar K)

      The corrected response block is positive definite.

      source
      theorem HCPolySupport.HighContrast.Response.centeredResponseMetric_posDef {d : ℕ} {S SStar : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (K : Mat d) :
      Matrix.PosDef (centeredResponseMetric S SStar K)

      The response metric is positive definite.

      source
      theorem HCPolySupport.HighContrast.Response.centeredResponseX_posSemidef {d : ℕ} {S SStar : Mat d} (hStar : Matrix.PosDef SStar) (horder : SStar ≤ S) :
      Matrix.PosSemidef (centeredResponseX S SStar)

      The normalized Schur excess X is positive semidefinite.

      source
      theorem HCPolySupport.HighContrast.Response.centeredResponseY_posSemidef {d : ℕ} {SStar : Mat d} (hStar : Matrix.PosDef SStar) (K : Mat d) :
      Matrix.PosSemidef (centeredResponseY SStar K)

      The symmetric-coordinate correction Y is positive semidefinite.

      source
      theorem HCPolySupport.HighContrast.Response.normalized_centeredResponseBlock_eq_X_add_Y {d : ℕ} (S SStar K : Mat d) :
      matSqrt SStar⁻¹ * centeredResponseBlock S SStar K * matSqrt SStar⁻¹ - 1 = centeredResponseX S SStar + centeredResponseY SStar K

      The normalized corrected block is exactly X + Y.