OAI/Computability/MaxCut/Estimates/ListSum.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OptimalMaxCut.CounterMachine.Expr.listSum line 13
  2. theorem OAI.OptimalMaxCut.CounterMachine.Expr.listSum_eval line 15
  3. def OAI.OptimalMaxCut.CounterMachine.Expr.finiteSum line 24
  4. theorem OAI.OptimalMaxCut.CounterMachine.Expr.finiteSum_eval line 26
  5. def OAI.OptimalMaxCut.CounterMachine.Expr.least line 33

    Source documentation

    First successful bounded index. All searches are expanded into finite counter loops, so the certificate does not postulate a search operation.

    def least (bound predicate : Expr) : Expr :=
…

    Mentions: OAI.OptimalMaxCut.CounterMachine.Expr

  6. theorem OAI.OptimalMaxCut.CounterMachine.Expr.least_eval line 39
  7. theorem OAI.OptimalMaxCut.CounterMachine.Expr.least_eq line 69
  8. def OAI.OptimalMaxCut.CounterMachine.Expr.Represented line 90
  9. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.const line 95
  10. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.arg line 96
  11. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.word line 97
  12. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.add line 99
  13. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.sub line 101
  14. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.mul line 103
  15. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.div line 105
  16. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.mod line 107
  17. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.pow line 109
  18. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.eq line 111
  19. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.lt line 114
  20. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.cond line 117
  21. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.sum line 121
  22. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.finiteSum line 125
  23. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.rename line 129
  24. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.subst line 133
  25. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.congr line 137
  26. theorem OAI.OptimalMaxCut.LongCode.roundedWeights_integer line 147
  27. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.degree line 167
  28. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.degree_eq line 170
  29. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.sampleLaw_weight line 178
  30. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.rowWords line 205

    Source documentation

    Exact unary game codec used by the supplied binary reduction.

    def rowWords {n q : ℕ} (c : Constraint n q) : List ℕ :=
…
  31. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.words line 207
  32. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.bits line 209
  33. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.rowWords_length line 211
  34. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.flatMap_getD line 214
  35. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.word_header line 233
  36. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.word_row line 238
  37. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.row_source line 248
  38. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.row_target line 251
  39. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.row_image line 254
  40. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.iteEq line 265
  41. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.iteAndEq line 268
  42. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.indicatorAnd line 273
  43. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.iteProp line 278
  44. theorem OAI.OptimalMaxCut.CounterMachine.Expr.Represented.bounded line 283
  45. def OAI.OptimalMaxCut.RawGrid.vertices line 296
  46. def OAI.OptimalMaxCut.RawGrid.edges line 297
  47. def OAI.OptimalMaxCut.RawGrid.row line 298
  48. def OAI.OptimalMaxCut.RawGrid.degree line 299
  49. def OAI.OptimalMaxCut.RawGrid.lookup line 301
  50. def OAI.OptimalMaxCut.RawGrid.permCode line 303
  51. def OAI.OptimalMaxCut.RawGrid.query line 305
  52. def OAI.OptimalMaxCut.RawGrid.gridSize line 307
  53. def OAI.OptimalMaxCut.RawGrid.atom line 309
  54. def OAI.OptimalMaxCut.RawGrid.weights line 316
  55. theorem OAI.OptimalMaxCut.RawGrid.Rep.vertices line 327
  56. theorem OAI.OptimalMaxCut.RawGrid.Rep.edges line 328
  57. theorem OAI.OptimalMaxCut.RawGrid.Rep.row line 329
  58. theorem OAI.OptimalMaxCut.RawGrid.Rep.degree line 332
  59. theorem OAI.OptimalMaxCut.RawGrid.Rep.lookup line 335
  60. theorem OAI.OptimalMaxCut.RawGrid.Rep.permCode line 338
  61. theorem OAI.OptimalMaxCut.RawGrid.Rep.query line 341
  62. theorem OAI.OptimalMaxCut.RawGrid.Rep.gridSize line 344
  63. theorem OAI.OptimalMaxCut.RawGrid.Rep.atom line 346
  64. theorem OAI.OptimalMaxCut.RawGrid.Rep.weights line 353