Real and complex matrix quadratic forms

Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

def OlevskiiGram.realDot {ι : Type u_1} [Fintype ι] (x y : ι → ℝ) : ℝ

Dot product on a finite real coordinate space.

Equations

• OlevskiiGram.realDot x y = ∑ i : ι, x i * y i

def OlevskiiGram.realQuadraticForm {ι : Type u_1} [Fintype ι] (A : Matrix ι ι ℝ) (x : ι → ℝ) : ℝ

Quadratic form associated to a real matrix.

Equations

• OlevskiiGram.realQuadraticForm A x = ∑ i : ι, x i * ∑ j : ι, A i j * x j

def OlevskiiGram.RealSymmetric {ι : Type u_1} (A : Matrix ι ι ℝ) : Prop

Real symmetry for a matrix.

Equations

• OlevskiiGram.RealSymmetric A = ∀ (i j : ι), A i j = A j i

def OlevskiiGram.RealPSD {ι : Type u_1} [Fintype ι] (A : Matrix ι ι ℝ) : Prop

Positive semidefiniteness in quadratic-form language.

Equations

• OlevskiiGram.RealPSD A = ∀ (x : ι → ℝ), 0 ≤ OlevskiiGram.realQuadraticForm A x

def OlevskiiGram.RealLoewnerLE {ι : Type u_1} [Fintype ι] (A B : Matrix ι ι ℝ) : Prop

Loewner order for real matrices, expressed by positive semidefinite difference.

Equations

• OlevskiiGram.RealLoewnerLE A B = OlevskiiGram.RealPSD (B - A)

def OlevskiiGram.RealLoewnerBetweenZeroAndOne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) : Prop

The real matrix inequality 0 ≤ A ≤ I.

Equations

• OlevskiiGram.RealLoewnerBetweenZeroAndOne A = (OlevskiiGram.RealPSD A ∧ OlevskiiGram.RealLoewnerLE A 1)

def OlevskiiGram.InRealUnitCube {ι : Type u_1} (x : ι → ℝ) : Prop

Coordinatewise membership in the real cube [-1,1]^ι.

Equations

• OlevskiiGram.InRealUnitCube x = ∀ (i : ι), |x i| ≤ 1

def OlevskiiGram.realRankOne {ι : Type u_1} (q : ι → ℝ) : Matrix ι ι ℝ

Rank-one real matrix q qᵀ.

Equations

• OlevskiiGram.realRankOne q i j = q i * q j

def OlevskiiGram.ComplexHermitian {ι : Type u_1} (A : Matrix ι ι ℂ) : Prop

Complex Hermitian symmetry, in entrywise form.

Equations

• OlevskiiGram.ComplexHermitian A = ∀ (i j : ι), A j i = star (A i j)

def OlevskiiGram.complexReMatrix {ι : Type u_1} (A : Matrix ι ι ℂ) : Matrix ι ι ℝ

Real part of a complex matrix.

Equations

• OlevskiiGram.complexReMatrix A i j = (A i j).re

def OlevskiiGram.complexImMatrix {ι : Type u_1} (A : Matrix ι ι ℂ) : Matrix ι ι ℝ

Imaginary part of a complex matrix.

Equations

• OlevskiiGram.complexImMatrix A i j = (A i j).im

def OlevskiiGram.complexQuadraticFormRe {ι : Type u_1} [Fintype ι] (A : Matrix ι ι ℂ) (x : ι → ℂ) : ℝ

Real part of the complex quadratic form x* A x.

Equations

• OlevskiiGram.complexQuadraticFormRe A x = (∑ i : ι, star (x i) * ∑ j : ι, A i j * x j).re

def OlevskiiGram.ComplexPSD {ι : Type u_1} [Fintype ι] (A : Matrix ι ι ℂ) : Prop

Positive semidefiniteness for complex matrices, stated through quadratic forms.

Equations

• OlevskiiGram.ComplexPSD A = ∀ (x : ι → ℂ), 0 ≤ OlevskiiGram.complexQuadraticFormRe A x

def OlevskiiGram.ComplexLoewnerBetweenZeroAndOne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) : Prop

The complex matrix inequality 0 ≤ A ≤ I.

Equations

• OlevskiiGram.ComplexLoewnerBetweenZeroAndOne A = (OlevskiiGram.ComplexPSD A ∧ OlevskiiGram.ComplexPSD (1 - A))

def OlevskiiGram.realBlockMatrix {ι : Type u_1} (A B : Matrix ι ι ℝ) : Matrix (ι ⊕ ι) (ι ⊕ ι) ℝ

The real block matrix associated to A + iB.

Equations

• OlevskiiGram.realBlockMatrix A B (Sum.inl i) (Sum.inl j) = A i j
• OlevskiiGram.realBlockMatrix A B (Sum.inl i) (Sum.inr j) = -B i j
• OlevskiiGram.realBlockMatrix A B (Sum.inr i) (Sum.inl j) = B i j
• OlevskiiGram.realBlockMatrix A B (Sum.inr i) (Sum.inr j) = A i j