OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseTrialProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

A complete executed trajectory and fresh-observation phase trial

  1. abbrev OAI.ContingencyTables.CompanionPhaseTrialProgram.Stored line 9
  2. abbrev OAI.ContingencyTables.CompanionPhaseTrialProgram.Frame line 10
  3. abbrev OAI.ContingencyTables.CompanionPhaseTrialProgram.Input line 11
  4. def OAI.ContingencyTables.CompanionPhaseTrialProgram.trajectory line 20
  5. def OAI.ContingencyTables.CompanionPhaseTrialProgram.trajectoryRealizer line 21
  6. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.polynomial_trajectory line 24
  7. def OAI.ContingencyTables.CompanionPhaseTrialProgram.catalogue line 28
  8. def OAI.ContingencyTables.CompanionPhaseTrialProgram.catalogueRealizer line 29
  9. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.polynomial_catalogue line 33
  10. def OAI.ContingencyTables.CompanionPhaseTrialProgram.returnInput line 40
  11. def OAI.ContingencyTables.CompanionPhaseTrialProgram.returnInputRealizer line 41
  12. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.polynomial_returnInput line 42
  13. def OAI.ContingencyTables.CompanionPhaseTrialProgram.storedInput line 45
  14. def OAI.ContingencyTables.CompanionPhaseTrialProgram.storedInputRealizer line 47
  15. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.polynomial_storedInput line 51
  16. def OAI.ContingencyTables.CompanionPhaseTrialProgram.updateInput line 58
  17. def OAI.ContingencyTables.CompanionPhaseTrialProgram.updateInputRealizer line 60
  18. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.polynomial_updateInput line 62
  19. def OAI.ContingencyTables.CompanionPhaseTrialProgram.output line 69
  20. def OAI.ContingencyTables.CompanionPhaseTrialProgram.outputRealizer line 70
  21. lemma OAI.ContingencyTables.CompanionPhaseTrialProgram.polynomial_output line 73