OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseFinishProgram.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Executing the observed ratio and learned phase update

The supplied pairs contain the current and next weight queries for every observed state. Only plain states contribute to the ratio. The same actual trajectory supplies the plain/defect counts and the abort test.

  1. abbrev OAI.ContingencyTables.CompanionPhaseFinishProgram.Fraction line 16
  2. abbrev OAI.ContingencyTables.CompanionPhaseFinishProgram.Stored line 17
  3. abbrev OAI.ContingencyTables.CompanionPhaseFinishProgram.Input line 18
  4. abbrev OAI.ContingencyTables.CompanionPhaseFinishProgram.TermInput line 19
  5. def OAI.ContingencyTables.CompanionPhaseFinishProgram.term line 21
  6. def OAI.ContingencyTables.CompanionPhaseFinishProgram.termRealizer line 23
  7. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_term line 29
  8. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.term_den_pos line 35
  9. def OAI.ContingencyTables.CompanionPhaseFinishProgram.trajectory line 41
  10. def OAI.ContingencyTables.CompanionPhaseFinishProgram.trajectoryRealizer line 42
  11. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_trajectory line 43
  12. def OAI.ContingencyTables.CompanionPhaseFinishProgram.indices line 46
  13. def OAI.ContingencyTables.CompanionPhaseFinishProgram.indicesRealizer line 47
  14. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_indices line 49
  15. def OAI.ContingencyTables.CompanionPhaseFinishProgram.termInput line 58
  16. def OAI.ContingencyTables.CompanionPhaseFinishProgram.termInputRealizer line 60
  17. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_termInput line 64
  18. def OAI.ContingencyTables.CompanionPhaseFinishProgram.indexedTerm line 73
  19. def OAI.ContingencyTables.CompanionPhaseFinishProgram.indexedTermRealizer line 74
  20. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_indexedTerm line 76
  21. def OAI.ContingencyTables.CompanionPhaseFinishProgram.terms line 79
  22. def OAI.ContingencyTables.CompanionPhaseFinishProgram.termsRealizer line 80
  23. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_terms line 81
  24. def OAI.ContingencyTables.CompanionPhaseFinishProgram.total line 87
  25. def OAI.ContingencyTables.CompanionPhaseFinishProgram.totalRealizer line 88
  26. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_total line 90
  27. def OAI.ContingencyTables.CompanionPhaseFinishProgram.count line 93
  28. def OAI.ContingencyTables.CompanionPhaseFinishProgram.countRealizer line 94
  29. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_count line 96
  30. def OAI.ContingencyTables.CompanionPhaseFinishProgram.ratio line 99
  31. def OAI.ContingencyTables.CompanionPhaseFinishProgram.ratioRealizer line 100
  32. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_ratio line 103
  33. def OAI.ContingencyTables.CompanionPhaseFinishProgram.estimate line 108
  34. def OAI.ContingencyTables.CompanionPhaseFinishProgram.estimateRealizer line 109
  35. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_estimate line 112
  36. def OAI.ContingencyTables.CompanionPhaseFinishProgram.next line 116
  37. def OAI.ContingencyTables.CompanionPhaseFinishProgram.nextRealizer line 117
  38. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_next line 120
  39. def OAI.ContingencyTables.CompanionPhaseFinishProgram.output line 126
  40. def OAI.ContingencyTables.CompanionPhaseFinishProgram.outputRealizer line 128
  41. lemma OAI.ContingencyTables.CompanionPhaseFinishProgram.polynomial_output line 131