OAI/Combinatorics/KServer/Tiers.lean

GitHub source file

158 declarations, 0 contain sorry, 0 declared as axioms

The actual adapted chronological tier process and its all-step compact pilot payment. No conditional drift or unconstructed roster is postulated.

  1. lemma OAI.KServer.Pilot.residual_bounds line 17
  2. lemma OAI.KServer.Pilot.profile_difference line 26
  3. lemma OAI.KServer.Pilot.residual_half line 44

    Source documentation

    A narrow residual has deficit at most one half unless a nearby pilot site has weight at least one half. Separation, not a new assumption about sparsity, proves that at most one positive bump contributes.

    lemma residual_half {T : Template} {r γ : ℝ} {z : Y → ℝ} {x p : Y}
    (hr : 0<r) (hγ : γ<T.σ) (hz : Feasible T r z)
    (hn : ∀ s,dist s x<3*T.σ*r → z s<1/2)
    (hp : dist x p≤γ*r) : 1/2 ≤ 1-∑ s,z s*b T (dist s p/r) := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.b

  4. lemma OAI.KServer.Pilot.surcharge_error line 76

    Source documentation

    Correcting each coefficient by epsilon uses the pilot capacity once, not the number of sites.

    lemma surcharge_error {T : Template} {r ε : ℝ} {z d : Y → ℝ} (hz : Feasible T r z)
    (hε : 0≤ε) (hd : ∀ s,-ε≤d s) (p : Y) :
    -ε ≤ ∑ s,z s*d s*a T (dist s p/r) := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.a

  5. lemma OAI.KServer.Pilot.surcharge_gain line 92
  6. lemma OAI.KServer.Pilot.indicator_sum line 111
  7. lemma OAI.KServer.Pilot.profile_error line 116

    Source documentation

    Common signed error estimate, including exact support.

    lemma profile_error {T : Template} {r ε : ℝ} {z g₀ g₁ : Y → ℝ}
    (hz : Feasible T r z) (hε : 0≤ε) (hd : ∀ i,-ε≤g₀ i-g₁ i) (W : Finset Y)
    (hres : ∀ p,p∉W → 0≤g₀ p-g₁ p)
    (hsur : ∀ p,p∉W → ∀ i,0≤z i*(g₀ i-g₁ i)*a T (dist i p/r)) (p : Y) :
    -257*ε*(if p∈W then (1:ℝ) else 0) ≤ integrand T r g₀ z p-integrand T r g₁ z p := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.a, OAI.KServer.Pilot.integrand

  8. lemma OAI.KServer.Pilot.profile_residual_gain line 134

    Source documentation

    A residual gain is added to the common signed error, pointwise.

    lemma profile_residual_gain {T : Template} {r ε : ℝ} {z g₀ g₁ : Y → ℝ}
    (hz : Feasible T r z) (hε : 0≤ε) (hd : ∀ i,-ε≤g₀ i-g₁ i) (W A : Finset Y)
    (hres : ∀ p,p∉W → 0≤g₀ p-g₁ p)
    (hsur : ∀ p,p∉W → ∀ i,0≤z i*(g₀ i-g₁ i)*a T (dist i p/r))
    (hgain : ∀ p∈A,g₀ p-g₁ p=1 ∧ 1/2≤1-∑ s,z s*b T (dist s p/r)) (p : Y) :
    (1/2:ℝ)*(if p∈A then 1 else 0)-257*ε*(if p∈W then (1:ℝ) else 0) ≤
      integrand T r g₀ z p-integrand T r g₁ z p := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.a, OAI.KServer.Pilot.b, OAI.KServer.Pilot.integrand

  9. lemma OAI.KServer.Pilot.profile_surcharge_gain line 155

    Source documentation

    A known near site creates a surcharge gain, pointwise.

    lemma profile_surcharge_gain {T : Template} {r ε : ℝ} {z g₀ g₁ : Y → ℝ}
    (hz : Feasible T r z) (hε : 0≤ε) (hd : ∀ i,-ε≤g₀ i-g₁ i) (W A : Finset Y)
    (hres : ∀ p,p∉W → 0≤g₀ p-g₁ p)
    (hsur : ∀ p,p∉W → ∀ i,0≤z i*(g₀ i-g₁ i)*a T (dist i p/r))
    (s : Y) (hs : g₀ s-g₁ s=1) (hzs : 1/2≤z s)
    (ha : ∀ p∈A,a T (dist s p/r)=1) (p : Y) :
    128*(if p∈A then (1:ℝ) else 0)-257*ε*(if p∈W then (1:ℝ) else 0) ≤
      integrand T r g₀ z p-integrand T r g₁ z p := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.a, OAI.KServer.Pilot.integrand

  10. lemma OAI.KServer.Pilot.potential_profile_gain line 183

    Source documentation

    Integrating a pointwise pilot edit estimate and testing the literal old minimizer proves a minimum decrease; no decrease assumption is needed.

    lemma potential_profile_gain {T : Template} {r c e : ℝ} {μ g₀ g₁ : Y → ℝ}
    (hr : 0≤r) (hμ : ∀ p,0≤μ p) (A W : Finset Y)
    (hpoint : ∀ p,c*(if p∈A then (1:ℝ) else 0)-e*(if p∈W then (1:ℝ) else 0) ≤
      integrand T r g₀ (minimizer T r μ g₀) p-
        integrand T r g₁ (minimizer T r μ g₀) p) :
    r*(c*mass μ A-e*mass μ W) ≤ potential T r μ g₀-potential T r μ g₁ := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.integrand, OAI.KServer.Pilot.minimizer, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.potential

  11. lemma OAI.KServer.Pilot.coefficient_lower line 207

    Source documentation

    A coefficient lower bound using the actual bump supports on any two finite regions. Used for the heavy annular version of the tier edit.

    lemma coefficient_lower {T : Template} {r : ℝ} {μ g : Y → ℝ} (s : Y)
    (hμ : ∀ p,0≤μ p) (hg : ∀ p,g p∈Set.Icc 0 1) (A B : Finset Y)
    (ha : ∀ p∈A,a T (dist s p/r)=1)
    (hb : ∀ p,b T (dist s p/r)≠0 → p∈B) :
    256*mass μ A-2*mass μ B ≤ coefficient T r μ g s := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.a, OAI.KServer.Pilot.b, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.coefficient

  12. lemma OAI.KServer.Pilot.a_eq_one line 241
  13. lemma OAI.KServer.Pilot.tier_increasing_site_zero line 260
  14. lemma OAI.KServer.Pilot.tier_near_bump line 296
  15. lemma OAI.KServer.Pilot.tier_outer_surcharge_nonneg line 318
  16. def OAI.KServer.Pilot.tierRegion line 337

    Source documentation

    The finite region whose mass is charged by one real tier insertion.

    def tierRegion (T : Template) (r γ δ : ℝ) (μ : Y → ℝ) (x : Y) : Finset Y :=
…

    Mentions: OAI.KServer.Pilot.Template

  17. lemma OAI.KServer.Pilot.tierRegion_subset line 342
  18. lemma OAI.KServer.Pilot.tier_error_support line 356

    Source documentation

    Geometry discharges the signed-error support with the annular heavy region, rather than paying the possibly large inner heavy mass.

    lemma tier_error_support {T : Template} {r γ δ : ℝ} {μ g₀ g₁ z : Y → ℝ} {x : Y}
    (hr : 0<r) (hσ : T.σ≤1/1000) (hγ : γ≤1/100) (hδ : δ≤1)
    (hμ : ∀ p,0≤μ p) (hg : ∀ p,g₀ p∈Set.Icc 0 1)
    (hz : Feasible T r z) (hmin : IsMinOn (objective T r μ g₀) {w | Feasible T r w} z)
    (hM : 0 < mass μ (ball x (γ*r)))
    (hdrop : ∀ p,dist x p≤r/8 → g₀ p-g₁ p=1)
    (hsupp : ∀ p,g₀ p-g₁ p<0 → dist x p≤21*r) :
    (∀ p,p∉tierRegion T r γ δ μ x → 0≤g₀ p-g₁ p) ∧
    (∀ p,p∉tierRegion T r γ δ μ x → ∀ i,0≤z i*(g₀ i-g₁ i)*a T (dist i p/r)) := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.Feasible, OAI.KServer.Pilot.objective, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.Pilot.tierRegion, OAI.KServer.Pilot.a

  19. theorem OAI.KServer.Pilot.tier_pilot_drop line 410

    Source documentation

    Tier-pilot drop, including the heavy annular refinement. The profile hypotheses describe the actual short-roster update; no pilot drop, site existence, or coefficient-vanishing statement is assumed.

    theorem tier_pilot_drop {T : Template} {r γH γL δ h ε : ℝ} {μ g₀ g₁ : Y → ℝ} {x : Y}
    (hr : 0<r) (hσ : T.σ≤1/1000) (hR : 51201≤T.R)
    (hγH : γH≤1/100) (hσH : 10*T.σ<γH) (hγL : γL<T.σ)
    (hδ0 : 0≤δ) (hδ : δ≤1/256) (hh : 0≤h) (hε : 0≤ε)
    (hμ : ∀ p,0≤μ p) (hg : ∀ p,g₀ p∈Set.Icc 0 1)
    (hM : 0 < mass μ (ball x (γL*r)))
    (hqual : mass μ (ball x (100*T.R*r))≤Real.exp h*mass μ (ball x (γL*r)))
    (hd : ∀ p,-ε≤g₀ p-g₁ p)
    (hdrop : ∀ p,dist x p≤r/8 → g₀ p-g₁ p=1)
    (hsupp : ∀ p,g₀ p-g₁ p<0 → dist x p≤21*r) :
    r*mass μ (tierRegion T r γH δ μ x)*(128*δ*Real.exp (-h)-257*ε) ≤
      potential T r μ g₀-potential T r μ g₁ := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.Pilot.tierRegion, OAI.KServer.Pilot.potential

  20. def OAI.KServer.TierProcess.request line 513
  21. lemma OAI.KServer.TierProcess.request_fin line 517
  22. lemma OAI.KServer.TierProcess.request_adapted line 521
  23. def OAI.KServer.TierProcess.qualifies line 530
  24. def OAI.KServer.TierProcess.roster line 535
  25. lemma OAI.KServer.TierProcess.roster_succ line 540
  26. lemma OAI.KServer.TierProcess.roster_before line 547
  27. lemma OAI.KServer.TierProcess.roster_adapted line 553
  28. def OAI.KServer.TierProcess.profile line 583
  29. lemma OAI.KServer.TierProcess.profile_adapted line 588
  30. def OAI.KServer.TierProcess.charge line 598

    Source documentation

    The genuine insertion mass W of the manuscript, zero on noninsertions.

    def charge (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (T : Template) (r γH γL δ h : ℝ) (K : ℕ) (t : Fin H) (σ : Fin H → Y) : ℝ :=
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution

  31. lemma OAI.KServer.TierProcess.charge_nonneg line 604
  32. lemma OAI.KServer.TierProcess.charge_le_drop line 612
  33. theorem OAI.KServer.TierProcess.insertion_budget line 650

    Source documentation

    All-step tier insertion budget against the actual finite-law optimum. Its endpoint depends only on finite scales and k, not on the input law.

    theorem insertion_budget (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    {T : Template} {r₀ τ γH γL δH δL h : ℝ} {K : ℕ} (n p : ℕ)
    (hr : 0<r₀) (hτ : 2≤τ) (hK : 2≤K) (hσ : T.σ≤1/1000) (hR : 51201≤T.R)
    (hγH : γH≤1/100) (hσH : 10*T.σ<γH) (hγL0 : 0<γL)
    (hγL : γL≤ min (T.σ/64) (1/(1+T.L)))
    (hδH0 : 0≤δH) (hδH : δH≤1/256) (hδL0 : 0<δL) (hδL : δL≤1/4112)
    (hh : 0≤h) (hL : 8≤T.L) (hpow : 100*T.R≤γL*(2:ℝ)^p) :
    (∑ t : Fin H,avg law.val (fun σ=>∑ j∈range n,
      charge s law T (radius r₀ τ j) γH γL δH h K t σ*(128*δH*Real.exp (-h)-257*(49/Real.sqrt K)))) ≤
      driftConstant T γL δL p*(1+Real.log ((k:ℝ)+1))*
        ∑ σ,law.val σ*optimalCost s (List.ofFn σ)+
          ∑ j∈range n,2*radius r₀ τ j*(k:ℝ) := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.TierProcess.charge

  34. def OAI.KServer.TierProcess.tierTemplate line 699
  35. def OAI.KServer.TierProcess.heavyGamma line 708
  36. def OAI.KServer.TierProcess.heavyDelta line 709
  37. def OAI.KServer.TierProcess.tierGamma line 710
  38. def OAI.KServer.TierProcess.tierDelta line 711
  39. def OAI.KServer.TierProcess.tierK line 713
  40. lemma OAI.KServer.TierProcess.tierK_exp line 715
  41. lemma OAI.KServer.TierProcess.exp_one_ge_two line 717
  42. lemma OAI.KServer.TierProcess.tierK_ge_two line 721
  43. lemma OAI.KServer.TierProcess.tierK_sqrt line 725
  44. lemma OAI.KServer.TierProcess.exp_large line 732
  45. lemma OAI.KServer.TierProcess.tier_error_absorb line 737
  46. lemma OAI.KServer.TierProcess.tier_reciprocal_absorb line 754
  47. lemma OAI.KServer.TierProcess.tier_weight_sum line 769
  48. lemma OAI.KServer.TierProcess.weighted_insertion_drop line 787
  49. def OAI.KServer.TierProcess.tierDrift line 812

    Source documentation

    The constant is shared by all tiers; the overlap integer is fixed.

    def tierDrift : ℝ := driftConstant tierTemplate tierGamma tierDelta 60

    Mentions: OAI.KServer.TierProcess.tierTemplate, OAI.KServer.TierProcess.tierGamma, OAI.KServer.TierProcess.tierDelta

  50. theorem OAI.KServer.TierProcess.weighted_insertion_budget line 816

    Source documentation

    A single real tier's actual insertion charges. The multiplier exp(-h) will be summable, so the estimate does not pay the number of tiers.

    theorem weighted_insertion_budget (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    {r₀ τ h : ℝ} (n : ℕ) (hr : 0<r₀) (hτ : 2≤τ) (hh : 1≤h) :
    (∑ t : Fin H,avg law.val (fun σ=>∑ j∈range n,
      charge s law tierTemplate (radius r₀ τ j) heavyGamma tierGamma heavyDelta h (tierK h) t σ/(tierK h:ℝ))) ≤
      Real.exp (-h)*(tierDrift*(1+Real.log ((k:ℝ)+1))*
        ∑ σ,law.val σ*optimalCost s (List.ofFn σ)+ ∑ j∈range n,2*radius r₀ τ j*(k:ℝ)) := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.TierProcess.charge, OAI.KServer.TierProcess.tierTemplate, OAI.KServer.TierProcess.heavyGamma, OAI.KServer.TierProcess.tierGamma, OAI.KServer.TierProcess.heavyDelta, OAI.KServer.TierProcess.tierK, OAI.KServer.TierProcess.tierDrift

  51. lemma OAI.KServer.Chronological.schedule_mem line 862
  52. lemma OAI.KServer.Chronological.schedule_mono line 886
  53. lemma OAI.KServer.Chronological.age_mono_history line 892
  54. def OAI.KServer.Chronological.reserved line 899
  55. lemma OAI.KServer.Chronological.reserved_card line 902
  56. lemma OAI.KServer.Chronological.reserved_before line 907
  57. lemma OAI.KServer.Chronological.reserved_backward line 912
  58. def OAI.KServer.Chronological.conflicts line 923

    Source documentation

    Reservation is deterministic and persists even after a random retirement. The previous prefix is also excluded, giving the stipulated one-step cooldown.

    def conflicts (center : ℕ → Y) (r : ℝ) (K : ℕ) (qualifies : ℕ → Prop) (t : ℕ) : Finset ℕ :=
…
  59. def OAI.KServer.Chronological.pool line 926
  60. lemma OAI.KServer.Chronological.pool_pos line 929
  61. lemma OAI.KServer.Chronological.conflicts_card line 931
  62. lemma OAI.KServer.Chronological.conflicts_before line 940
  63. def OAI.KServer.Chronological.label line 947

    Source documentation

    Actual permanent record labels in the finite source pool.

    def label (center : ℕ → Y) {r : ℝ} (hr : 0≤r) (K : ℕ) (qualifies : ℕ → Prop) (i : ℕ) : Fin (pool Y K) :=
…

    Mentions: OAI.KServer.Chronological.pool

  64. theorem OAI.KServer.Chronological.label_injective_consecutive line 952

    Source documentation

    Common labels on consecutive maps identify the same chronological record. In particular ordinary roster anchors do not move when a label persists.

    theorem label_injective_consecutive (center : ℕ → Y) {r : ℝ} (hr : 0≤r) (K : ℕ)
    (qualifies : ℕ → Prop) (t : ℕ) :
    Set.InjOn (label center hr K qualifies)
      (↑(reserved center r K qualifies t ∪ reserved center r K qualifies (t+1)) : Set ℕ) := by
…

    Mentions: OAI.KServer.Chronological.label, OAI.KServer.Chronological.reserved

  65. def OAI.KServer.TierKeys.key line 983
  66. lemma OAI.KServer.TierKeys.key_some line 989
  67. lemma OAI.KServer.TierKeys.first_reserved line 999
  68. lemma OAI.KServer.TierKeys.common_same_record line 1006
  69. def OAI.KServer.TierKeys.anchor line 1019
  70. lemma OAI.KServer.TierKeys.anchor_record line 1024
  71. lemma OAI.KServer.TierKeys.anchor_distance line 1034
  72. lemma OAI.KServer.TierKeys.anchors_persist line 1042
  73. lemma OAI.KServer.TierKeys.guaranteed_coverage line 1055
  74. theorem OAI.KServer.TierKeys.spatial_bound line 1068
  75. def OAI.KServer.PriorityKeys.covered line 1094
  76. def OAI.KServer.PriorityKeys.selected line 1097
  77. lemma OAI.KServer.PriorityKeys.selected_some_of_mem line 1103
  78. lemma OAI.KServer.PriorityKeys.selected_none_iff line 1113
  79. lemma OAI.KServer.PriorityKeys.selected_some line 1129
  80. lemma OAI.KServer.PriorityKeys.selected_eq_of_prefix line 1145
  81. def OAI.KServer.PriorityKeys.key line 1171
  82. lemma OAI.KServer.PriorityKeys.key_ne_prefix line 1176
  83. theorem OAI.KServer.PriorityKeys.probability_prefix_bound line 1186
  84. def OAI.KServer.PriorityKeys.anchor line 1208
  85. lemma OAI.KServer.PriorityKeys.anchor_distance line 1212
  86. lemma OAI.KServer.PriorityKeys.cell_diameter line 1221
  87. lemma OAI.KServer.TierDyadic.exists_power line 1243
  88. def OAI.KServer.TierDyadic.index line 1248
  89. lemma OAI.KServer.TierDyadic.index_covers line 1250
  90. lemma OAI.KServer.TierDyadic.index_le line 1252
  91. lemma OAI.KServer.TierDyadic.index_zero line 1254
  92. lemma OAI.KServer.TierDyadic.preceding_lt line 1258
  93. lemma OAI.KServer.TierDyadic.tier_sum line 1261
  94. theorem OAI.KServer.TierDyadic.qualified_sum line 1266
  95. lemma OAI.KServer.TierDyadic.index_mono line 1278
  96. lemma OAI.KServer.TierDyadic.tierK_upper line 1282
  97. lemma OAI.KServer.TierDyadic.exp_three_ge_five line 1288
  98. theorem OAI.KServer.TierDyadic.radius_coefficient line 1295
  99. lemma OAI.KServer.LevelCoverage.ball_mass_mono line 1324
  100. lemma OAI.KServer.LevelCoverage.ball_mass_total line 1330
  101. lemma OAI.KServer.LevelCoverage.ball_mass_served line 1334
  102. def OAI.KServer.LevelCoverage.logratio line 1341
  103. lemma OAI.KServer.LevelCoverage.logratio_bounds line 1346
  104. lemma OAI.KServer.LevelCoverage.qualifies_of_log line 1363
  105. def OAI.KServer.LevelCoverage.firstTier line 1376
  106. lemma OAI.KServer.LevelCoverage.firstTier_le line 1379
  107. lemma OAI.KServer.LevelCoverage.firstTier_qualifies line 1384
  108. lemma OAI.KServer.LevelCoverage.heavy_near_center line 1389
  109. lemma OAI.KServer.LevelCoverage.heavy_agrees line 1401
  110. abbrev OAI.KServer.LevelKeys.Tier line 1433
  111. abbrev OAI.KServer.LevelKeys.Structure line 1434
  112. def OAI.KServer.LevelKeys.height line 1436
  113. lemma OAI.KServer.LevelKeys.height_ge line 1438
  114. abbrev OAI.KServer.LevelKeys.Alphabet line 1440
  115. abbrev OAI.KServer.LevelKeys.Key line 1444
  116. abbrev OAI.KServer.LevelKeys.Tape line 1446
  117. def OAI.KServer.LevelKeys.tierQualifies line 1451
  118. def OAI.KServer.LevelKeys.keys line 1455
  119. def OAI.KServer.LevelKeys.map line 1462
  120. lemma OAI.KServer.LevelKeys.covered_request line 1466
  121. def OAI.KServer.LevelKeys.heavyAnchor line 1481
  122. lemma OAI.KServer.LevelKeys.heavy_anchor_distance line 1487
  123. theorem OAI.KServer.LevelKeys.nonemptyY line 1508
  124. def OAI.KServer.LevelKeys.anchors line 1510
  125. lemma OAI.KServer.LevelKeys.structure_anchor_distance line 1517
  126. def OAI.KServer.LevelKeys.anchor line 1530
  127. lemma OAI.KServer.LevelKeys.anchor_distance line 1534
  128. lemma OAI.KServer.LevelKeys.cell_diameter line 1539
  129. lemma OAI.KServer.FiniteTape.marginal line 1558
  130. lemma OAI.KServer.FiniteTape.event_marginal line 1573
  131. def OAI.KServer.FiniteTape.pair line 1580
  132. lemma OAI.KServer.FiniteTape.pair_nonneg line 1583
  133. lemma OAI.KServer.FiniteTape.pair_sum line 1586
  134. lemma OAI.KServer.FiniteTape.pair_left line 1589
  135. lemma OAI.KServer.FiniteTape.pair_right line 1598
  136. lemma OAI.KServer.FiniteTape.pair_event_left line 1602
  137. lemma OAI.KServer.FiniteTape.pair_event_right line 1606
  138. abbrev OAI.KServer.LevelLaw.RequestLaw line 1622
  139. def OAI.KServer.LevelLaw.heavyWeight line 1626
  140. def OAI.KServer.LevelLaw.lifetimeWeight line 1629
  141. def OAI.KServer.LevelLaw.radiusWeight line 1632
  142. def OAI.KServer.LevelLaw.tierWeight line 1635
  143. def OAI.KServer.LevelLaw.weight line 1639
  144. lemma OAI.KServer.LevelLaw.heavy_sum line 1642
  145. lemma OAI.KServer.LevelLaw.lifetime_sum line 1645
  146. lemma OAI.KServer.LevelLaw.log_pos line 1649
  147. lemma OAI.KServer.LevelLaw.radius_sum line 1655
  148. lemma OAI.KServer.LevelLaw.tier_sum line 1660
  149. lemma OAI.KServer.LevelLaw.weight_sum line 1663
  150. lemma OAI.KServer.LevelLaw.heavy_nonneg line 1667
  151. lemma OAI.KServer.LevelLaw.lifetime_nonneg line 1670
  152. lemma OAI.KServer.LevelLaw.radius_nonneg line 1675
  153. lemma OAI.KServer.LevelLaw.tier_nonneg line 1679
  154. lemma OAI.KServer.LevelLaw.weight_nonneg line 1682
  155. lemma OAI.KServer.LevelLaw.heavy_event line 1685
  156. lemma OAI.KServer.LevelLaw.tier_event line 1691
  157. lemma OAI.KServer.LevelLaw.heavy_spatial line 1700
  158. lemma OAI.KServer.LevelLaw.tier_spatial line 1719