OAI/Combinatorics/MatchingCount/Algorithm/TreeGeneratedUpdate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableSource.GeneratedUpdateData line 14
  2. abbrev OAI.MatchingFPRAS.ExecutableSource.GeneratedUpdateInput line 15
  3. def OAI.MatchingFPRAS.ExecutableSource.generatedUpdateArg line 17
  4. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_generatedUpdateArg line 19
  5. def OAI.MatchingFPRAS.ExecutableSource.generatedUpdateSetup line 25
  6. def OAI.MatchingFPRAS.ExecutableSource.generatedUpdateSetupRealizer line 27
  7. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_generatedUpdateSetup line 30
  8. def OAI.MatchingFPRAS.ExecutableSource.updateWith line 35
  9. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_updateWith line 40
  10. def OAI.MatchingFPRAS.ExecutableSource.generatedUpdate line 49
  11. def OAI.MatchingFPRAS.ExecutableSource.generatedUpdateRealizer line 51
  12. lemma OAI.MatchingFPRAS.ExecutableSource.polynomial_generatedUpdate line 52
  13. def OAI.MatchingFPRAS.ExecutableSource.generatedSourceSample line 56
  14. lemma OAI.MatchingFPRAS.ExecutableSource.numericMarks_selected line 71
  15. lemma OAI.MatchingFPRAS.ExecutableSource.generatedMarked_sourceSample line 80
  16. lemma OAI.MatchingFPRAS.ExecutableSource.generatedSamples_source line 97
  17. lemma OAI.MatchingFPRAS.ExecutableSource.generatedUpdate_source line 115
  18. theorem OAI.MatchingFPRAS.ExecutableSource.generatedUpdate_post line 148