OAI/Computability/MinUncut/Estimates/UniformGrid.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Preprocess.c_coefficient line 15
  2. lemma OAI.MinUncut.Preprocess.c_primitive line 18
  3. lemma OAI.MinUncut.Preprocess.c_qIntegral line 31
  4. lemma OAI.MinUncut.Preprocess.c_endpoint line 34
  5. lemma OAI.MinUncut.Preprocess.ca_endpoint line 41
  6. lemma OAI.MinUncut.Preprocess.ca_qIntegral line 46
  7. lemma OAI.MinUncut.Preprocess.c_midpoint line 51
  8. lemma OAI.MinUncut.Preprocess.c_rawCellWeight line 56
  9. def OAI.MinUncut.Preprocess.Grid.coordinates line 78
  10. def OAI.MinUncut.Preprocess.Grid.cells line 80
  11. def OAI.MinUncut.Preprocess.Grid.samples line 81
  12. lemma OAI.MinUncut.Preprocess.Grid.out_midpoint line 82
  13. lemma OAI.MinUncut.Preprocess.Grid.out_cellWeight line 85
  14. lemma OAI.MinUncut.Preprocess.Grid.out_gridWeight line 87
  15. def OAI.MinUncut.Preprocess.Grid.indices line 99
  16. lemma OAI.MinUncut.Preprocess.Grid.out_coord line 101
  17. lemma OAI.MinUncut.Preprocess.Grid.out_sign line 107
  18. lemma OAI.MinUncut.Preprocess.Grid.out_scoreSummand line 112
  19. lemma OAI.MinUncut.Preprocess.Grid.map_scoreTable line 133
  20. lemma OAI.MinUncut.Preprocess.UEncoding.Out.unit line 160
  21. lemma OAI.MinUncut.Preprocess.UEncoding.computable_prod line 163
  22. abbrev OAI.MinUncut.Preprocess.tests line 167
  23. instance OAI.MinUncut.Preprocess.primcodableTest line 169
  24. def OAI.MinUncut.Preprocess.Weights.localSamples line 177
  25. lemma OAI.MinUncut.Preprocess.Weights.out_rationalRowDensity line 180
  26. lemma OAI.MinUncut.Preprocess.Weights.out_rationalDensity line 193
  27. lemma OAI.MinUncut.Preprocess.Weights.out_noiseWeight line 203
  28. lemma OAI.MinUncut.Preprocess.Weights.out_localWeight line 220
  29. lemma OAI.MinUncut.Preprocess.Denominator.c_faceCardBound line 245
  30. lemma OAI.MinUncut.Preprocess.Denominator.c_gridDenominator line 249
  31. lemma OAI.MinUncut.Preprocess.Denominator.c_budgetDenominator line 262
  32. lemma OAI.MinUncut.Preprocess.Denominator.c_innerDenominator line 266
  33. lemma OAI.MinUncut.Preprocess.UEncoding.map_testCases line 282
  34. def OAI.MinUncut.Preprocess.Queries.table line 298
  35. def OAI.MinUncut.Preprocess.Queries.queryEquiv line 299
  36. def OAI.MinUncut.Preprocess.Queries.queries line 304
  37. lemma OAI.MinUncut.Preprocess.Queries.map_first line 306
  38. lemma OAI.MinUncut.Preprocess.Queries.map_left line 309
  39. lemma OAI.MinUncut.Preprocess.Queries.map_right line 312
  40. lemma OAI.MinUncut.Preprocess.Queries.map_leftEval line 326
  41. lemma OAI.MinUncut.Preprocess.Queries.map_rightEval line 342
  42. lemma OAI.MinUncut.Preprocess.Queries.map_query line 357
  43. lemma OAI.MinUncut.Preprocess.Queries.zero_map line 380
  44. lemma OAI.MinUncut.Preprocess.Queries.map_leftBase line 385
  45. lemma OAI.MinUncut.Preprocess.Queries.map_leftTableEval line 392
  46. lemma OAI.MinUncut.Preprocess.Queries.map_rightTableEval line 408
  47. lemma OAI.MinUncut.Preprocess.Queries.map_localSign line 416
  48. lemma OAI.MinUncut.Preprocess.Queries.map_leftTable line 422
  49. lemma OAI.MinUncut.Preprocess.Queries.map_rightTable line 426
  50. def OAI.MinUncut.Costed.SourceWords.signatureExpr line 436
  51. lemma OAI.MinUncut.Costed.SourceWords.signatureExpr_eval line 450
  52. def OAI.MinUncut.Costed.SourceWords.signatureLookup line 472
  53. lemma OAI.MinUncut.Costed.SourceWords.signatureLookup_eval line 474