feat: add Oppenheim inequality eval problem

FormalMathEval/LinearAlgebra/Oppenheim.lean

@@ -0,0 +1,25 @@
+import Mathlib.Analysis.Matrix.Order
+import EvalTools.Markers
+
+namespace FormalMathEval
+namespace LinearAlgebra
+
+open scoped MatrixOrder Matrix
+
+/-!
+Oppenheim's inequality (1930).
+
+For positive semidefinite matrices `A` and `B`, the determinant of the Hadamard (entrywise)
+product satisfies `det(A) · ∏ᵢ B_{ii} ≤ det(A ⊙ B)`. This strengthens the Schur product
+theorem, which only asserts that `A ⊙ B` is positive semidefinite.
+-/
+
+@[eval_problem]
+theorem oppenheim_inequality
+    {n : Type*} [Fintype n] [DecidableEq n]
+    {A B : Matrix n n ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) :
+    A.det * ∏ i, B i i ≤ (A ⊙ B).det := by
+  sorry
+
+end LinearAlgebra
+end FormalMathEval

manifests/problems.toml

@@ -230,3 +230,14 @@ submitter = "Kim Morrison"
 notes = "A foundational result in geometric group theory using the newly defined Cayley graph. Connectivity of the Cayley graph is equivalent to the generating set S generating G as a group."
 source = "A. Cayley, On the theory of groups, as depending on the symbolic equation θ^n = 1, 1878."
 informal_solution = "Forward: if connected, any g ∈ G is reached from 1 by a path, which corresponds to a product of generators. Reverse: if S generates, any g is a product of generators, giving a path from 1 to g."
+
+[[problem]]
+id = "oppenheim_inequality"
+title = "Oppenheim's inequality for Hadamard products"
+test = false
+module = "FormalMathEval.LinearAlgebra.Oppenheim"
+theorem = "oppenheim_inequality"
+submitter = "Kim Morrison"
+notes = "Oppenheim's 1930 inequality: for PSD matrices A, B, det(A ⊙ B) ≥ det(A) · ∏ᵢ Bᵢᵢ. Uses the Schur product theorem (newly formalized) as a key ingredient."
+source = "I. Schur, Bemerkungen zur Theorie der beschränkten Bilinearformen, 1911; A. Oppenheim, Inequalities connected with definite Hermitian forms, 1930."
+informal_solution = "Use induction on the matrix size, extracting a Schur complement at each step and applying the Schur product theorem to bound the determinant."