OAI/Combinatorics/UniformKServer/FiniteFlowSpace.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A literal finite coordinate model of all horizon-H causal flows. Compactness comes from their probability bounds, not from assuming a minimax input.

  1. abbrev OAI.UniformKServer.FiniteFlowSpace.Word line 16
  2. def OAI.UniformKServer.FiniteFlowSpace.letters line 17
  3. def OAI.UniformKServer.FiniteFlowSpace.code line 18
  4. theorem OAI.UniformKServer.FiniteFlowSpace.letters_code line 20
  5. theorem OAI.UniformKServer.FiniteFlowSpace.letters_length line 24
  6. theorem OAI.UniformKServer.FiniteFlowSpace.letters_bound line 26
  7. abbrev OAI.UniformKServer.FiniteFlowSpace.Index line 31
  8. abbrev OAI.UniformKServer.FiniteFlowSpace.Space line 32
  9. def OAI.UniformKServer.FiniteFlowSpace.decode line 34
  10. def OAI.UniformKServer.FiniteFlowSpace.encode line 38
  11. theorem OAI.UniformKServer.FiniteFlowSpace.decode_encode_mass line 42
  12. theorem OAI.UniformKServer.FiniteFlowSpace.decode_encode_flow line 46
  13. theorem OAI.UniformKServer.FiniteFlowSpace.decode_encode_valid line 53
  14. theorem OAI.UniformKServer.FiniteFlowSpace.encode_bounds line 67
  15. theorem OAI.UniformKServer.FiniteFlowSpace.decode_combine line 87
  16. theorem OAI.UniformKServer.FiniteFlowSpace.mass_continuous line 96
  17. theorem OAI.UniformKServer.FiniteFlowSpace.flow_continuous line 103