OAI/Combinatorics/MatchingCount/Tapes/TreeSparseCertificate.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableSource.CertificateMatrixInput line 16
  2. def OAI.MatchingFPRAS.ExecutableSource.certificateCellData line 17
  3. def OAI.MatchingFPRAS.ExecutableSource.certificateCellDataRealizer line 18
  4. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_certificateCellData line 20
  5. def OAI.MatchingFPRAS.ExecutableSource.certificateMatrix line 25
  6. def OAI.MatchingFPRAS.ExecutableSource.certificateMatrixRealizer line 27
  7. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_certificateMatrix line 30
  8. lemma OAI.MatchingFPRAS.ExecutableSource.certificateMatrix_source line 37
  9. def OAI.MatchingFPRAS.ExecutableSource.sparseCertificateMatrixArg line 63
  10. def OAI.MatchingFPRAS.ExecutableSource.sparseCertificateMatrixArgRealizer line 64
  11. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseCertificateMatrixArg line 66
  12. def OAI.MatchingFPRAS.ExecutableSource.sparseCertificateData line 71
  13. def OAI.MatchingFPRAS.ExecutableSource.sparseCertificateDataRealizer line 73
  14. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseCertificateData line 75
  15. def OAI.MatchingFPRAS.ExecutableSource.sparseCertificate line 79
  16. def OAI.MatchingFPRAS.ExecutableSource.sparseCertificateRealizer line 80
  17. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_sparseCertificate line 82
  18. lemma OAI.MatchingFPRAS.ExecutableSource.sparseCertificateData_source line 86
  19. lemma OAI.MatchingFPRAS.ExecutableSource.sparseCertificate_source line 98
  20. lemma OAI.MatchingFPRAS.ExecutableSource.sparseCertificate_zero line 123
  21. theorem OAI.MatchingFPRAS.ExecutableSource.sparseCertificate_post line 142