Entrywise Exponential of PSD Matrices

Develops Hadamard (entrywise) operations on real matrices and proves that the entrywise exponential preserves positive semidefiniteness. The key tool is the Schur product theorem (from SchurProduct.lean): Hadamard powers of a PD matrix remain PD, so summing them with coefficients 1/n! yields a PD matrix. The PSD case follows by a continuity argument: R + ε I is PD for every ε > 0, and the limit ε → 0 uses continuity of the entrywise exponential.

noncomputable def OSforGFF.entrywiseExp {ι : Type u} (R : Matrix ι ι ℝ) : Matrix ι ι ℝ

Entrywise real exponential of a matrix: (entrywiseExp R) i j = exp (R i j). Used for the OS3 proof (Glimm–Jaffe): if R is PSD, then exp(R) (entrywise) should be PSD.

Equations

• OSforGFF.entrywiseExp R i j = Real.exp (R i j)

@[simp]

theorem OSforGFF.entrywiseExp_apply {ι : Type u} (R : Matrix ι ι ℝ) (i j : ι) : entrywiseExp R i j = Real.exp (R i j)

theorem OSforGFF.continuous_entrywiseExp (ι : Type u) : Continuous fun (R : Matrix ι ι ℝ) => entrywiseExp R

Continuity of the entrywise exponential map R ↦ exp ∘ R on matrices.

def OSforGFF.hadamardOne (ι : Type u) : Matrix ι ι ℝ

Hadamard identity element: the all-ones matrix for entrywise multiplication.

Equations

• OSforGFF.hadamardOne ι x✝¹ x✝ = 1

def OSforGFF.hadamardPow {ι : Type u} (R : Matrix ι ι ℝ) : ℕ → Matrix ι ι ℝ

n-fold Hadamard power of a matrix: hadamardPow R n = R ∘ₕ ⋯ ∘ₕ R (n times), with hadamardPow R 0 = hadamardOne.

Equations

• OSforGFF.hadamardPow R 0 = OSforGFF.hadamardOne ι
• OSforGFF.hadamardPow R n.succ = OSforGFF.hadamardPow R n∘ₕR

@[simp]

theorem OSforGFF.hadamardPow_zero {ι : Type u} (R : Matrix ι ι ℝ) : hadamardPow R 0 = hadamardOne ι

@[simp]

theorem OSforGFF.hadamardPow_succ {ι : Type u} (R : Matrix ι ι ℝ) (n : ℕ) : hadamardPow R (n + 1) = hadamardPow R n∘ₕR

theorem OSforGFF.hadamardPow_apply {ι : Type u} (R : Matrix ι ι ℝ) (n : ℕ) (i j : ι) : hadamardPow R n i j = R i j ^ n

Hadamard powers act entrywise as usual scalar powers.

noncomputable def OSforGFF.entrywiseExpSeriesTerm {ι : Type u} (R : Matrix ι ι ℝ) (n : ℕ) : Matrix ι ι ℝ

One term of the Hadamard-series for the entrywise exponential.

Equations

• OSforGFF.entrywiseExpSeriesTerm R n = (1 / ↑n.factorial) • OSforGFF.hadamardPow R n

noncomputable def OSforGFF.entrywiseExpHadamardSeries {ι : Type u} (R : Matrix ι ι ℝ) : Matrix ι ι ℝ

Series definition of the entrywise exponential using Hadamard powers (entrywise tsum).

Equations

• OSforGFF.entrywiseExpHadamardSeries R i j = ∑' (n : ℕ), 1 / ↑n.factorial * OSforGFF.hadamardPow R n i j

theorem OSforGFF.entrywiseExp_eq_hadamardSeries {ι : Type u} (R : Matrix ι ι ℝ) : entrywiseExp R = entrywiseExpHadamardSeries R

The entrywise exponential agrees with its Hadamard series expansion. Uses the Taylor series for Complex.exp and converts to the real case.

theorem OSforGFF.hadamardOne_hMul_left {ι : Type u} (R : Matrix ι ι ℝ) : (hadamardOne ι∘ₕR) = R

Ones is the identity for the Hadamard product.

theorem OSforGFF.hadamardPow_posDef_of_posDef {ι : Type u} [Finite ι] (R : Matrix ι ι ℝ) (hR : R.PosDef) (n : ℕ) : 1 ≤ n → (hadamardPow R n).PosDef

Hadamard powers of a positive definite matrix are positive definite for all n ≥ 1.

theorem OSforGFF.quadratic_form_entrywiseExp_hadamardSeries {ι : Type u} [Fintype ι] (R : Matrix ι ι ℝ) (x : ι → ℝ) : x ⬝ᵥ (entrywiseExpHadamardSeries R).mulVec x = ∑' (n : ℕ), 1 / ↑n.factorial * x ⬝ᵥ (hadamardPow R n).mulVec x

The quadratic form of the Hadamard series equals the sum of quadratic forms of individual terms. This lemma handles the complex interchange of summation and quadratic form evaluation.

theorem OSforGFF.summable_hadamardQuadSeries {ι : Type u} [Fintype ι] (R : Matrix ι ι ℝ) (x : ι → ℝ) : Summable fun (n : ℕ) => 1 / ↑n.factorial * x ⬝ᵥ (hadamardPow R n).mulVec x

Summability of the scalar quadratic-form coefficients appearing in the Hadamard exponential series.

theorem OSforGFF.posDef_entrywiseExp_hadamardSeries_of_posDef {ι : Type u} [Finite ι] (R : Matrix ι ι ℝ) (hR : R.PosDef) : (entrywiseExpHadamardSeries R).PosDef

The Hadamard-series entrywise exponential preserves positive definiteness. Sketch: each Hadamard power (for n ≥ 1) is PD by the Schur product theorem and induction; summing with positive coefficients 1/n! yields strictly positive quadratic form for every x ≠ 0 since the n = 1 term already contributes xᵀ R x > 0. Interchange of sum and quadratic form follows from absolute convergence of the scalar exp series; IsHermitian follows termwise.

theorem OSforGFF.posSemidef_entrywiseExp_hadamardSeries_of_posSemidef {ι : Type u} [Finite ι] (R : Matrix ι ι ℝ) (hR : R.PosSemidef) : (entrywiseExpHadamardSeries R).PosSemidef

The Hadamard-series entrywise exponential preserves positive semidefiniteness. This follows from the positive definite case by continuity: if R is PSD, then R + εI is PD for ε > 0, so entrywiseExpHadamardSeries(R + εI) is PD, and taking ε → 0⁺ with continuity of entrywiseExpHadamardSeries gives that entrywiseExpHadamardSeries(R) is PSD.

NOTE: This proof is simplified to avoid matrix reduction timeouts.