OAI/Probability/SKGap/Matrix/PrimitiveTrace.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Recipe.testSize line 17
  2. lemma OAI.SKGapCutoff.Recipe.testSize_nonneg line 18
  3. lemma OAI.SKGapCutoff.Recipe.opNorm_le_testSize line 19
  4. structure OAI.SKGapCutoff.Recipe.TraceControl line 21
  5. lemma OAI.SKGapCutoff.Recipe.TraceControl.zero line 25
  6. lemma OAI.SKGapCutoff.Recipe.TraceControl.mono line 26
  7. lemma OAI.SKGapCutoff.Recipe.TraceControl.add line 28
  8. lemma OAI.SKGapCutoff.Recipe.TraceControl.smul line 33
  9. lemma OAI.SKGapCutoff.Recipe.TraceControl.neg line 38
  10. lemma OAI.SKGapCutoff.Recipe.TraceControl.sub line 40
  11. lemma OAI.SKGapCutoff.Recipe.TraceControl.sum line 42
  12. lemma OAI.SKGapCutoff.Recipe.control_of_operator line 48
  13. lemma OAI.SKGapCutoff.Recipe.small_diagonal_control line 52
  14. lemma OAI.SKGapCutoff.Recipe.small_mean_control line 56
  15. lemma OAI.SKGapCutoff.Recipe.averageError_control line 60
  16. lemma OAI.SKGapCutoff.Recipe.primary_averageError_control line 64
  17. lemma OAI.SKGapCutoff.Recipe.sourceError_control line 72
  18. abbrev OAI.SKGapCutoff.Recipe.OrdinaryWord line 113
  19. def OAI.SKGapCutoff.Recipe.wordBounded line 114
  20. lemma OAI.SKGapCutoff.Recipe.wordBounded_diag line 116
  21. lemma OAI.SKGapCutoff.Recipe.wordBounded_noise line 121
  22. def OAI.SKGapCutoff.Recipe.WordTestBound line 127
  23. def OAI.SKGapCutoff.Recipe.errorBudget line 130
  24. lemma OAI.SKGapCutoff.Recipe.errorBudget_nonneg line 134
  25. theorem OAI.SKGapCutoff.Recipe.finite_graph_trace line 144