OAI/Computability/MinUncut/Estimates/UniformEquation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.Preprocess.Source.Par line 14
  2. abbrev OAI.MinUncut.Preprocess.Source.up line 15
  3. def OAI.MinUncut.Preprocess.Source.ls line 17
  4. def OAI.MinUncut.Preprocess.Source.rs line 18
  5. def OAI.MinUncut.Preprocess.Source.fc line 19
  6. def OAI.MinUncut.Preprocess.Source.gc line 20
  7. def OAI.MinUncut.Preprocess.Source.keys line 21
  8. lemma OAI.MinUncut.Preprocess.Source.map_rawLocal line 24
  9. def OAI.MinUncut.Preprocess.Source.ds line 58
  10. def OAI.MinUncut.Preprocess.Source.tapes line 59
  11. def OAI.MinUncut.Preprocess.Source.sigs line 61
  12. def OAI.MinUncut.Preprocess.Source.sls line 62
  13. def OAI.MinUncut.Preprocess.Source.context line 63
  14. lemma OAI.MinUncut.Preprocess.Source.map_context_signature line 65
  15. lemma OAI.MinUncut.Preprocess.Source.map_context_slot line 67
  16. lemma OAI.MinUncut.Preprocess.Source.map_context_first line 69
  17. lemma OAI.MinUncut.Preprocess.Source.map_context_last line 71
  18. lemma OAI.MinUncut.Preprocess.Source.map_context_noiseTape line 73
  19. lemma OAI.MinUncut.Preprocess.Source.map_context_valid line 75
  20. lemma OAI.MinUncut.Preprocess.Source.map_context_project line 78
  21. lemma OAI.MinUncut.Preprocess.Source.map_context_noise line 85
  22. lemma OAI.MinUncut.Preprocess.Source.map_localEquation line 88
  23. lemma OAI.MinUncut.Preprocess.Syntax.C.precomp line 103
  24. lemma OAI.MinUncut.Preprocess.Syntax.O.tupleDigit line 105
  25. lemma OAI.MinUncut.Preprocess.Syntax.O.slotWord line 107
  26. abbrev OAI.MinUncut.Preprocess.Syntax.unitN line 115
  27. lemma OAI.MinUncut.Preprocess.Syntax.c_positiveExpr line 116
  28. lemma OAI.MinUncut.Preprocess.Syntax.c_sameExpr line 122
  29. lemma OAI.MinUncut.Preprocess.Syntax.c_signatureExpr line 134
  30. lemma OAI.MinUncut.Preprocess.Syntax.O.sourceLookup line 138
  31. lemma OAI.MinUncut.Preprocess.Syntax.map_sourceSlot line 143
  32. lemma OAI.MinUncut.Preprocess.Syntax.O.sourceSampled line 148
  33. def OAI.MinUncut.Preprocess.Face.axes line 167
  34. def OAI.MinUncut.Preprocess.Face.values line 168
  35. def OAI.MinUncut.Preprocess.Face.points line 169
  36. def OAI.MinUncut.Preprocess.Face.rowPairs line 170
  37. def OAI.MinUncut.Preprocess.Face.rowGood line 171
  38. lemma OAI.MinUncut.Preprocess.Face.map_rowGood line 173
  39. def OAI.MinUncut.Preprocess.Face.rowEquiv line 178
  40. def OAI.MinUncut.Preprocess.Face.rows line 201
  41. lemma OAI.MinUncut.Preprocess.Face.map_faceRow line 205
  42. lemma OAI.MinUncut.Preprocess.Face.map_faceSum line 233
  43. def OAI.MinUncut.Preprocess.Face.codeGood line 246
  44. lemma OAI.MinUncut.Preprocess.Face.map_codeGood line 249
  45. def OAI.MinUncut.Preprocess.Face.codeEquiv line 258
  46. def OAI.MinUncut.Preprocess.Face.codes line 265
  47. lemma OAI.MinUncut.Preprocess.Face.map_codeVal line 268
  48. lemma OAI.MinUncut.Preprocess.Face.map_codeMk line 275