OAI/Combinatorics/ThinTrees/Encoding/BinaryReduction.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Binary reduction.

  1. lemma OAI.AlgorithmicThinTrees.sum_min_capacity line 13
  2. lemma OAI.AlgorithmicThinTrees.sum_div_rounding line 27
  3. def OAI.AlgorithmicThinTrees.BinaryInput.crossing line 48
  4. lemma OAI.AlgorithmicThinTrees.BinaryInput.cut_card line 52
  5. lemma OAI.AlgorithmicThinTrees.BinaryInput.pairs_bound line 64
  6. abbrev OAI.AlgorithmicThinTrees.BinaryInput.reduced line 112
  7. lemma OAI.AlgorithmicThinTrees.BinaryInput.reduced_crossing line 122
  8. lemma OAI.AlgorithmicThinTrees.BinaryInput.reduced_multiplicity_le line 125
  9. lemma OAI.AlgorithmicThinTrees.BinaryInput.reduced_edgeConnected line 132
  10. lemma OAI.AlgorithmicThinTrees.BinaryInput.reduced_size line 151
  11. lemma OAI.AlgorithmicThinTrees.BinaryInput.reduced_cut_upper line 164
  12. lemma OAI.StrongThinTree.MultiGraph.cut_image line 191
  13. lemma OAI.StrongThinTree.MultiGraph.spanningTree_image line 207
  14. lemma OAI.StrongThinTree.MultiGraph.cut_image_card_le line 230
  15. lemma OAI.AlgorithmicThinTrees.BinaryInput.original_copy_exists line 242
  16. def OAI.AlgorithmicThinTrees.BinaryInput.liftCopy line 249
  17. def OAI.AlgorithmicThinTrees.BinaryInput.liftLabel line 252
  18. lemma OAI.AlgorithmicThinTrees.BinaryInput.liftLabel_left line 256
  19. lemma OAI.AlgorithmicThinTrees.BinaryInput.liftLabel_right line 260
  20. lemma OAI.AlgorithmicThinTrees.BinaryInput.lift_thinTree line 264
  21. theorem OAI.AlgorithmicThinTrees.BinaryInput.reduction_correct line 287
  22. lemma OAI.AlgorithmicThinTrees.framed_nat_length_pos line 305
  23. lemma OAI.AlgorithmicThinTrees.record_count_le_bits line 309
  24. lemma OAI.AlgorithmicThinTrees.BinaryInput.vertices_le_twice_records line 321
  25. lemma OAI.AlgorithmicThinTrees.BinaryInput.records_le_encoding line 351
  26. lemma OAI.AlgorithmicThinTrees.BinaryInput.vertices_le_binary_length line 366
  27. theorem OAI.AlgorithmicThinTrees.BinaryInput.reduced_size_binary_bound line 373