A reciprocal sum is minimized at the midpoint
ProvedConway99Formal.TwoSidedSchur.reciprocal_sum_boundconditional-source-resultconway99-formal-project-20261003familytwo-sided-schurmetadata-only-not-proofreciprocal-inequalityscalar-lemma
g 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. For a real number a strictly between 0 and 28, the sum of reciprocals of the two complementary parts is at least 1/7.
A scalar inequality used in the two-sided Schur argument; it has no graph assumption.
Preamble
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]
Formal statement
theorem Conway99Formal.TwoSidedSchur.reciprocal_sum_bound (a : ℝ) (ha : 0 < a) (hb : a < 28) :
1 / 7 ≤ 1 / a + 1 / (28 - a) := by sorry
Source
Exact original Lean source: formalization/2026-10-03/two-sided-schur/TwoSidedSchur.lean#L81-L93; source commit a45708acebe3f397faccb1b646be906f24f23ee5; source SHA-256 61d8a9ae110b34e6c9ea60c974ec342f79de6b77c383dd7b756583ac0b54a3e8. Mechanically extracted declaration: blob/a45708acebe3f397faccb1b646be906f24f23ee5/formalization/2026-10-03/two-sided-schur/TwoSidedSchur.lean#L81-L93.