OAI/Computability/LoopMatching/Accumulator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-time approximation of weighted matchings with singleton loops.

  1. def OAI.LoopMatching.Accumulator.Q line 16
  2. theorem OAI.LoopMatching.Accumulator.Q_zero line 20
  3. theorem OAI.LoopMatching.Accumulator.Q_succ line 22
  4. theorem OAI.LoopMatching.Accumulator.denominator_pos line 25
  5. theorem OAI.LoopMatching.Accumulator.quotient_eq_sum line 27
  6. theorem OAI.LoopMatching.Accumulator.Q_le_factorial_mul line 40