OAI/Combinatorics/MatchingCount/Algorithm/RationalEstimator.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.FiniteTrial.sampleAverage line 11
  2. lemma OAI.MatchingFPRAS.FiniteTrial.sampleAverage_cast line 13
  3. def OAI.MatchingFPRAS.FiniteTrial.probeMatrix line 16
  4. lemma OAI.MatchingFPRAS.FiniteTrial.probeMatrix_cast line 18
  5. lemma OAI.MatchingFPRAS.FiniteTrial.probeMatrix_symm line 22
  6. def OAI.MatchingFPRAS.FiniteTrial.estimateMatrix line 25
  7. lemma OAI.MatchingFPRAS.FiniteTrial.estimateMatrix_cast line 27
  8. lemma OAI.MatchingFPRAS.FiniteTrial.estimateMatrix_symm line 31
  9. lemma OAI.MatchingFPRAS.FiniteTrial.estimateMatrix_bounds line 34
  10. def OAI.MatchingFPRAS.FiniteTrial.sourceD line 49
  11. lemma OAI.MatchingFPRAS.FiniteTrial.sourceD_eq line 52
  12. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.matrix line 55
  13. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.matrix_bounds line 60
  14. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.matrix_symm line 62
  15. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.updateVector line 64
  16. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.updateVector_bounds line 67
  17. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.update line 73
  18. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.update_activity line 80
  19. def OAI.MatchingFPRAS.FiniteTrial.ScaleState.ratioEstimate line 87
  20. lemma OAI.MatchingFPRAS.FiniteTrial.average_A line 91
  21. lemma OAI.MatchingFPRAS.FiniteTrial.average_D line 97
  22. lemma OAI.MatchingFPRAS.FiniteTrial.average_Probe line 103
  23. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.matrix_cast line 109
  24. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.ratioEstimate_cast line 119