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

Not yet solved.