OAI/Probability/SKGap/Matrix/PrimaryMatrix.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.Noncrossing.Primary.wordPrediction_lift line 16
  2. def OAI.SKGap.Noncrossing.Primary.matrixLetter line 32
  3. def OAI.SKGap.Noncrossing.Primary.matrixWord line 36
  4. def OAI.SKGap.Noncrossing.Primary.matrixPolynomial line 39
  5. lemma OAI.SKGap.Noncrossing.Primary.exactWord_lift line 42
  6. lemma OAI.SKGap.Noncrossing.Primary.matrixWord_append line 50
  7. lemma OAI.SKGap.Noncrossing.Primary.matrixPolynomial_append line 52
  8. lemma OAI.SKGap.Noncrossing.Primary.matrixPolynomial_prefix line 55
  9. lemma OAI.SKGap.Noncrossing.Primary.matrixPolynomial_scale line 63
  10. def OAI.SKGap.Noncrossing.Primary.primaryMatrix line 71
  11. lemma OAI.SKGap.Noncrossing.Primary.primaryPolynomial_matrix line 77
  12. lemma OAI.SKGap.Noncrossing.Primary.matrixWordSeminorm_zero line 88
  13. lemma OAI.SKGap.Noncrossing.Primary.matrixWordSeminorm_smul line 93
  14. lemma OAI.SKGap.Noncrossing.Primary.matrixWordSeminorm_list_sum line 104
  15. def OAI.SKGap.Noncrossing.Primary.coefficientMass line 112
  16. lemma OAI.SKGap.Noncrossing.Primary.polynomial_error line 114
  17. theorem OAI.SKGap.Noncrossing.Primary.primaryMatrix_seminorm line 145
  18. lemma OAI.SKGap.Noncrossing.Primary.coefficientMass_nonneg line 158
  19. lemma OAI.SKGap.Noncrossing.Primary.coefficientMass_append line 161
  20. lemma OAI.SKGap.Noncrossing.Primary.coefficientMass_prefix line 164
  21. lemma OAI.SKGap.Noncrossing.Primary.coefficientMass_scale line 168
  22. lemma OAI.SKGap.Noncrossing.Primary.mean_abs_le_one line 172
  23. def OAI.SKGap.Noncrossing.Primary.massBound line 184
  24. lemma OAI.SKGap.Noncrossing.Primary.massBound_pos line 188
  25. lemma OAI.SKGap.Noncrossing.Primary.primaryMass_bound line 193
  26. lemma OAI.SKGap.Noncrossing.Primary.primaryPolynomial_admissible line 211