OAI/Combinatorics/KServer/AllocationSchedule.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

Binding the literal filtered-rank size schedule to the live child domain. In particular no core or positive lower-envelope rank is silently discarded when the coarse active state turns off.

  1. def OAI.KServer.AllocationSchedule.activeSet line 17

    Source documentation

    Active domain and literal held epoch mass, rather than a bound supplied to an allocation interface.

    def activeSet (x : J → ℝ) : Finset J := univ.filter fun i => 0<x i
  2. def OAI.KServer.AllocationSchedule.mass line 19
  3. def OAI.KServer.AllocationSchedule.sideHeld line 21
  4. def OAI.KServer.AllocationSchedule.sideRatio line 24
  5. def OAI.KServer.AllocationSchedule.weight line 27
  6. lemma OAI.KServer.AllocationSchedule.mem_activeSet line 32
  7. lemma OAI.KServer.AllocationSchedule.sum_activeSet line 35
  8. lemma OAI.KServer.AllocationSchedule.mass_nonneg line 42
  9. lemma OAI.KServer.AllocationSchedule.mass_accuracy line 46
  10. lemma OAI.KServer.AllocationSchedule.dominant_mass_pos line 51
  11. lemma OAI.KServer.AllocationSchedule.marked_active line 58
  12. lemma OAI.KServer.AllocationSchedule.side_eq_erase line 65
  13. lemma OAI.KServer.AllocationSchedule.side_held_nonneg line 76
  14. lemma OAI.KServer.AllocationSchedule.side_held_accuracy line 81
  15. lemma OAI.KServer.AllocationSchedule.side_ratio_nonneg line 88
  16. lemma OAI.KServer.AllocationSchedule.side_ratio_upper line 92
  17. lemma OAI.KServer.AllocationSchedule.side_zero_iff line 107
  18. lemma OAI.KServer.AllocationSchedule.marked_zero_singleton line 124
  19. lemma OAI.KServer.AllocationSchedule.weight_side_lower line 144

    Source documentation

    On the true active sides, held logarithmic weights satisfy the special marked profile condition used in the decrement-gap argument.

    lemma weight_side_lower {δ : ℝ} (hδ : 0<δ) (hδu : δ ≤ 1/1000)
    (x : ℕ → J → ℝ) (key : ℕ → K) (hx : ∀ t i, 0 ≤ x t i)
    (t : ℕ) {o i : J} (ho : dominant (run x key t)=some o)
    (hi : i∈activeSet (x t)) (hio : i≠o) (hu : 0<sideRatio δ x key t) :
    (1/2:ℝ)*(1+Real.log (1/sideRatio δ x key t)) ≤ weight δ x key t i := by
…

    Mentions: OAI.KServer.AllocationSchedule.activeSet, OAI.KServer.AllocationSchedule.sideRatio, OAI.KServer.AllocationSchedule.weight

  20. lemma OAI.KServer.AllocationSchedule.mass_upper line 174
  21. lemma OAI.KServer.AllocationSchedule.regular_weight line 185
  22. lemma OAI.KServer.AllocationSchedule.marked_weight line 189
  23. lemma OAI.KServer.AllocationSchedule.weight_regular_one line 193
  24. lemma OAI.KServer.AllocationSchedule.weight_nonneg line 198
  25. lemma OAI.KServer.AllocationSchedule.weight_upper line 205
  26. lemma OAI.KServer.AllocationSchedule.regular_exp_sum line 221
  27. lemma OAI.KServer.AllocationSchedule.side_exp_sum line 232
  28. def OAI.KServer.AllocationSchedule.epoch line 253

    Source documentation

    Epoch labels record the actual wholesale test.

    def epoch (x : ℕ → J → ℝ) (key : ℕ → K) : ℕ → ℕ
  | 0 => 0
  | t+1 => if CoarseSide.epochReset x key t then epoch x key t+1 else epoch x key t

omit [DecidableEq J] in

    Mentions: OAI.KServer.CoarseSide.epochReset

  29. lemma OAI.KServer.AllocationSchedule.epoch_same_iff line 258
  30. def OAI.KServer.AllocationSchedule.zeroData line 268

    Source documentation

    Empty and genuinely side-free marked domains have the source's zero potential. The dummy regular kernel is never evaluated by that potential.

    def zeroData (A : Finset J) (flags : J → R → Bool) : SimplexFamilies.Data J R :=
…

    Mentions: OAI.KServer.SimplexFamilies.Data

  31. def OAI.KServer.AllocationSchedule.data line 271
  32. lemma OAI.KServer.AllocationSchedule.data_active line 289
  33. lemma OAI.KServer.AllocationSchedule.data_flags line 302
  34. def OAI.KServer.StarProfile.cutoff line 329
  35. lemma OAI.KServer.StarProfile.live_iff line 331
  36. lemma OAI.KServer.StarProfile.too_small_inactive line 346
  37. lemma OAI.KServer.StarProfile.inactive_rank_cutoff line 353
  38. lemma OAI.KServer.StarProfile.inactive_lower_zero line 364
  39. lemma OAI.KServer.StarProfile.inactive_flag_false line 370
  40. lemma OAI.KServer.StarProfile.vector_floor line 382
  41. lemma OAI.KServer.StarProfile.vector_total line 391
  42. lemma OAI.KServer.StarProfile.flags_supported line 400
  43. lemma OAI.KServer.StarProfile.vector_adapted line 407
  44. lemma OAI.KServer.StarProfile.parent_adapted line 415
  45. lemma OAI.KServer.ScheduledSimplex.singleton_feasible line 444
  46. lemma OAI.KServer.ScheduledSimplex.nonempty_mass line 464
  47. lemma OAI.KServer.ScheduledSimplex.update_feasible line 474
  48. lemma OAI.KServer.ActualParameters.log_bound line 560
  49. lemma OAI.KServer.ActualParameters.beta_bounds line 580
  50. lemma OAI.KServer.ActualParameters.gap line 594
  51. lemma OAI.KServer.ActualParameters.held_error line 641
  52. def OAI.KServer.ScheduleCausality.PrefixEq line 673
  53. lemma OAI.KServer.ScheduleCausality.PrefixEq.mono line 675
  54. lemma OAI.KServer.ScheduleCausality.run_prefix line 679
  55. lemma OAI.KServer.ScheduleCausality.mass_prefix line 689
  56. lemma OAI.KServer.ScheduleCausality.side_prefix line 694
  57. lemma OAI.KServer.ScheduleCausality.reset_prefix line 700
  58. lemma OAI.KServer.ScheduleCausality.sideHeld_prefix line 708
  59. lemma OAI.KServer.ScheduleCausality.ratio_prefix line 721
  60. lemma OAI.KServer.ScheduleCausality.weight_prefix line 725
  61. lemma OAI.KServer.ScheduleCausality.epoch_prefix line 732
  62. lemma OAI.KServer.ScheduleCausality.data_prefix line 741
  63. def OAI.KServer.StarSimplex.flags line 804
  64. def OAI.KServer.StarSimplex.input line 807
  65. def OAI.KServer.StarSimplex.proportion line 814
  66. lemma OAI.KServer.StarSimplex.proportion_mem line 818
  67. lemma OAI.KServer.StarSimplex.input_core line 824
  68. lemma OAI.KServer.StarSimplex.feasible line 832
  69. lemma OAI.KServer.StarSimplex.history_prefix line 888
  70. lemma OAI.KServer.StarSimplex.input_adapted line 898
  71. lemma OAI.KServer.StarSimplex.proportion_adapted line 920
  72. structure OAI.KServer.CausalSide.Input line 943
  73. def OAI.KServer.CausalSide.move line 948
  74. lemma OAI.KServer.CausalSide.zero_mem line 953
  75. lemma OAI.KServer.CausalSide.move_mem line 957
  76. def OAI.KServer.CausalSide.model line 964
  77. lemma OAI.KServer.CausalSide.model_value line 974
  78. lemma OAI.KServer.CausalSide.model_update line 977
  79. def OAI.KServer.CausalSide.transport line 980
  80. def OAI.KServer.CausalSide.run line 984
  81. lemma OAI.KServer.CausalSide.run_mem line 987
  82. lemma OAI.KServer.CausalSide.run_initial line 992
  83. lemma OAI.KServer.CausalSide.run_successor line 996
  84. lemma OAI.KServer.CausalSide.run_adapted line 1000
  85. lemma OAI.KServer.CausalSide.ordinary_successor line 1008
  86. lemma OAI.KServer.CausalSide.wholesale_successor line 1016
  87. lemma OAI.KServer.CausalSide.run_feasible line 1022
  88. lemma OAI.KServer.CausalSide.ordinary_payment line 1036