OAI/Combinatorics/VariableWL/RefinementTable.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.MachineReduction.schemaConstant line 10
  2. theorem OAI.VariableWL.MachineReduction.input_le_bits line 13
  3. theorem OAI.VariableWL.MachineReduction.kind_card line 19
  4. theorem OAI.VariableWL.MachineReduction.triple_card line 24
  5. theorem OAI.VariableWL.MachineReduction.edge_card line 28
  6. theorem OAI.VariableWL.MachineReduction.real_card line 35
  7. theorem OAI.VariableWL.MachineReduction.comparison_card line 55
  8. theorem OAI.VariableWL.MachineReduction.bits_le_dimension line 81
  9. theorem OAI.VariableWL.MachineReduction.schemas_in_dimension line 83
  10. theorem OAI.VariableWL.MachineReduction.blocks_card line 90
  11. def OAI.VariableWL.RefinementTable.sameCounts line 108
  12. theorem OAI.VariableWL.RefinementTable.sameCounts_iff line 111
  13. abbrev OAI.VariableWL.RefinementTable.Entry line 142
  14. abbrev OAI.VariableWL.RefinementTable.Vector line 143
  15. def OAI.VariableWL.RefinementTable.neighbors line 145
  16. def OAI.VariableWL.RefinementTable.vectorEqual line 149
  17. def OAI.VariableWL.RefinementTable.update line 152
  18. theorem OAI.VariableWL.RefinementTable.vectorEqual_iff line 155
  19. theorem OAI.VariableWL.RefinementTable.neighbors_color line 161
  20. theorem OAI.VariableWL.RefinementTable.update_correct line 175
  21. def OAI.VariableWL.RefinementTable.initial line 187
  22. def OAI.VariableWL.RefinementTable.table line 190
  23. theorem OAI.VariableWL.RefinementTable.table_correct line 194
  24. def OAI.VariableWL.RefinementTable.histogramEqual line 200
  25. theorem OAI.VariableWL.RefinementTable.histogramEqual_correct line 204
  26. def OAI.VariableWL.RefinementTable.accepts line 212
  27. theorem OAI.VariableWL.RefinementTable.accepts_correct line 214
  28. theorem OAI.VariableWL.RealizationSize.general_order_polynomial line 224
  29. theorem OAI.VariableWL.RealizationSize.subcubic_order_polynomial line 231
  30. theorem OAI.VariableWL.MachineReduction.blocks_succ_bound line 250
  31. theorem OAI.VariableWL.MachineReduction.general_order_dimension line 257
  32. theorem OAI.VariableWL.MachineReduction.subcubic_order_dimension line 265
  33. def OAI.VariableWL.MachineReduction.dimensionConstant line 274
  34. theorem OAI.VariableWL.MachineReduction.dimension_succ_polynomial line 276
  35. theorem OAI.VariableWL.MachineReduction.general_order_input line 283
  36. theorem OAI.VariableWL.MachineReduction.subcubic_order_input line 292
  37. def OAI.VariableWL.MachineReduction.generalWord line 301
  38. def OAI.VariableWL.MachineReduction.subcubicWord line 303
  39. theorem OAI.VariableWL.MachineReduction.generalWord_correct line 306
  40. theorem OAI.VariableWL.MachineReduction.subcubicWord_correct line 312