OAI/Probability/SKGap/Localization/FiniteRankPositive.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.rayleigh line 14
  2. lemma OAI.SKGap.continuous_rayleigh line 17
  3. lemma OAI.SKGap.rayleigh_smul line 21
  4. lemma OAI.SKGap.rayleigh_zero line 27
  5. def OAI.SKGap.unitEuclidean line 30
  6. lemma OAI.SKGap.isCompact_unitEuclidean line 32
  7. lemma OAI.SKGap.unitEuclidean_nonempty line 36
  8. def OAI.SKGap.lowerRayleigh line 42
  9. lemma OAI.SKGap.continuous_lowerRayleigh line 44
  10. lemma OAI.SKGap.lowerRayleigh_attained line 47
  11. lemma OAI.SKGap.lowerRayleigh_le line 53
  12. lemma OAI.SKGap.unitEuclidean_normalize line 59
  13. lemma OAI.SKGap.nonneg_rayleigh_of_unit line 65
  14. lemma OAI.SKGap.rayleigh_pos_of_unit line 74
  15. lemma OAI.SKGap.lowerRayleigh_nonneg_iff line 81
  16. lemma OAI.SKGap.lowerRayleigh_pos_iff line 93
  17. theorem OAI.SKGap.matrix_path_posDef line 110
  18. def OAI.SKGap.limitingGram line 143
  19. def OAI.SKGap.rankCoefficient line 146
  20. lemma OAI.SKGap.limiting_rank_determinant line 149
  21. lemma OAI.SKGap.rankCoefficient_hermitian line 156
  22. def OAI.SKGap.limitingPositiveMatrix line 162
  23. lemma OAI.SKGap.limitingPositiveMatrix_det line 165
  24. lemma OAI.SKGap.limitingPositiveMatrix_hermitian line 182
  25. lemma OAI.SKGap.continuous_limitingPositiveMatrix line 190
  26. theorem OAI.SKGap.limitingPositiveMatrix_posDef line 198