OAI/Combinatorics/KServer/PartitionBudget.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

Literal conditional averaging for the hidden optimum's stationary members. Only conditioning on the true request prefix is used; tape averages may be performed first without conditioning on a surviving random roster.

  1. lemma OAI.KServer.HiddenAverages.counting_integral line 18
  2. lemma OAI.KServer.HiddenAverages.expected_counting_test line 27
  3. lemma OAI.KServer.HiddenAverages.expected_before_test line 43
  4. lemma OAI.KServer.HiddenAverages.expected_mover_test line 59
  5. def OAI.KServer.HiddenAverages.stationary line 76
  6. lemma OAI.KServer.HiddenAverages.stationary_nonneg line 79
  7. lemma OAI.KServer.HiddenAverages.stationary_le line 83
  8. lemma OAI.KServer.HiddenAverages.stationary_identity line 89
  9. lemma OAI.KServer.HiddenAverages.expected_stationary_test line 97
  10. lemma OAI.KServer.TierTemporal.mean_add line 128
  11. lemma OAI.KServer.TierTemporal.mean_sub line 131
  12. lemma OAI.KServer.TierTemporal.mean_sum line 134
  13. lemma OAI.KServer.TierTemporal.mover_inner line 139
  14. lemma OAI.KServer.TierTemporal.mover_mean_inner line 151
  15. lemma OAI.KServer.TierTemporal.dyadic_exp_sum line 163
  16. lemma OAI.KServer.TierTemporal.dyadic_reciprocal_sum line 181
  17. def OAI.KServer.TierTemporal.potential line 190
  18. def OAI.KServer.TierTemporal.editCost line 194
  19. lemma OAI.KServer.TierTemporal.potential_bounds line 198
  20. lemma OAI.KServer.TierTemporal.potential_step line 206
  21. def OAI.KServer.TierAverages.region line 247
  22. def OAI.KServer.TierAverages.test line 250
  23. lemma OAI.KServer.TierAverages.test_nonneg line 253
  24. lemma OAI.KServer.TierAverages.inserted_adapted line 256
  25. lemma OAI.KServer.TierAverages.test_adapted line 265
  26. lemma OAI.KServer.TierAverages.retirement_region line 271
  27. lemma OAI.KServer.TierAverages.stationary_test_bound line 286
  28. lemma OAI.KServer.TierAverages.test_mass line 304
  29. lemma OAI.KServer.TierAverages.expected_stationary_bound line 316
  30. lemma OAI.KServer.TierAverages.nonheavy_mass line 335
  31. def OAI.KServer.TierBudget.paidMass line 364
  32. lemma OAI.KServer.TierBudget.paidMass_nonneg line 367
  33. lemma OAI.KServer.TierBudget.paidMass_charge line 374
  34. lemma OAI.KServer.TierBudget.mover_bound line 381
  35. lemma OAI.KServer.TierBudget.average_step line 410
  36. lemma OAI.KServer.TierGlobal.telescope_budget line 468
  37. lemma OAI.KServer.TierGlobal.potential_mean_bounds line 481
  38. lemma OAI.KServer.TierGlobal.tier_budget line 494
  39. lemma OAI.KServer.TierGlobal.actual_move_cost line 509
  40. lemma OAI.KServer.TierGlobal.far_scales line 514
  41. lemma OAI.KServer.TierScaleBudget.avg_finset_sum line 543
  42. lemma OAI.KServer.TierScaleBudget.factor_sum line 549
  43. lemma OAI.KServer.TierScaleBudget.insertion_budget line 552
  44. lemma OAI.KServer.TierScaleBudget.insertion_all line 578
  45. lemma OAI.KServer.TierScaleBudget.far_all line 605
  46. lemma OAI.KServer.TierScaleBudget.noinsert_all line 651
  47. def OAI.KServer.HeavyEdit.ramp line 717

    Source documentation

    The heavy profile is zero up to radius 9 and one from radius 10.

    def ramp (u : ℝ) : ℝ := min 1 (max 0 (u-9))
  48. lemma OAI.KServer.HeavyEdit.ramp_bounds line 718
  49. lemma OAI.KServer.HeavyEdit.ramp_zero line 720
  50. lemma OAI.KServer.HeavyEdit.ramp_one line 722
  51. lemma OAI.KServer.HeavyEdit.ramp_lipschitz line 724
  52. def OAI.KServer.HeavyEdit.profile line 734

    Source documentation

    Finite minimum with a default value 1, also for the empty center set.

    def profile (r : ℝ) (C : Finset Y) (y : Y) : ℝ :=
…
  53. lemma OAI.KServer.HeavyEdit.profile_nonneg line 737
  54. lemma OAI.KServer.HeavyEdit.profile_le_one line 745
  55. lemma OAI.KServer.HeavyEdit.profile_bounds line 747
  56. lemma OAI.KServer.HeavyEdit.profile_le line 749
  57. lemma OAI.KServer.HeavyEdit.le_profile line 752
  58. lemma OAI.KServer.HeavyEdit.profile_empty line 760
  59. lemma OAI.KServer.HeavyEdit.profile_eq_one line 762
  60. lemma OAI.KServer.HeavyEdit.profile_eq_zero line 768
  61. lemma OAI.KServer.HeavyEdit.profile_gt_witness line 773
  62. lemma OAI.KServer.HeavyEdit.profile_lipschitz line 780
  63. lemma OAI.KServer.HeavyEdit.profile_far line 800
  64. def OAI.KServer.HeavyEdit.oldKey line 822
  65. def OAI.KServer.HeavyEdit.newKey line 825
  66. lemma OAI.KServer.HeavyEdit.replace_separated line 831
  67. lemma OAI.KServer.HeavyEdit.new_radius line 844
  68. lemma OAI.KServer.HeavyEdit.inner_reuses line 853
  69. lemma OAI.KServer.HeavyEdit.keys_far line 869
  70. lemma OAI.KServer.HeavyEdit.inner_paid line 896
  71. theorem OAI.KServer.HeavyEdit.stationary line 916

    Source documentation

    Source heavy edit charge table for a stationary member.

    theorem stationary {r R:ℝ} (hr:0<r) {C D:Finset Y} {x p:Y} {rad:Y→ℝ}
    {lab prev:Y→Pool Y} (hC:(C:Set Y).Pairwise (fun a b=>100*r<dist a b))
    (hrad:∀ a∈C,rad a∈Set.Icc (16*r) (20*r)) (hR:R∈Set.Icc (16*r) (20*r)) :
    (if oldKey C rad lab p≠newKey C D rad lab prev r x R p then (1:ℝ) else 0) +
      profile r (replace r C x) p-profile r C p≤
        if 3*r<dist x p ∧ dist x p≤120*r then 2 else 0 := by
…

    Mentions: OAI.KServer.HeavyEdit.oldKey, OAI.KServer.HeavyEdit.newKey, OAI.KServer.HeavyEdit.profile

  72. theorem OAI.KServer.HeavyEdit.mover line 936

    Source documentation

    Source heavy edit charge table for the designated mover.

    theorem mover {r R:ℝ} (hr:0<r) {C D:Finset Y} {x p:Y} {rad:Y→ℝ}
    {lab prev:Y→Pool Y} (hC:(C:Set Y).Pairwise (fun a b=>100*r<dist a b))
    (hrad:∀ a∈C,rad a∈Set.Icc (16*r) (20*r)) (hR:R∈Set.Icc (16*r) (20*r)) :
    (if oldKey C rad lab p≠newKey C D rad lab prev r x R p then (1:ℝ) else 0) +
      profile r (replace r C x) x-profile r C p≤ if 3*r<dist x p then 1 else 0 := by
…

    Mentions: OAI.KServer.HeavyEdit.oldKey, OAI.KServer.HeavyEdit.newKey, OAI.KServer.HeavyEdit.profile

  73. def OAI.KServer.HeavyTemporal.active line 968
  74. def OAI.KServer.HeavyTemporal.charge line 972
  75. def OAI.KServer.HeavyTemporal.profile line 977
  76. lemma OAI.KServer.HeavyTemporal.ite_indicator line 981
  77. lemma OAI.KServer.HeavyTemporal.charge_le line 984
  78. lemma OAI.KServer.HeavyTemporal.active_keys line 991
  79. lemma OAI.KServer.HeavyTemporal.inactive_keys line 1004
  80. lemma OAI.KServer.HeavyTemporal.inactive_charge line 1011
  81. lemma OAI.KServer.HeavyTemporal.active_profile line 1019
  82. lemma OAI.KServer.HeavyTemporal.inactive_profile line 1026
  83. lemma OAI.KServer.HeavyTemporal.stationary line 1032
  84. def OAI.KServer.HeavyTemporal.heavy line 1061
  85. lemma OAI.KServer.HeavyTemporal.mover line 1065
  86. lemma OAI.KServer.KeysAdapted.history_mono line 1123
  87. lemma OAI.KServer.KeysAdapted.run_adapted line 1133
  88. lemma OAI.KServer.KeysAdapted.heavy_key_adapted line 1151
  89. lemma OAI.KServer.KeysAdapted.reserved_adapted line 1158
  90. lemma OAI.KServer.KeysAdapted.conflicts_adapted line 1173
  91. lemma OAI.KServer.KeysAdapted.stage_congr line 1183
  92. lemma OAI.KServer.KeysAdapted.label_adapted line 1192
  93. lemma OAI.KServer.KeysAdapted.first_congr line 1204
  94. lemma OAI.KServer.KeysAdapted.tier_key_adapted line 1217
  95. lemma OAI.KServer.KeysAdapted.keys_adapted line 1239
  96. lemma OAI.KServer.KeysAdapted.map_adapted line 1250
  97. def OAI.KServer.HeavyBudget.test line 1274
  98. lemma OAI.KServer.HeavyBudget.test_nonneg line 1277
  99. lemma OAI.KServer.HeavyBudget.test_adapted line 1280
  100. lemma OAI.KServer.HeavyBudget.test_mass line 1290
  101. lemma OAI.KServer.HeavyBudget.stationary_bound line 1300
  102. def OAI.KServer.HeavyBudget.potential line 1319
  103. def OAI.KServer.HeavyBudget.editCost line 1322
  104. lemma OAI.KServer.HeavyBudget.potential_bounds line 1326
  105. lemma OAI.KServer.HeavyBudget.potential_step line 1332
  106. lemma OAI.KServer.HeavyBudget.step_bound line 1357
  107. lemma OAI.KServer.HeavyBudget.average_step line 1376
  108. lemma OAI.KServer.HeavyBudget.mean_bounds line 1389
  109. lemma OAI.KServer.HeavyBudget.heavy_budget line 1397