OAI/Probability/SKGap/Matrix/WordTemplateSurjective.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.inverseChart line 14
  2. def OAI.SKGap.diagonalChart line 17
  3. lemma OAI.SKGap.inverseChart_exact line 24
  4. lemma OAI.SKGap.diagonalChart_exact line 28
  5. def OAI.SKGap.WordLetter.diagonalValue line 34
  6. lemma OAI.SKGap.WordLetter.diagonalValue_bound line 37
  7. theorem OAI.SKGap.templateWord_surjective line 44
  8. theorem OAI.SKGap.all_actualWords_gaussian_chaining line 90
  9. lemma OAI.SKGap.WordLetter.sign line 120
  10. lemma OAI.SKGap.actualWord_sign line 128
  11. theorem OAI.SKGap.actualWord_offdiag_mean line 140