Oppenheim's inequality for Hadamard products

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.

theorem declaration uses `sorry`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 := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝB:Matrix n n ℝhA:A.PosSemidefhB:B.PosSemidef⊢ A.det * ∏ i, B i i ≤ (A ⊙ B).det
  sorryAll goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 8, 2026 (proof)

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 18, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026