Matrix.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Small positive semidefinite forms and Schur completion

The closed determinant criterion includes vanishing diagonal entries. The Schur estimate below consequently includes the singular axial endpoint of the quadratic comparison in Section 6 of the manuscript.

theorem OAI.PositiveEinsteinFour.quadratic_form_nonneg_of_det line 19
Source documentation
The determinant test for a symmetric two-by-two real quadratic form, including zero diagonal entries.
```
theorem quadratic_form_nonneg_of_det
    (r h s : ℝ) (hr : 0 ≤ r) (hh : 0 ≤ h) (hdet : s ^ 2 ≤ r * h)
    (x y : ℝ) :
    0 ≤ r * x ^ 2 + 2 * s * x * y + h * y ^ 2 := by
…
```
theorem OAI.PositiveEinsteinFour.quadratic_form_det_of_nonneg line 41
Source documentation
Conversely, nonnegativity of the binary form implies the closed diagonal and determinant conditions. The singular diagonal case is tested directly.
```
theorem quadratic_form_det_of_nonneg
    (r h s : ℝ)
    (hform : ∀ x y, 0 ≤ r * x ^ 2 + 2 * s * x * y + h * y ^ 2) :
    0 ≤ r ∧ 0 ≤ h ∧ s ^ 2 ≤ r * h := by
…
```

theorem OAI.PositiveEinsteinFour.schur_complement_nonneg line 62

Source documentation

Division-free Schur completion. The scalar first corner may vanish; nonnegativity of the lower form and the Schur bound handle that endpoint.

theorem schur_complement_nonneg
    (a b c f d e : ℝ) (ha : 0 ≤ a)
    (hbase : ∀ y z, 0 ≤ b * y ^ 2 + 2 * c * y * z + f * z ^ 2)
    (hschur : ∀ y z,
      (d * y + e * z) ^ 2 ≤ a * (b * y ^ 2 + 2 * c * y * z + f * z ^ 2))
    (x y z : ℝ) :
    0 ≤ a * x ^ 2 + 2 * x * (d * y + e * z) +
      b * y ^ 2 + 2 * c * y * z + f * z ^ 2 := by
…

theorem OAI.PositiveEinsteinFour.schur_zero_corner line 77
Source documentation
At a zero scalar corner, the Schur bound forces both mixed coefficients to vanish. This isolates the endpoint without a division by the corner.
```
theorem schur_zero_corner
    (b c f d e : ℝ)
    (hschur : ∀ y z,
      (d * y + e * z) ^ 2 ≤ (0 : ℝ) * (b * y ^ 2 + 2 * c * y * z + f * z ^ 2)) :
    d = 0 ∧ e = 0 := by
…
```