OAI/Combinatorics/PerfectMatching/DyadicEntropy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.Algorithm.concave_affine_chord line 11
  2. lemma OAI.BinaryMatching.Algorithm.psiReal_on_first line 26
  3. lemma OAI.BinaryMatching.Algorithm.psiReal_on_chord line 34
  4. lemma OAI.BinaryMatching.Algorithm.dyadic_cover line 44
  5. def OAI.BinaryMatching.Algorithm.phi line 56
  6. lemma OAI.BinaryMatching.Algorithm.log_two_pos line 58
  7. lemma OAI.BinaryMatching.Algorithm.half_le_log_two line 59
  8. lemma OAI.BinaryMatching.Algorithm.log_dyadic line 65
  9. lemma OAI.BinaryMatching.Algorithm.phi_dyadic line 68
  10. lemma OAI.BinaryMatching.Algorithm.phi_zero line 72
  11. lemma OAI.BinaryMatching.Algorithm.phi_concave line 74
  12. lemma OAI.BinaryMatching.Algorithm.phi_le_one line 82
  13. lemma OAI.BinaryMatching.Algorithm.phi_mul line 95
  14. lemma OAI.BinaryMatching.Algorithm.phi_lower_first line 98
  15. lemma OAI.BinaryMatching.Algorithm.phi_lower_chord line 104
  16. lemma OAI.BinaryMatching.Algorithm.phi_upper_chord line 112
  17. lemma OAI.BinaryMatching.Algorithm.phi_error_first line 122
  18. theorem OAI.BinaryMatching.Algorithm.dyadic_entropy_error line 133