OAI/Analysis/HyperbolicCones/LeastEigenvalue.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The least spectral value and its continuity in the real symmetric matrix space.

  1. def OAI.Paper256.leastEigenvalue line 14
  2. theorem OAI.Paper256.leastEigenvalue_isLeast line 17
  3. theorem OAI.Paper256.leastEigenvalue_nonneg_iff line 45
  4. theorem OAI.Paper256.leastEigenvalue_neg_iff line 57
  5. theorem OAI.Paper256.continuous_leastEigenvalue line 61
  6. theorem OAI.Paper256.leastEigenvalue_tendsto line 66
  7. theorem OAI.Paper256.leastEigenvalue_pos_iff line 71
  8. theorem OAI.Paper256.det_eq_zero_of_leastEigenvalue_eq_zero line 84
  9. theorem OAI.Paper256.exists_positive_singular_on_segment line 91