Schur Product Theorem

Proves the Schur product theorem (real, finite-index case): if A and B are positive semidefinite Hermitian matrices, then their entrywise (Hadamard) product D with entries D i j = A i j * B i j is also positive semidefinite. The proof reduces positivity of the Hadamard form x ᵀ (A ∘ B) x to positivity of the Kronecker product A ⊗ B applied to the diagonal embedding of x into ι × ι. Used in the OS3 reflection positivity argument to transfer PSD properties through the matrix exponential via HadamardExp.lean.

def OSforGFF.«term_∘ₕ_» : Lean.TrailingParserDescr

Notation alias for the Hadamard (entrywise) product from Mathlib.

Equations

• OSforGFF.«term_∘ₕ_» = Lean.ParserDescr.trailingNode `OSforGFF.«term_∘ₕ_» 100 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∘ₕ") (Lean.ParserDescr.cat `term 0))

noncomputable def OSforGFF.diagEmbed {ι : Type u} (x : ι → ℝ) : ι × ι → ℝ

Auxiliary: diagonal embedding of a vector x : ι → ℝ into ι×ι used for the restriction argument: only the diagonal entries are nonzero and equal to x.

Equations

• OSforGFF.diagEmbed x p = if p.2 = p.1 then x p.1 else 0

theorem OSforGFF.diagEmbed_ne_zero_of_ne_zero {ι : Type u} {x : ι → ℝ} (hx : x ≠ 0) : diagEmbed x ≠ 0

theorem OSforGFF.sum_pairs_eq_double {ι : Type u} [Fintype ι] (g : ι × ι → ℝ) : ∑ p : ι × ι, g p = ∑ i : ι, ∑ j : ι, g (i, j)

Finite sum over pairs equals iterated double sum over coordinates (binderless sums).

@[simp]

theorem OSforGFF.schur_product_posDef {ι : Type u} [Finite ι] (A B : Matrix ι ι ℝ) (hA : A.PosDef) (hB : B.PosDef) : (A∘ₕB).PosDef

Schur product theorem (real case, finite index): If A B are positive definite matrices over ℝ, then the Hadamard product is positive definite.