OAI/Combinatorics/UniformKServer/PrefixMovement.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Height-free deterministic conversion of coordinate-key disagreements into weighted subtree-count variation on the literal full prefix universe.

  1. def OAI.UniformKServer.PrefixMovement.diff line 17
  2. theorem OAI.UniformKServer.PrefixMovement.diff_nonneg line 19
  3. theorem OAI.UniformKServer.PrefixMovement.prefix_ext line 22
  4. theorem OAI.UniformKServer.PrefixMovement.prefix_disagreement line 30
  5. def OAI.UniformKServer.PrefixMovement.mark line 46
  6. theorem OAI.UniformKServer.PrefixMovement.mark_nonneg line 49
  7. theorem OAI.UniformKServer.PrefixMovement.mark_iff line 52
  8. theorem OAI.UniformKServer.PrefixMovement.level_mark line 60
  9. theorem OAI.UniformKServer.PrefixMovement.level_variation line 75
  10. theorem OAI.UniformKServer.PrefixMovement.depth_sum line 106
  11. theorem OAI.UniformKServer.PrefixMovement.path_variation line 118
  12. theorem OAI.UniformKServer.PrefixMovement.tail_bound line 141
  13. theorem OAI.UniformKServer.PrefixMovement.tail_depths line 156
  14. def OAI.UniformKServer.PrefixMovement.edgeWeight line 181
  15. theorem OAI.UniformKServer.PrefixMovement.spatial_variation line 183