OAI/Combinatorics/PerfectMatching/SizeBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Algorithm.inputLength line 11
  2. lemma OAI.BinaryMatching.Algorithm.encodeNat_length line 13
  3. lemma OAI.BinaryMatching.Algorithm.encodeRecord_length line 16
  4. lemma OAI.BinaryMatching.Algorithm.records_length_le_input line 21
  5. lemma OAI.BinaryMatching.Algorithm.record_bits_le_input line 32
  6. lemma OAI.BinaryMatching.Algorithm.log2_le_bits line 42
  7. lemma OAI.BinaryMatching.Algorithm.B_le_input line 48
  8. lemma OAI.BinaryMatching.Algorithm.covered_card_le_records line 54
  9. lemma OAI.BinaryMatching.Algorithm.positive_count_order_bound line 65
  10. lemma OAI.BinaryMatching.Algorithm.multiplicity_pow_bound line 69
  11. lemma OAI.BinaryMatching.Algorithm.count_pow_bound line 73
  12. lemma OAI.BinaryMatching.Algorithm.approximate_bits_bound line 87
  13. theorem OAI.BinaryMatching.Algorithm.approximate_polynomial_output line 109