OAI/Combinatorics/UniformKServer/StarOutputData.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Concrete data for the output rules, including the signed total cap error. All rank and tracker quantities are derived from the finite hidden law.

  1. def OAI.UniformKServer.StarOutputData.core line 18
  2. def OAI.UniformKServer.StarOutputData.mass line 20
  3. def OAI.UniformKServer.StarOutputData.parentFlex line 21
  4. def OAI.UniformKServer.StarOutputData.childFlex line 23
  5. def OAI.UniformKServer.StarOutputData.error line 26
  6. def OAI.UniformKServer.StarOutputData.alphaData line 31
  7. def OAI.UniformKServer.StarOutputData.sideData line 35
  8. def OAI.UniformKServer.StarOutputData.alpha line 38
  9. def OAI.UniformKServer.StarOutputData.side line 40
  10. theorem OAI.UniformKServer.StarOutputData.mass_nonneg line 43
  11. theorem OAI.UniformKServer.StarOutputData.parent_nonneg line 46
  12. theorem OAI.UniformKServer.StarOutputData.parent_expand line 51
  13. theorem OAI.UniformKServer.StarOutputData.child_expand line 57
  14. theorem OAI.UniformKServer.StarOutputData.flex_inactive line 62
  15. theorem OAI.UniformKServer.StarOutputData.regular_flex line 69
  16. theorem OAI.UniformKServer.StarOutputData.cap_child line 79
  17. theorem OAI.UniformKServer.StarOutputData.error_nonneg line 85
  18. theorem OAI.UniformKServer.StarOutputData.error_sum line 92
  19. theorem OAI.UniformKServer.StarOutputData.error_rule_one line 109
  20. theorem OAI.UniformKServer.StarOutputData.required_holes line 128
  21. theorem OAI.UniformKServer.StarOutputData.alpha_nonneg line 136
  22. theorem OAI.UniformKServer.StarOutputData.alpha_proportion line 139
  23. theorem OAI.UniformKServer.StarOutputData.alpha_supported line 144
  24. theorem OAI.UniformKServer.StarOutputData.alpha_sum line 157
  25. theorem OAI.UniformKServer.StarOutputData.side_input_active line 170
  26. theorem OAI.UniformKServer.StarOutputData.core_inactive line 180
  27. theorem OAI.UniformKServer.StarOutputData.side_nonneg line 185
  28. theorem OAI.UniformKServer.StarOutputData.side_supported line 188