OAI/Combinatorics/UniformKServer/HiddenFlow.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The true-metric posterior flow is derived from literal labeled one-server trajectories. Observing further partition randomness may refine the filtration; no filtering identity on a later selected event is assumed.

  1. structure OAI.UniformKServer.HiddenFlow.Data line 19
  2. def OAI.UniformKServer.HiddenFlow.atom line 31
  3. def OAI.UniformKServer.HiddenFlow.counts line 33
  4. def OAI.UniformKServer.HiddenFlow.moverAtom line 36
  5. def OAI.UniformKServer.HiddenFlow.current line 39
  6. def OAI.UniformKServer.HiddenFlow.filtered line 42
  7. def OAI.UniformKServer.HiddenFlow.mover line 45
  8. theorem OAI.UniformKServer.HiddenFlow.atom_nonneg line 49
  9. theorem OAI.UniformKServer.HiddenFlow.atom_total line 51
  10. theorem OAI.UniformKServer.HiddenFlow.counts_nonneg line 54
  11. theorem OAI.UniformKServer.HiddenFlow.counts_total line 57
  12. theorem OAI.UniformKServer.HiddenFlow.mover_le_count line 63
  13. theorem OAI.UniformKServer.HiddenFlow.counts_update line 68
  14. theorem OAI.UniformKServer.HiddenFlow.normalization line 79
  15. theorem OAI.UniformKServer.HiddenFlow.posterior_local line 86
  16. theorem OAI.UniformKServer.HiddenFlow.posterior_total line 99
  17. theorem OAI.UniformKServer.HiddenFlow.posterior_mono line 107
  18. def OAI.UniformKServer.HiddenFlow.flow line 112
  19. theorem OAI.UniformKServer.HiddenFlow.expected_mover_cost line 149