A Sylvester criterion for a positive frame, and openness

IsPositiveFrame is stated as a condition on the plane a pair spans. This file gives the equivalent condition on the pair itself,

IsPositiveFrame Q x y ↔ 0 < Q x ∧ 0 < 4 * Q x * Q y - (polar Q x y) ^ 2,

which is Sylvester's criterion for the 2 × 2 Gram matrix, and which subsumes independence: a pair satisfying it spans a plane rather than a line, so the finrank = 2 clause comes free.

Both sides of the criterion are continuous, so the positive frames form an open set — the fact a genericity argument needs, and the reason this file exists.

theorem PeriodDomain.apply_smul_add_smul {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y : M) (a b : ℝ) : Q (a • x + b • y) = a * a * Q x + a * b * QuadraticMap.polar (⇑Q) x y + b * b * Q y

The value of Q on a combination, in terms of the pair's Gram data.

theorem PeriodDomain.isPositiveFrame_iff {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x y : M) : IsPositiveFrame Q x y ↔ 0 < Q x ∧ 0 < 4 * Q x * Q y - QuadraticMap.polar (⇑Q) x y ^ 2

Sylvester's criterion for a pair. The 2 × 2 Gram matrix of (x, y) is positive definite exactly when Q x and the discriminant are positive, and that is exactly the condition that the pair spans a positive plane.

theorem PeriodDomain.isOpen_setOf_isPositiveFrame {N : Type u_2} [NormedAddCommGroup N] [NormedSpace ℝ N] [FiniteDimensional ℝ N] (Q : QuadraticForm ℝ N) : IsOpen {p : N × N | IsPositiveFrame Q p.1 p.2}

The positive frames form an open set. Both halves of the Sylvester criterion are continuous.