OAI/Combinatorics/ContingencyTables/Counting/CompanionRestartInitializer.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

The computed finite initializer used before every restart experiment

  1. abbrev OAI.ContingencyTables.CompanionRestartInitializer.Prepared line 10
  2. abbrev OAI.ContingencyTables.CompanionRestartInitializer.Input line 11
  3. def OAI.ContingencyTables.CompanionRestartInitializer.forest line 13
  4. def OAI.ContingencyTables.CompanionRestartInitializer.forestRealizer line 14
  5. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_forest line 16
  6. def OAI.ContingencyTables.CompanionRestartInitializer.cellInput line 22
  7. def OAI.ContingencyTables.CompanionRestartInitializer.cellInputRealizer line 24
  8. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_cellInput line 30
  9. def OAI.ContingencyTables.CompanionRestartInitializer.fields line 37
  10. def OAI.ContingencyTables.CompanionRestartInitializer.fieldsRealizer line 38
  11. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_fields line 43
  12. def OAI.ContingencyTables.CompanionRestartInitializer.initialBound line 51
  13. def OAI.ContingencyTables.CompanionRestartInitializer.initialExponent line 52
  14. def OAI.ContingencyTables.CompanionRestartInitializer.scalar line 53
  15. def OAI.ContingencyTables.CompanionRestartInitializer.scalarRealizer line 54
  16. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_scalar line 56
  17. def OAI.ContingencyTables.CompanionRestartInitializer.precision line 59
  18. def OAI.ContingencyTables.CompanionRestartInitializer.precisionRealizer line 60
  19. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_precision line 66
  20. def OAI.ContingencyTables.CompanionRestartInitializer.capacities line 71
  21. def OAI.ContingencyTables.CompanionRestartInitializer.capacitiesRealizer line 72
  22. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_capacities line 75
  23. def OAI.ContingencyTables.CompanionRestartInitializer.width line 78
  24. def OAI.ContingencyTables.CompanionRestartInitializer.widthRealizer line 79
  25. theorem OAI.ContingencyTables.CompanionRestartInitializer.polynomial_width line 84
  26. def OAI.ContingencyTables.CompanionRestartInitializer.prepare line 88
  27. def OAI.ContingencyTables.CompanionRestartInitializer.prepareRealizer line 89
  28. lemma OAI.ContingencyTables.CompanionRestartInitializer.polynomial_prepare line 92
  29. def OAI.ContingencyTables.CompanionRestartInitializer.output line 96
  30. def OAI.ContingencyTables.CompanionRestartInitializer.outputRealizer line 97
  31. theorem OAI.ContingencyTables.CompanionRestartInitializer.polynomial_output line 100
  32. def OAI.ContingencyTables.CompanionRestartInitializer.data line 109
  33. lemma OAI.ContingencyTables.CompanionRestartInitializer.cellInput_data line 115
  34. lemma OAI.ContingencyTables.CompanionRestartInitializer.precision_data line 120
  35. lemma OAI.ContingencyTables.CompanionRestartInitializer.width_data line 128
  36. theorem OAI.ContingencyTables.CompanionRestartInitializer.output_sameLaw line 139