OAI/Combinatorics/MatchingCount/Algorithm/TreeGeneratedCertificate.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.NumericMarking.numeric_observableD_rep line 9
  2. def OAI.MatchingFPRAS.TreeTyped.applyFirst line 21
  3. lemma OAI.MatchingFPRAS.TreeTyped.polynomial_applyFirst line 23
  4. abbrev OAI.MatchingFPRAS.ExecutableSource.GeneratedCertificateInput line 35
  5. def OAI.MatchingFPRAS.ExecutableSource.generatedCertificate line 36
  6. def OAI.MatchingFPRAS.ExecutableSource.certificateSampleArg line 38
  7. def OAI.MatchingFPRAS.ExecutableSource.certificateSampleArgRealizer line 39
  8. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_certificateSampleArg line 41
  9. def OAI.MatchingFPRAS.ExecutableSource.certificateSample line 43
  10. def OAI.MatchingFPRAS.ExecutableSource.certificateSampleRealizer line 44
  11. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_certificateSample line 46
  12. def OAI.MatchingFPRAS.ExecutableSource.certificateReweights line 48
  13. def OAI.MatchingFPRAS.ExecutableSource.certificateReweightsRealizer line 49
  14. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_certificateReweights line 51
  15. def OAI.MatchingFPRAS.ExecutableSource.certificateArgs line 53
  16. def OAI.MatchingFPRAS.ExecutableSource.certificateArgsRealizer line 55
  17. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_certificateArgs line 57
  18. def OAI.MatchingFPRAS.ExecutableSource.generatedCertificateRealizer line 59
  19. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_generatedCertificate line 62
  20. lemma OAI.MatchingFPRAS.ExecutableSource.numeric_certificate_source line 65
  21. lemma OAI.MatchingFPRAS.ExecutableSource.generatedCertificate_source line 76
  22. theorem OAI.MatchingFPRAS.ExecutableSource.generatedCertificate_post line 97