OAI/Combinatorics/MatchingCount/Arithmetic/TreeAdaptiveArithmetic.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableAdaptive.ProbeTable line 13
  2. abbrev OAI.MatchingFPRAS.ExecutableAdaptive.MatrixData line 14
  3. def OAI.MatchingFPRAS.ExecutableAdaptive.orderedPair line 16
  4. def OAI.MatchingFPRAS.ExecutableAdaptive.orderedPairRealizer line 17
  5. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_orderedPair line 19
  6. def OAI.MatchingFPRAS.ExecutableAdaptive.probeValue line 22
  7. def OAI.MatchingFPRAS.ExecutableAdaptive.probeValueRealizer line 24
  8. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_probeValue line 27
  9. def OAI.MatchingFPRAS.ExecutableAdaptive.estimateCell line 33
  10. def OAI.MatchingFPRAS.ExecutableAdaptive.estimateCellRealizer line 35
  11. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_estimateCell line 37
  12. def OAI.MatchingFPRAS.ExecutableAdaptive.estimateRow line 43
  13. def OAI.MatchingFPRAS.ExecutableAdaptive.estimateRowRealizer line 45
  14. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_estimateRow line 48
  15. def OAI.MatchingFPRAS.ExecutableAdaptive.estimateMatrix line 53
  16. def OAI.MatchingFPRAS.ExecutableAdaptive.estimateMatrixRealizer line 54
  17. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_estimateMatrix line 55
  18. def OAI.MatchingFPRAS.ExecutableAdaptive.multiplyVector line 59
  19. def OAI.MatchingFPRAS.ExecutableAdaptive.multiplyVectorRealizer line 61
  20. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_multiplyVector line 64
  21. def OAI.MatchingFPRAS.ExecutableAdaptive.updateVector line 70
  22. def OAI.MatchingFPRAS.ExecutableAdaptive.updateVectorRealizer line 71
  23. lemma OAI.MatchingFPRAS.ExecutableAdaptive.polynomial_updateVector line 74
  24. lemma OAI.MatchingFPRAS.ExecutableAdaptive.orderedPair_fin line 80
  25. lemma OAI.MatchingFPRAS.ExecutableAdaptive.probeValue_rep line 87
  26. lemma OAI.MatchingFPRAS.ExecutableAdaptive.estimateMatrix_rep line 98
  27. lemma OAI.MatchingFPRAS.ExecutableAdaptive.multiplyVector_rep line 117
  28. lemma OAI.MatchingFPRAS.ExecutableAdaptive.updateVector_rep line 128