OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorBlockProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Executed sample blocks and the product weight estimator

The lists contain the actual sample inputs and their disjoint finite words. Each sample is evaluated by the checked binary program before its average or product is formed.

  1. abbrev OAI.ContingencyTables.RootedEstimatorBlockProgram.RatioBlock line 18
  2. abbrev OAI.ContingencyTables.RootedEstimatorBlockProgram.CorrectionBlock line 19
  3. def OAI.ContingencyTables.RootedEstimatorBlockProgram.ratioAverage line 21
  4. def OAI.ContingencyTables.RootedEstimatorBlockProgram.ratioAverageRealizer line 23
  5. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.polynomial_ratioAverage line 27
  6. def OAI.ContingencyTables.RootedEstimatorBlockProgram.correctionAverage line 31
  7. def OAI.ContingencyTables.RootedEstimatorBlockProgram.correctionAverageRealizer line 33
  8. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.polynomial_correctionAverage line 37
  9. abbrev OAI.ContingencyTables.RootedEstimatorBlockProgram.Input line 41
  10. def OAI.ContingencyTables.RootedEstimatorBlockProgram.ratioProduct line 45
  11. def OAI.ContingencyTables.RootedEstimatorBlockProgram.ratioProductRealizer line 47
  12. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.polynomial_ratioProduct line 52
  13. def OAI.ContingencyTables.RootedEstimatorBlockProgram.factors line 57
  14. def OAI.ContingencyTables.RootedEstimatorBlockProgram.factorsRealizer line 59
  15. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.polynomial_factors line 63
  16. def OAI.ContingencyTables.RootedEstimatorBlockProgram.output line 67
  17. def OAI.ContingencyTables.RootedEstimatorBlockProgram.outputRealizer line 68
  18. theorem OAI.ContingencyTables.RootedEstimatorBlockProgram.polynomial_output line 71
  19. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.ratioAverage_value line 76
  20. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.correctionAverage_value line 82
  21. lemma OAI.ContingencyTables.RootedEstimatorBlockProgram.output_value line 88