Complementary PSD blocks bound correlations of distinct columns
ProvedConway99Formal.TwoSidedSchur.distinct_column_principal_testg and e are finite row/column index types; L is a real g-by-e matrix, and x,y are vectors on the respective index sets. In the complementary-block results, both PSD inequalities use the same L and paired complementary matrices. The exact theorem type supplies the remaining premises. Let L have real entries indexed by finite sets g×e, and assume the two complementary block quadratic forms are positive semidefinite using the same L and complementary terms. For distinct columns j,k, the product of their remaining diagonal capacities, 196 minus each squared column norm, dominates their squared inner product.
A two-column principal-minor consequence of the paired PSD hypotheses. The shared L and complementary block assumptions are essential and preserved.
import Definitions.Def_TwoSidedSchur
import Mathlib
namespace Conway99Formal.TwoSidedSchur
end Conway99Formal.TwoSidedSchur
set_option autoImplicit false
/-! Quadratic-form consequences of one complementary pair of PSD blocks. -/
open Conway99Formal.TwoSidedSchur
open Matrix
variable {g e : Type*} [Fintype g] [Fintype e]
theorem Conway99Formal.TwoSidedSchur.distinct_column_principal_test [DecidableEq e]
(L : Matrix g e ℝ) (h : ComplementaryPSD L) (j k : e) (hjk : j ≠ k) :
(196 - normSq (fun i => L i j)) * (196 - normSq (fun i => L i k)) ≥
(∑ i, L i j * L i k) ^ 2 := by sorry