OAI/Probability/SKGap/Localization/BilinearUnion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.bilinearPathGood line 13
  2. theorem OAI.SKGap.bilinear_deterministic_equivalents line 19
  3. def OAI.SKGap.matrixPair line 102
  4. lemma OAI.SKGap.matrixPair_sub line 104
  5. lemma OAI.SKGap.matrixPair_smul line 107
  6. lemma OAI.SKGap.matrixPair_sub_right line 110
  7. lemma OAI.SKGap.matrixPair_sub_left line 113
  8. lemma OAI.SKGap.matrixPair_smul_right line 116
  9. lemma OAI.SKGap.matrixPair_smul_left line 119
  10. lemma OAI.SKGap.matrixPair_mul_right line 122
  11. lemma OAI.SKGap.matrixPair_symm line 125
  12. lemma OAI.SKGap.matrixPair_mul_left line 128
  13. def OAI.SKGap.residualGramVector line 137
  14. lemma OAI.SKGap.centered_gram_mixed line 140
  15. lemma OAI.SKGap.centered_gram_diagonal line 147
  16. lemma OAI.SKGap.centered_gram_mixed_bound line 167
  17. lemma OAI.SKGap.centered_gram_diagonal_bound line 180