OAI/Combinatorics/UniformKServer/BalancedStar.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

One conditional update of the complete finite tree rounding process. The arbitrary supported old law includes every correlation produced by earlier ancestor roundings; no conditional independence is imposed.

  1. def OAI.UniformKServer.BalancedStar.Balanced line 11
  2. structure OAI.UniformKServer.BalancedStar.Input line 13
  3. def OAI.UniformKServer.BalancedStar.realized line 28
  4. def OAI.UniformKServer.BalancedStar.T line 31
  5. def OAI.UniformKServer.BalancedStar.imbalance line 32
  6. def OAI.UniformKServer.BalancedStar.jointCost line 35
  7. def OAI.UniformKServer.BalancedStar.Valid line 38
  8. def OAI.UniformKServer.BalancedStar.clip line 43
  9. theorem OAI.UniformKServer.BalancedStar.balanced_bounds line 45
  10. theorem OAI.UniformKServer.BalancedStar.bounds_balanced line 49
  11. theorem OAI.UniformKServer.BalancedStar.clip_balanced line 54
  12. theorem OAI.UniformKServer.BalancedStar.clip_nonexpansive line 60
  13. def OAI.UniformKServer.BalancedStar.lowerSum line 109
  14. def OAI.UniformKServer.BalancedStar.upperSet line 110
  15. def OAI.UniformKServer.BalancedStar.clippedSet line 112
  16. def OAI.UniformKServer.BalancedStar.slots line 114
  17. def OAI.UniformKServer.BalancedStar.fraction line 115
  18. theorem OAI.UniformKServer.BalancedStar.fraction_bounds line 118
  19. theorem OAI.UniformKServer.BalancedStar.sum_realized line 124
  20. theorem OAI.UniformKServer.BalancedStar.clippedSet_subset line 129
  21. theorem OAI.UniformKServer.BalancedStar.represented_clip line 135
  22. theorem OAI.UniformKServer.BalancedStar.subset_balanced line 142
  23. theorem OAI.UniformKServer.BalancedStar.ceil_sum line 154
  24. theorem OAI.UniformKServer.BalancedStar.lowerSum_le_floor line 166
  25. theorem OAI.UniformKServer.BalancedStar.ceil_le_sum line 172
  26. theorem OAI.UniformKServer.BalancedStar.slots_spec line 177
  27. theorem OAI.UniformKServer.BalancedStar.slots_two line 190
  28. theorem OAI.UniformKServer.BalancedStar.realized_distance line 199
  29. theorem OAI.UniformKServer.BalancedStar.choose_subset_close line 208
  30. theorem OAI.UniformKServer.BalancedStar.preliminary_exists line 222
  31. def OAI.UniformKServer.BalancedStar.preliminary line 238
  32. theorem OAI.UniformKServer.BalancedStar.preliminary_spec line 242
  33. theorem OAI.UniformKServer.BalancedStar.abs_sum_sub_le line 250
  34. theorem OAI.UniformKServer.BalancedStar.weighted_abs_le line 256
  35. def OAI.UniformKServer.BalancedStar.preliminaryCost line 262
  36. def OAI.UniformKServer.BalancedStar.clipCost line 265
  37. theorem OAI.UniformKServer.BalancedStar.clipCost_le line 269
  38. theorem OAI.UniformKServer.BalancedStar.preliminaryCost_le line 277
  39. theorem OAI.UniformKServer.BalancedStar.initial_marginal line 307
  40. theorem OAI.UniformKServer.BalancedStar.initial_realized_mean line 319
  41. theorem OAI.UniformKServer.BalancedStar.discrepancy_le line 327
  42. theorem OAI.UniformKServer.BalancedStar.slots_mean line 350
  43. theorem OAI.UniformKServer.BalancedStar.marginal_realized_mean line 360
  44. theorem OAI.UniformKServer.BalancedStar.support_subset line 369
  45. theorem OAI.UniformKServer.BalancedStar.cost_transfer line 390
  46. theorem OAI.UniformKServer.BalancedStar.rounding_star line 412