OAI/Combinatorics/TreeEdit/RandomCode.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TreeEdit.card_orderEmb_le_choose line 11
  2. theorem OAI.TreeEdit.card_prescribed_bits line 30
  3. theorem OAI.TreeEdit.choose_weight_bound line 48
  4. theorem OAI.TreeEdit.choose_matching_bound line 57
  5. theorem OAI.TreeEdit.card_agreement_embedding line 91
  6. def OAI.TreeEdit.segmentPositions line 112
  7. theorem OAI.TreeEdit.card_matched_segments line 116
  8. theorem OAI.TreeEdit.large_lcs_segment_witness line 144
  9. theorem OAI.TreeEdit.card_bad_segment line 166
  10. def OAI.TreeEdit.VectorSeparated line 196
  11. theorem OAI.TreeEdit.VectorSeparated.symm line 200
  12. theorem OAI.TreeEdit.card_bad_vector line 208
  13. theorem OAI.TreeEdit.exists_separated_vectors line 245
  14. theorem OAI.TreeEdit.exists_segment_code line 292
  15. def OAI.TreeEdit.sourceCodeCutoff line 301
  16. theorem OAI.TreeEdit.sourceCodeCutoff_bounds line 304
  17. theorem OAI.TreeEdit.cutoff_dyadic_domination line 329
  18. theorem OAI.TreeEdit.sourceCodeCutoff_absorb line 337
  19. theorem OAI.TreeEdit.polynomial_code_count line 349
  20. theorem OAI.TreeEdit.source_segment_code_exists line 365
  21. theorem OAI.TreeEdit.binary_conversion line 375