Coarse-graining support: Support.Ambient.ScalarMatrix

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Positive scalar matrices

Small helpers for scalar multiples of the identity, used when a deterministic black-box statement is meant only for scalar constant backgrounds.

@[reducible, inline]

abbrev HCPolySupport.scalarMatrix {d : ℕ} (sigma : ℝ) : Mat d

The scalar matrix sigma • I.

Equations

• HCPolySupport.scalarMatrix sigma = sigma • 1

def HCPolySupport.IsPositiveScalarMatrix {d : ℕ} (A : Mat d) : Prop

A matrix is a positive scalar matrix if it is sigma • I with sigma > 0.

Equations

• HCPolySupport.IsPositiveScalarMatrix A = ∃ (sigma : ℝ), 0 < sigma ∧ A = HCPolySupport.scalarMatrix sigma

theorem HCPolySupport.matVecMul_scalarMatrix {d : ℕ} (sigma : ℝ) (x : Vec d) : matVecMul (scalarMatrix sigma) x = sigma • x

theorem HCPolySupport.scalarMatrix_isSymm {d : ℕ} (sigma : ℝ) : Matrix.IsSymm (scalarMatrix sigma)

theorem HCPolySupport.isEllipticMatrix_scalarMatrix {d : ℕ} {sigma : ℝ} (hsigma : 0 < sigma) : IsEllipticMatrix sigma sigma (scalarMatrix sigma)

theorem HCPolySupport.IsPositiveScalarMatrix.isSymm {d : ℕ} {A : Mat d} (hA : IsPositiveScalarMatrix A) : Matrix.IsSymm A

theorem HCPolySupport.IsPositiveScalarMatrix.isEllipticMatrix {d : ℕ} {A : Mat d} (hA : IsPositiveScalarMatrix A) : ∃ (sigma : ℝ), 0 < sigma ∧ IsEllipticMatrix sigma sigma A