OAI/Combinatorics/MatchingCount/Algorithm/RationalScale.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Counting.rowMaximum_cast line 11
  2. lemma OAI.MatchingFPRAS.Counting.scaleUpdate_cast line 16
  3. lemma OAI.MatchingFPRAS.Counting.scalingTrace_cast line 22
  4. lemma OAI.MatchingFPRAS.Counting.ratioEstimate_cast line 35
  5. lemma OAI.MatchingFPRAS.Counting.upperEstimate_cast line 41
  6. lemma OAI.MatchingFPRAS.Counting.sigma_cast line 47
  7. def OAI.MatchingFPRAS.FiniteTrial.cooling line 55
  8. lemma OAI.MatchingFPRAS.FiniteTrial.cooling_cast line 56
  9. def OAI.MatchingFPRAS.FiniteTrial.raw line 59
  10. lemma OAI.MatchingFPRAS.FiniteTrial.raw_cast line 61
  11. structure OAI.MatchingFPRAS.FiniteTrial.ScaleState line 66
  12. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.toReal line 71
  13. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.activity line 76
  14. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.nextActivity line 79
  15. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.activity_cast line 81
  16. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.nextActivity_cast line 85
  17. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.activity_pos line 89
  18. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.nextActivity_pos line 95
  19. def OAI.MatchingFPRAS.FiniteTrial.initialScaleState line 102
  20. lemma OAI.MatchingFPRAS.FiniteTrial.initialScaleState_cast line 109