OAI/Combinatorics/VariableWL/MachineReduction.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.MachineOneHead.linearConstant line 10
  2. def OAI.VariableWL.MachineOneHead.quadraticConstant line 11
  3. theorem OAI.VariableWL.MachineOneHead.stackTime_le line 15
  4. theorem OAI.VariableWL.MachineOneHead.time_le line 20
  5. def OAI.VariableWL.MachineOneHead.inputExponent line 46
  6. def OAI.VariableWL.MachineOneHead.simulationExponent line 47
  7. def OAI.VariableWL.MachineOneHead.addressBits line 49
  8. theorem OAI.VariableWL.MachineOneHead.inputExponent_ge_time line 51
  9. theorem OAI.VariableWL.MachineOneHead.inputExponent_ge_length line 57
  10. theorem OAI.VariableWL.MachineOneHead.exponential_input_bound line 63
  11. theorem OAI.VariableWL.MachineOneHead.simulation_bound line 72
  12. theorem OAI.VariableWL.MachineOneHead.input_fits_budget line 84
  13. theorem OAI.VariableWL.MachineOneHead.ring_budget line 90
  14. theorem OAI.VariableWL.MachineOneHead.addressBits_ge_four line 98
  15. theorem OAI.VariableWL.MachineOneHead.addressBits_polynomial line 102
  16. abbrev OAI.VariableWL.MachineReduction.Letter line 115
  17. instance OAI.VariableWL.MachineReduction.letterFintype line 116
  18. def OAI.VariableWL.MachineReduction.bits line 117
  19. def OAI.VariableWL.MachineReduction.dimension line 118
  20. def OAI.VariableWL.MachineReduction.internal line 119
  21. theorem OAI.VariableWL.MachineReduction.fits line 121
  22. def OAI.VariableWL.MachineReduction.circuit line 127
  23. abbrev OAI.VariableWL.MachineReduction.Real line 131
  24. abbrev OAI.VariableWL.MachineReduction.Comparison line 134
  25. def OAI.VariableWL.MachineReduction.imageInstance line 138
  26. instance OAI.VariableWL.MachineReduction.realFintype line 141
  27. instance OAI.VariableWL.MachineReduction.comparisonFintype line 142
  28. instance OAI.VariableWL.MachineReduction.realNonempty line 149
  29. theorem OAI.VariableWL.MachineReduction.dimension_large line 151
  30. theorem OAI.VariableWL.MachineReduction.internal_pos line 156
  31. theorem OAI.VariableWL.MachineReduction.enough_links line 158
  32. def OAI.VariableWL.MachineReduction.marked line 162
  33. def OAI.VariableWL.MachineReduction.generalGraph line 164
  34. def OAI.VariableWL.MachineReduction.subcubicGraph line 167
  35. theorem OAI.VariableWL.MachineReduction.consistent_iff_output line 171
  36. theorem OAI.VariableWL.MachineReduction.general_correct line 184
  37. theorem OAI.VariableWL.MachineReduction.subcubic_correct line 191
  38. theorem OAI.VariableWL.MachineReduction.subcubic_promise line 198
  39. theorem OAI.VariableWL.MachineReduction.general_promise line 205
  40. theorem OAI.VariableWL.MachineReduction.dimension_polynomial line 210
  41. theorem OAI.VariableWL.RealizationSize.dimension_le_two line 225
  42. theorem OAI.VariableWL.RealizationSize.horizontal_card line 230
  43. theorem OAI.VariableWL.RealizationSize.square_card line 241
  44. theorem OAI.VariableWL.RealizationSize.block_card line 251
  45. theorem OAI.VariableWL.RealizationSize.coordinate_card line 260
  46. theorem OAI.VariableWL.RealizationSize.rawValue_card line 272
  47. theorem OAI.VariableWL.RealizationSize.valuation_card line 278
  48. theorem OAI.VariableWL.RealizationSize.general_base_card line 282
  49. theorem OAI.VariableWL.RealizationSize.general_leaves line 289
  50. theorem OAI.VariableWL.RealizationSize.general_order line 296
  51. def OAI.VariableWL.RealizationSize.readoutSet line 321
  52. theorem OAI.VariableWL.RealizationSize.readout_card line 325
  53. theorem OAI.VariableWL.RealizationSize.proper_card line 341
  54. theorem OAI.VariableWL.RealizationSize.data_dimension line 355
  55. theorem OAI.VariableWL.RealizationSize.data_channels line 358
  56. theorem OAI.VariableWL.PrefixParts.Data.valuation_card_bound line 370
  57. theorem OAI.VariableWL.PrefixParts.Data.tree_card_bound line 376
  58. theorem OAI.VariableWL.PrefixParts.Data.vertex_card_bound line 385
  59. theorem OAI.VariableWL.PrefixParts.Data.sort_card_bound line 392
  60. theorem OAI.VariableWL.RealizationSize.owner_card line 412
  61. theorem OAI.VariableWL.RealizationSize.sort_card line 423
  62. theorem OAI.VariableWL.RealizationSize.subcubic_order line 434