OAI/Combinatorics/ContingencyTables/Counting/CompanionPhaseContextProgram.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Computing a phase configuration from immutable prepared data

The reserve is used only through its length. All precision-marker bits are false, so the physical configuration is independent of the random contents of the word that provides its bounded allocation.

  1. abbrev OAI.ContingencyTables.CompanionPhaseContextProgram.Prepared line 17
  2. abbrev OAI.ContingencyTables.CompanionPhaseContextProgram.Input line 18
  3. def OAI.ContingencyTables.CompanionPhaseContextProgram.noise line 20
  4. def OAI.ContingencyTables.CompanionPhaseContextProgram.noiseRealizer line 21
  5. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.polynomial_noise line 24
  6. def OAI.ContingencyTables.CompanionPhaseContextProgram.precision line 28
  7. def OAI.ContingencyTables.CompanionPhaseContextProgram.precisionRealizer line 29
  8. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.polynomial_precision line 32
  9. def OAI.ContingencyTables.CompanionPhaseContextProgram.scalar line 36
  10. def OAI.ContingencyTables.CompanionPhaseContextProgram.scalarRealizer line 38
  11. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.polynomial_scalar line 41
  12. def OAI.ContingencyTables.CompanionPhaseContextProgram.falseReserve line 45
  13. def OAI.ContingencyTables.CompanionPhaseContextProgram.falseReserveRealizer line 46
  14. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.polynomial_falseReserve line 47
  15. def OAI.ContingencyTables.CompanionPhaseContextProgram.configInput line 50
  16. def OAI.ContingencyTables.CompanionPhaseContextProgram.configInputRealizer line 52
  17. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.polynomial_configInput line 55
  18. def OAI.ContingencyTables.CompanionPhaseContextProgram.config line 60
  19. def OAI.ContingencyTables.CompanionPhaseContextProgram.configRealizer line 62
  20. theorem OAI.ContingencyTables.CompanionPhaseContextProgram.polynomial_config line 65
  21. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.falseReserve_length line 68
  22. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.falseReserve_eq line 70
  23. def OAI.ContingencyTables.CompanionPhaseContextProgram.data line 81
  24. lemma OAI.ContingencyTables.CompanionPhaseContextProgram.config_data line 87