OAI/Combinatorics/UniformKServer/PublicRounding.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Causal rounded distributions are realized without exposing the hidden trajectory. Only an observed request prefix selects the conditional rows.

  1. structure OAI.UniformKServer.TreeRounding.PublicInput line 17
  2. def OAI.UniformKServer.TreeRounding.PublicInput.pick line 29
  3. theorem OAI.UniformKServer.TreeRounding.PublicInput.pick_trace line 33
  4. theorem OAI.UniformKServer.TreeRounding.PublicInput.pick_related line 40
  5. def OAI.UniformKServer.TreeRounding.PublicInput.input line 43
  6. theorem OAI.UniformKServer.TreeRounding.PublicInput.kernel_trace line 48
  7. theorem OAI.UniformKServer.TreeRounding.PublicInput.location_trace line 55
  8. def OAI.UniformKServer.TreeRounding.PublicInput.initial line 61
  9. theorem OAI.UniformKServer.TreeRounding.PublicInput.initial_first line 64
  10. theorem OAI.UniformKServer.TreeRounding.PublicInput.process_marginal line 71
  11. def OAI.UniformKServer.TreeRounding.PublicInput.potential line 79
  12. def OAI.UniformKServer.TreeRounding.PublicInput.charge line 82
  13. def OAI.UniformKServer.TreeRounding.PublicInput.transport line 85
  14. theorem OAI.UniformKServer.TreeRounding.PublicInput.step line 88
  15. theorem OAI.UniformKServer.TreeRounding.PublicInput.potential_nonneg line 111
  16. theorem OAI.UniformKServer.TreeRounding.PublicInput.potential_initial line 117
  17. theorem OAI.UniformKServer.TreeRounding.PublicInput.total_charge line 122