OAI/Combinatorics/PerfectMatching/DyadicEnvelope.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Algorithm.Piece.evalReal line 11
  2. def OAI.BinaryMatching.Algorithm.selectedReal line 13
  3. def OAI.BinaryMatching.Algorithm.psiReal line 17
  4. def OAI.BinaryMatching.Algorithm.dyadic line 19
  5. lemma OAI.BinaryMatching.Algorithm.pieces_nonempty line 21
  6. lemma OAI.BinaryMatching.Algorithm.selectedPiece_mem_argmin line 23
  7. lemma OAI.BinaryMatching.Algorithm.selectedReal_mem_argmin line 30
  8. lemma OAI.BinaryMatching.Algorithm.psiReal_le_piece line 38
  9. lemma OAI.BinaryMatching.Algorithm.le_psiReal line 42
  10. lemma OAI.BinaryMatching.Algorithm.realPsi_cast line 45
  11. lemma OAI.BinaryMatching.Algorithm.psiReal_concave line 56
  12. lemma OAI.BinaryMatching.Algorithm.mem_pieces line 71
  13. lemma OAI.BinaryMatching.Algorithm.first_mem_pieces line 76
  14. lemma OAI.BinaryMatching.Algorithm.chord_mem_pieces line 77
  15. lemma OAI.BinaryMatching.Algorithm.chord_eval line 80
  16. lemma OAI.BinaryMatching.Algorithm.first_eval line 84
  17. lemma OAI.BinaryMatching.Algorithm.dyadic_pos line 87
  18. lemma OAI.BinaryMatching.Algorithm.dyadic_nonneg line 88
  19. lemma OAI.BinaryMatching.Algorithm.dyadic_succ line 89
  20. lemma OAI.BinaryMatching.Algorithm.dyadic_zero line 90
  21. lemma OAI.BinaryMatching.Algorithm.dyadic_mul_pow line 91
  22. lemma OAI.BinaryMatching.Algorithm.dyadic_scale line 94
  23. lemma OAI.BinaryMatching.Algorithm.chord_above_knot line 103
  24. lemma OAI.BinaryMatching.Algorithm.psiReal_knot line 120
  25. lemma OAI.BinaryMatching.Algorithm.psiReal_zero line 135