OAI/Combinatorics/KServer/RosterEdits.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

One-structure edits of the actual priority map. These lemmas keep earlier structures fixed; in particular a covered heavy key suppresses all tier edits.

  1. lemma OAI.KServer.ActualRoster.final_survival line 13
  2. lemma OAI.KServer.ActualRoster.death_marginal line 23

    Source documentation

    Unconditional marginal death bound. The extra tail is never interpreted as a conditional compulsory hazard.

    lemma death_marginal {K a b : ℕ} (hK : 2 ≤ K) (hab : a ≤ b) (hba : b ≤ a+1) :
    (∑ d : Lifetime K, if alive K a d ∧ ¬alive K b d then lifetimeLaw K d else 0) ≤
      (1/(K:ℝ))*actualPresence K a+
        if a<K^2 then survive (1/(K:ℝ)) (K^2-K) else 0 := by
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.ActualRoster.alive, OAI.KServer.ActualRoster.lifetimeLaw

  3. theorem OAI.KServer.ActualRoster.first_retirement_bound line 51

    Source documentation

    A literal finite lifetime-tape first-coverer estimate. The S hypothesis is only a deterministic candidate count, and is discharged by chronological ages below.

    theorem first_retirement_bound {H K : ℕ} (hK : 2 ≤ K)
    (a b : Fin H → ℕ) (inc : ∀ i, a i≤b i ∧ b i≤a i+1)
    (cover : Fin H → Prop) (S : Finset (Fin H))
    (hS : ∀ i, cover i → a i<K^2 → i∈S) (hcard : S.card ≤ K^2) :
    PartitionProbabilities.probability (fun _ : Fin H=>lifetimeLaw K)
      (firstSeparation (fun i d=>cover i ∧ alive K (a i) d)
        (fun i d=>cover i ∧ alive K (a i) d ∧ ¬alive K (b i) d)) ≤ 49/(K:ℝ) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.probability, OAI.KServer.ActualRoster.lifetimeLaw, OAI.KServer.ActualRoster.alive

  4. theorem OAI.KServer.ActualRoster.chronological_retirement_bound line 107

    Source documentation

    The unconditional first-coverer retirement estimate for an actual fixed chronological roster and arbitrary fixed radii. Increment bounds follow from one chronological insertion, not from the realized random presences.

    theorem chronological_retirement_bound (center : ℕ → Y) (I : Finset ℕ)
    {r : ℝ} (hr : 0 < r) (hK : 2≤K) (rad : Fin H → Outcome Y r) (p : Y)
    (b : Fin H → ℕ) (hinc : ∀ i : Fin H, age center I (20*r) i≤b i ∧ b i≤age center I (20*r) i+1) :
    PartitionProbabilities.probability (fun _ : Fin H=>lifetimeLaw K)
      (firstSeparation
        (fun i d=>(i:ℕ)∈I ∧ dist (center i) p≤radius r (rad i) ∧ alive K (age center I (20*r) i) d)
        (fun i d=>(i:ℕ)∈I ∧ dist (center i) p≤radius r (rad i) ∧
          alive K (age center I (20*r) i) d ∧ ¬alive K (b i) d)) ≤49/(K:ℝ) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.probability, OAI.KServer.ActualRoster.lifetimeLaw, OAI.KServer.ActualRoster.alive

  5. lemma OAI.KServer.ActualRoster.age_insert_bounds line 141
  6. lemma OAI.KServer.ActualRoster.old_covered_of_new line 151
  7. lemma OAI.KServer.ActualRoster.new_covered_of_persists line 158
  8. lemma OAI.KServer.ActualRoster.first_persists line 164

    Source documentation

    Chronological appending cannot supersede a surviving first coverer.

    lemma first_persists (center : ℕ → Y) (I : Finset ℕ) (r : ℝ) (t : ℕ)
    (hI : ∀ i∈I, i<t) (life : Fin H → Lifetime K) (rad : Fin H → Outcome Y r)
    (p : Y) (i : Fin H) (hfirst : first center I r life rad p=some i)
    (hp : present center (insert t I) r life i) :
    first center (insert t I) r life rad p=some i := by
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.ActualRoster.first, OAI.KServer.ActualRoster.present

  9. def OAI.KServer.ActualRoster.retired line 177
  10. lemma OAI.KServer.ActualRoster.retired_iff line 181
  11. theorem OAI.KServer.ActualRoster.insertion_retirement line 201

    Source documentation

    An actual insertion's exceptional first-coverer retirement row, under the literal lifetime tape and with every radius held fixed.

    theorem insertion_retirement (center : ℕ → Y) (I : Finset ℕ) {r : ℝ} (hr : 0<r)
    (hK : 2≤K) (t : ℕ) (rad : Fin H → Outcome Y r) (p : Y) :
    PartitionProbabilities.probability (fun _ : Fin H=>lifetimeLaw K)
      (fun life=>retired center I (insert t I) r life rad p) ≤49/(K:ℝ) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.probability, OAI.KServer.ActualRoster.lifetimeLaw, OAI.KServer.ActualRoster.retired

  12. lemma OAI.KServer.ActualRoster.retired_near line 216

    Source documentation

    The retirement error is supported inside the 22r neighbourhood.

    lemma retired_near (center : ℕ → Y) (I : Finset ℕ) {r : ℝ} (hr : 0<r) (t : ℕ)
    (hI : ∀ i∈I, i<t) (life : Fin H → Lifetime K) (rad : Fin H → Outcome Y r)
    (p : Y) (h : retired center I (insert t I) r life rad p) : dist p (center t)≤22*r := by
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.ActualRoster.retired

  13. lemma OAI.KServer.ActualRoster.inserted_covers line 236

    Source documentation

    A fresh appended ball covers every point within r, pathwise even on zero-probability lifetime tape outcomes.

    lemma inserted_covers (center : ℕ → Y) (I : Finset ℕ) {r : ℝ} (hr : 0<r) (hK : 0<K)
    (t : Fin H) (hI : ∀ i∈I, i<t) (life : Fin H → Lifetime K)
    (rad : Fin H → Outcome Y r) (p : Y) (hp : dist (center t) p≤r) :
    covered center (insert (t:ℕ) I) r life rad p t := by
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.ActualRoster.covered

  14. def OAI.KServer.ActualRoster.indicator line 244
  15. lemma OAI.KServer.ActualRoster.indicator_nonneg line 246
  16. lemma OAI.KServer.ActualRoster.indicator_le_one line 247
  17. theorem OAI.KServer.ActualRoster.stationary_table line 250

    Source documentation

    Literal stationary noncoverage table.

    theorem stationary_table (center : ℕ → Y) (I : Finset ℕ) (r : ℝ) (t : ℕ)
    (hI : ∀ i∈I, i<t) (life : Fin H → Lifetime K) (rad : Fin H → Outcome Y r) (p : Y) :
    indicator (first center I r life rad p≠first center (insert t I) r life rad p)+
      indicator (first center (insert t I) r life rad p=none)-
      indicator (first center I r life rad p=none) ≤
        2*indicator (retired center I (insert t I) r life rad p) := by
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.ActualRoster.indicator, OAI.KServer.ActualRoster.first, OAI.KServer.ActualRoster.retired

  18. theorem OAI.KServer.ActualRoster.mover_table line 274

    Source documentation

    Mover row, using final guaranteed coverage instead of a stationary final position. Its retirement coefficient is one instead of two.

    theorem mover_table (center : ℕ → Y) (I : Finset ℕ) {r : ℝ} (hr : 0<r) (hK : 0<K)
    (t : Fin H) (hI : ∀ i∈I, i<t) (life : Fin H → Lifetime K)
    (rad : Fin H → Outcome Y r) (p : Y) :
    indicator (first center I r life rad p≠first center (insert (t:ℕ) I) r life rad p)+
      indicator (first center (insert (t:ℕ) I) r life rad (center t)=none)-
      indicator (first center I r life rad p=none) ≤
        indicator (retired center I (insert (t:ℕ) I) r life rad p) := by
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.ActualRoster.indicator, OAI.KServer.ActualRoster.first, OAI.KServer.ActualRoster.retired

  19. lemma OAI.KServer.PriorityKeys.selected_congr_point line 313
  20. lemma OAI.KServer.PriorityKeys.key_congr_point line 321
  21. lemma OAI.KServer.PriorityKeys.key_ne_single line 325
  22. lemma OAI.KServer.PriorityKeys.single_indicator line 335
  23. def OAI.KServer.PriorityKeys.stageBefore line 343

    Source documentation

    Before and after the elementary edit at structure j.

    def stageBefore (q₀ q₁:(i:I)→Y→Option (A i)) (j:I) : (i:I)→Y→Option (A i) :=
…
  24. def OAI.KServer.PriorityKeys.stageAfter line 346
  25. lemma OAI.KServer.PriorityKeys.stage_at line 350
  26. lemma OAI.KServer.PriorityKeys.stage_outside line 355
  27. lemma OAI.KServer.PriorityKeys.stage_charge line 359
  28. lemma OAI.KServer.PriorityKeys.selected_bot line 368
  29. lemma OAI.KServer.PriorityKeys.key_bot line 378
  30. lemma OAI.KServer.PriorityKeys.bot_shadow line 381
  31. lemma OAI.KServer.PriorityKeys.stage_shadow line 384
  32. lemma OAI.KServer.TierEdits.indicator_mono line 405
  33. lemma OAI.KServer.TierEdits.map_charge line 410
  34. lemma OAI.KServer.TierEdits.map_none line 414
  35. lemma OAI.KServer.TierEdits.key_none line 420
  36. lemma OAI.KServer.TierEdits.key_change line 426
  37. lemma OAI.KServer.TierEdits.stationary line 433
  38. lemma OAI.KServer.TierEdits.mover line 448
  39. lemma OAI.KServer.TierEdits.no_insert line 463
  40. lemma OAI.KServer.TierEdits.covered_inner line 470
  41. def OAI.KServer.LevelTierEdits.charge line 500
  42. def OAI.KServer.LevelTierEdits.uncovered line 507
  43. def OAI.KServer.LevelTierEdits.inserted line 511
  44. def OAI.KServer.LevelTierEdits.retirement line 516
  45. lemma OAI.KServer.LevelTierEdits.charge_nonneg line 522
  46. lemma OAI.KServer.LevelTierEdits.charge_le line 526
  47. lemma OAI.KServer.LevelTierEdits.stationary line 532
  48. lemma OAI.KServer.LevelTierEdits.mover line 543
  49. lemma OAI.KServer.LevelTierEdits.no_insert_charge line 556
  50. lemma OAI.KServer.LevelTierEdits.no_insert_stationary line 566
  51. lemma OAI.KServer.LevelTierEdits.covered_qualified line 578
  52. lemma OAI.KServer.LevelTierEdits.no_insert_mover line 590
  53. lemma OAI.KServer.LevelTierEdits.heavy_inner_covers line 612
  54. lemma OAI.KServer.LevelTierEdits.heavy_inner_charge line 629
  55. lemma OAI.KServer.LevelTierEdits.heavy_inner_stationary line 639
  56. lemma OAI.KServer.LevelRetirement.tier_lifetime_bound line 673
  57. lemma OAI.KServer.LevelRetirement.retirement_bound line 703
  58. lemma OAI.KServer.LevelRetirement.retirement_far line 720
  59. def OAI.KServer.LevelRetirement.mean line 735
  60. lemma OAI.KServer.LevelRetirement.mean_mono line 738
  61. lemma OAI.KServer.LevelRetirement.mean_const line 742
  62. lemma OAI.KServer.LevelRetirement.mean_indicator line 747
  63. lemma OAI.KServer.LevelRetirement.mean_scale line 757
  64. lemma OAI.KServer.LevelRetirement.stationary_mean line 765
  65. lemma OAI.KServer.LevelRetirement.mover_mean line 790
  66. lemma OAI.KServer.LevelScale.log_ball_bounds line 814
  67. lemma OAI.KServer.LevelScale.mass_positive line 822
  68. lemma OAI.KServer.LevelScale.logratio_sum line 828
  69. lemma OAI.KServer.LevelScale.nonheavy_count line 853
  70. lemma OAI.KServer.LevelScale.tier_shift line 878
  71. lemma OAI.KServer.LevelScale.heavy_shift line 883
  72. lemma OAI.KServer.LevelScale.actual_logratio_sum line 890
  73. lemma OAI.KServer.LevelScale.actual_nonheavy_count line 897
  74. lemma OAI.KServer.LevelSpatial.fin_prefix_sum line 922
  75. lemma OAI.KServer.LevelSpatial.structure_prefix_sum line 933
  76. def OAI.KServer.LevelSpatial.separation line 956
  77. lemma OAI.KServer.LevelSpatial.separation_nonneg line 960
  78. lemma OAI.KServer.LevelSpatial.separation_le_one line 964
  79. lemma OAI.KServer.LevelSpatial.separation_self line 970
  80. lemma OAI.KServer.LevelSpatial.prefix_bound line 974
  81. lemma OAI.KServer.LevelSpatial.request_bound line 1020
  82. lemma OAI.KServer.LevelSpatial.map_eq_of_heavy line 1050
  83. lemma OAI.KServer.LevelSpatial.heavy_zero line 1064
  84. lemma OAI.KServer.LevelSpatial.spatial_sum line 1075

    Source documentation

    The complete-level estimate (final-map-separation), with an explicit absolute factor and no number-of-scales or largest-tier multiplier.

    lemma spatial_sum (s:Configuration k Y) (law:RequestLaw Y H)
    (σ:Fin H→Y) (hσ:0 < law.val σ) (t:Fin H) (y:Y)
    {r₀ τ:ℝ} (hr:0 < r₀) (hτ:2 ≤ τ) (n:ℕ) :
    (∑ j∈range n, Pilot.radius r₀ τ j *
      separation s law (Pilot.radius_pos hr (by linarith) j).le σ (t.val+1) (σ t) y) ≤
      (8+1050*(60/Real.log (1+heavyDelta)+60)*Real.log k)*dist (σ t) y := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.Pilot.radius, OAI.KServer.LevelSpatial.separation, OAI.KServer.Pilot.radius_pos

  85. lemma OAI.KServer.LevelNoInsert.filtered_powers line 1130
  86. lemma OAI.KServer.LevelNoInsert.tier_count line 1147
  87. lemma OAI.KServer.LevelNoInsert.unqualified_height_sum line 1160
  88. def OAI.KServer.LevelNoInsert.error line 1180

    Source documentation

    Positive error is zero on insertion steps here; those steps are separately charged to the actual retirement and pilot budgets.

    def error (s:Configuration k Y) (law:RequestLaw Y H) {r:ℝ} (hr:0 ≤ r)
    (σ:Fin H→Y) (t:Fin H) (i:Tier k) (p:Y) : ℝ :=
…

    Mentions: OAI.KServer.Configuration

  89. lemma OAI.KServer.LevelNoInsert.error_le_one line 1186
  90. lemma OAI.KServer.LevelNoInsert.error_spatial line 1197
  91. lemma OAI.KServer.LevelNoInsert.level_error line 1227
  92. lemma OAI.KServer.LevelNoInsert.scales_error line 1248