OAI/Combinatorics/UniformKServer/AlphaFiniteInput.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Actual posterior/core inputs in a finite reveal law. Conditions describe the held, measurable data, not a movement conclusion. Empty and null-fiber cases still use the zero conventions of the conditional kernel.

  1. structure OAI.UniformKServer.AlphaFiniteInput.Data line 19
  2. def OAI.UniformKServer.AlphaFiniteInput.post line 33
  3. def OAI.UniformKServer.AlphaFiniteInput.activeFlag line 36
  4. def OAI.UniformKServer.AlphaFiniteInput.input line 38
  5. def OAI.UniformKServer.AlphaFiniteInput.star line 41
  6. def OAI.UniformKServer.AlphaFiniteInput.oldMask line 45
  7. def OAI.UniformKServer.AlphaFiniteInput.changes line 48
  8. def OAI.UniformKServer.AlphaFiniteInput.alpha line 51
  9. def OAI.UniformKServer.AlphaFiniteInput.prepared line 55
  10. theorem OAI.UniformKServer.AlphaFiniteInput.post_range line 59
  11. theorem OAI.UniformKServer.AlphaFiniteInput.flag_supported line 64
  12. theorem OAI.UniformKServer.AlphaFiniteInput.input_nonneg line 69
  13. theorem OAI.UniformKServer.AlphaFiniteInput.input_supported line 72
  14. theorem OAI.UniformKServer.AlphaFiniteInput.star_supported_old line 77
  15. theorem OAI.UniformKServer.AlphaFiniteInput.star_supported_new line 82
  16. theorem OAI.UniformKServer.AlphaFiniteInput.valid_input line 87
  17. theorem OAI.UniformKServer.AlphaFiniteInput.errors line 99
  18. theorem OAI.UniformKServer.AlphaFiniteInput.alpha_state line 107
  19. theorem OAI.UniformKServer.AlphaFiniteInput.step line 110
  20. theorem OAI.UniformKServer.AlphaFiniteInput.refining line 115
  21. theorem OAI.UniformKServer.AlphaFiniteInput.input_measurable line 121
  22. theorem OAI.UniformKServer.AlphaFiniteInput.star_measurable line 130
  23. theorem OAI.UniformKServer.AlphaFiniteInput.alpha_measurable line 139