feat: add entrywise exponential PSD eval problem

Uses the newly formalized Schur product theorem (PosSemidef.hadamard)
to state that the entrywise exponential of a PSD matrix is PSD
(Schoenberg 1942, Schur-Polya-Loewner theory).

Bumps mathlib to include the Schur product theorem PR.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: kim-em

FormalMathEval/LinearAlgebra/EntrywiseExpPSD.lean

@@ -0,0 +1,32 @@
+import Mathlib.Analysis.Matrix.Order
+import Mathlib.Analysis.SpecialFunctions.ExpDeriv
+import EvalTools.Markers
+
+namespace FormalMathEval
+namespace LinearAlgebra
+
+open scoped MatrixOrder Matrix
+
+/-!
+The entrywise exponential of a positive semidefinite matrix is positive semidefinite.
+
+This is a consequence of the Schur product theorem (Schur 1911) and the Taylor expansion
+of the exponential function. The key idea is that `exp_⊙(A)_{ij} = exp(a_{ij})` can be
+written as the convergent series `∑ₖ (1/k!) A^{⊙k}`, where `A^{⊙k}` denotes the k-fold
+Hadamard product. Each `A^{⊙k}` is positive semidefinite by iterated application of the
+Schur product theorem, and a convergent nonnegative combination of PSD matrices is PSD.
+
+This result is part of the Schur–Pólya–Loewner theory of entrywise functions preserving
+positive semidefiniteness, with applications in statistics (correlation matrices) and
+quantum information theory (density matrices).
+-/
+
+@[eval_problem]
+theorem posSemidef_map_exp
+    {n : Type*} [Fintype n] [DecidableEq n]
+    {A : Matrix n n ℝ} (hA : A.PosSemidef) :
+    (A.map Real.exp).PosSemidef := by
+  sorry
+
+end LinearAlgebra
+end FormalMathEval

manifests/problems.toml

@@ -186,3 +186,14 @@ submitter = "Kim Morrison"
 notes = "A concrete stable-family homotopy-group computation."
 source = "Classical theorem in unstable homotopy theory."
 informal_solution = "Use suspension and the stable range to show the first stable stem is Z/2."
+
+[[problem]]
+id = "posSemidef_map_exp"
+title = "Entrywise exponential of a PSD matrix is PSD"
+test = false
+module = "FormalMathEval.LinearAlgebra.EntrywiseExpPSD"
+theorem = "posSemidef_map_exp"
+submitter = "Kim Morrison"
+notes = "Part of the Schur-Polya-Loewner theory of entrywise functions preserving PSD. The proof uses the Schur product theorem iteratively: exp_⊙(A) = ∑ A^{⊙k}/k!, each Hadamard power is PSD, and the convergent series of PSD matrices is PSD."
+source = "I.J. Schoenberg, Positive definite functions on spheres, 1942."
+informal_solution = "Write exp(a_{ij}) as the convergent series ∑ (a_{ij})^k / k!. The matrix with entries (a_{ij})^k is the k-fold Hadamard product A^{⊙k}, which is PSD by iterated Schur product. The partial sums are nonneg combinations of PSD matrices, hence PSD. PSD is a closed condition, so the limit is PSD."