OAI/Combinatorics/KServer/PrefixAllocation.lean

GitHub source file

157 declarations, 0 contain sorry, 0 declared as axioms

Persistent heavy-slot size tracking on the actual finite observation experiment. Raw counts can change with both the hidden trajectory and the adapted partition. No martingale identity is postulated.

  1. def OAI.KServer.KeySizeTracking.tangent line 14
  2. def OAI.KServer.KeySizeTracking.entropy line 16
  3. lemma OAI.KServer.KeySizeTracking.tangent_credit line 18
  4. lemma OAI.KServer.KeySizeTracking.lower_ratio line 24
  5. lemma OAI.KServer.KeySizeTracking.upper_ratio line 46
  6. lemma OAI.KServer.KeySizeTracking.entropy_quadratic line 71
  7. lemma OAI.KServer.KeySizeTracking.relative_credit line 88
  8. def OAI.KServer.KeySizeTracking.avg line 111
  9. lemma OAI.KServer.KeySizeTracking.avg_add line 113
  10. lemma OAI.KServer.KeySizeTracking.avg_sub line 115
  11. lemma OAI.KServer.KeySizeTracking.avg_mul line 117
  12. lemma OAI.KServer.KeySizeTracking.avg_sum line 119
  13. lemma OAI.KServer.KeySizeTracking.avg_mono line 122
  14. lemma OAI.KServer.KeySizeTracking.avg_const line 124
  15. def OAI.KServer.KeySizeTracking.Adapted line 127
  16. lemma OAI.KServer.KeySizeTracking.fiber_weighted_zero line 129
  17. structure OAI.KServer.KeySizeTracking.FilteredSizes line 155

    Source documentation

    Old and new membership counts shifted by one, with literal finite-fiber conditioning. There is no policy-existence or budget assumption in this data.

    structure FilteredSizes (w : Ω → ℝ) (K : ℝ) where
…
  18. def OAI.KServer.KeySizeTracking.refresh line 166
  19. instance OAI.KServer.KeySizeTracking.(instance at line 167) line 167
  20. def OAI.KServer.KeySizeTracking.held line 169
  21. lemma OAI.KServer.KeySizeTracking.held_range line 174
  22. lemma OAI.KServer.KeySizeTracking.held_adapted line 181
  23. lemma OAI.KServer.KeySizeTracking.held_accurate line 193
  24. lemma OAI.KServer.KeySizeTracking.slope_bound line 204
  25. lemma OAI.KServer.KeySizeTracking.tangent_bound line 211
  26. def OAI.KServer.KeySizeTracking.refreshCost line 224
  27. lemma OAI.KServer.KeySizeTracking.refresh_cost_step line 228
  28. lemma OAI.KServer.KeySizeTracking.filtering_zero line 245
  29. lemma OAI.KServer.KeySizeTracking.expected_refresh_step line 254
  30. theorem OAI.KServer.KeySizeTracking.size_refresh_budget line 282

    Source documentation

    Size-refresh budget, before substituting the mapped-member transport bound. Crucially the constant is independent of the horizon.

    theorem size_refresh_budget {w : Ω → ℝ} {K : ℝ} (hw : ∀ ω, 0 ≤ w ω)
    (hw1 : ∑ ω, w ω=1) (R : FilteredSizes w K) (N : ℕ) :
    ∑ t ∈ range N, avg w (refreshCost R.s t) ≤
      144*(1+Real.log K)*(∑ t ∈ range N, avg w (fun ω => |R.s (t+1) ω-R.before (t+1) ω|))+
      288*K*(1+(1+Real.log K)) := by
…

    Mentions: OAI.KServer.KeySizeTracking.FilteredSizes, OAI.KServer.KeySizeTracking.avg, OAI.KServer.KeySizeTracking.refreshCost

  31. lemma OAI.KServer.PosteriorSizes.bounded line 319
  32. def OAI.KServer.PosteriorSizes.process line 327
  33. lemma OAI.KServer.PosteriorSizes.process_drift line 344
  34. lemma OAI.KServer.PosteriorSizes.refresh_budget line 353
  35. abbrev OAI.KServer.PrefixTree.Child line 381
  36. lemma OAI.KServer.PrefixTree.depth_zero_iff line 384
  37. lemma OAI.KServer.PrefixTree.parent_succ line 395
  38. lemma OAI.KServer.PrefixTree.child_depth line 401
  39. lemma OAI.KServer.PrefixTree.child_last_lt line 408
  40. def OAI.KServer.PrefixTree.extend line 412
  41. lemma OAI.KServer.PrefixTree.parent_extend line 416
  42. lemma OAI.KServer.PrefixTree.extend_ne_root line 422
  43. def OAI.KServer.PrefixTree.childEquiv line 429
  44. lemma OAI.KServer.PrefixTree.no_child line 450
  45. def OAI.KServer.PrefixTree.numberedChildEquiv line 456
  46. lemma OAI.KServer.PrefixTree.children_sum line 477
  47. lemma OAI.KServer.PrefixTree.children_sum_leaf line 489
  48. def OAI.KServer.PrefixTree.weight line 496
  49. lemma OAI.KServer.PrefixTree.weight_nonneg line 499
  50. lemma OAI.KServer.PrefixTree.parent_weight line 502
  51. def OAI.KServer.PrefixTree.travelTree line 527
  52. def OAI.KServer.PrefixTree.Q line 537
  53. def OAI.KServer.PrefixTree.region line 540
  54. lemma OAI.KServer.PrefixTree.Q_root line 544
  55. lemma OAI.KServer.PrefixTree.Q_nonneg line 549
  56. lemma OAI.KServer.PrefixTree.Q_children line 554
  57. lemma OAI.KServer.PrefixTree.Q_adapted line 566
  58. lemma OAI.KServer.PrefixTree.Q_mass line 571
  59. lemma OAI.KServer.PrefixTree.Q_witness line 579
  60. lemma OAI.KServer.PrefixTree.park_nonneg line 592
  61. lemma OAI.KServer.PrefixTree.park_le_Q line 598
  62. lemma OAI.KServer.Rounding.Tree.under_root line 607
  63. lemma OAI.KServer.Rounding.Tree.park_total line 615
  64. def OAI.KServer.PrefixTree.take line 632
  65. lemma OAI.KServer.PrefixTree.take_self line 636
  66. lemma OAI.KServer.PrefixTree.parent_depth line 641
  67. lemma OAI.KServer.PrefixTree.take_parent line 646
  68. lemma OAI.KServer.PrefixTree.hit_take line 655
  69. lemma OAI.KServer.PrefixTree.numbering_parent line 661
  70. lemma OAI.KServer.PrefixTree.numbering_eq_root line 665
  71. lemma OAI.KServer.PrefixTree.take_under line 670
  72. lemma OAI.KServer.PrefixTree.eq_of_common_hit line 714
  73. theorem OAI.KServer.PrefixTree.park_ball_capacity line 730
  74. lemma OAI.KServer.Rounding.Tree.park_difference line 789
  75. lemma OAI.KServer.Rounding.Tree.weighted_park_variation line 798
  76. lemma OAI.KServer.PrefixTree.sum_vertices line 826
  77. abbrev OAI.KServer.PrefixTree.Node line 847
  78. def OAI.KServer.PrefixTree.depth line 848
  79. def OAI.KServer.PrefixTree.lastKey line 849
  80. def OAI.KServer.PrefixTree.band line 852
  81. def OAI.KServer.PrefixTree.bandMass line 855
  82. lemma OAI.KServer.PrefixTree.band_nonneg line 857
  83. lemma OAI.KServer.PrefixTree.band_key line 860
  84. lemma OAI.KServer.PrefixTree.band_depth line 871
  85. lemma OAI.KServer.PrefixTree.band_disjoint line 874
  86. lemma OAI.KServer.PrefixTree.band_capacity line 891
  87. def OAI.KServer.KeyReferences.count line 924
  88. lemma OAI.KServer.KeyReferences.count_range line 927
  89. def OAI.KServer.KeyReferences.size line 934
  90. def OAI.KServer.KeyReferences.reference line 936
  91. lemma OAI.KServer.KeyReferences.mass_eq line 939
  92. def OAI.KServer.KeyReferences.process line 951
  93. lemma OAI.KServer.KeyReferences.size_range line 956
  94. lemma OAI.KServer.KeyReferences.reference_range line 960
  95. lemma OAI.KServer.KeyReferences.reference_pos line 965
  96. lemma OAI.KServer.KeyReferences.reference_comparison line 969
  97. lemma OAI.KServer.KeyReferences.reference_adapted line 975
  98. lemma OAI.KServer.KeyReferences.refresh_budget line 979
  99. def OAI.KServer.ParkedCoefficients.tail line 999
  100. lemma OAI.KServer.ParkedCoefficients.tail_zero line 1001
  101. lemma OAI.KServer.ParkedCoefficients.tail_step line 1002
  102. lemma OAI.KServer.ParkedCoefficients.logarithmic_increment line 1007
  103. lemma OAI.KServer.ParkedCoefficients.summation_by_parts line 1015
  104. theorem OAI.KServer.ParkedCoefficients.capacity_log_sum line 1029

    Source documentation

    Positive tail capacities control reciprocal-weighted mass logarithmically. The extra endpoint A n may be chosen as A (n-1), or any smaller positive value.

    theorem capacity_log_sum {b A : ℕ → ℝ} {n : ℕ} {C K : ℝ}
    (hC : 0 ≤ C) (hA : ∀ i ≤ n, A i ∈ Set.Icc 1 K)
    (hdec : ∀ i < n, A (i+1) ≤ A i)
    (hcap : ∀ i ≤ n, tail b n i ≤ C*A i) :
    ∑ i ∈ range n, b i/A i ≤ C*(1+Real.log K) := by
…

    Mentions: OAI.KServer.ParkedCoefficients.tail

  105. lemma OAI.KServer.ParkedCoefficients.tail_mono line 1056
  106. theorem OAI.KServer.ParkedCoefficients.park_coefficients line 1065

    Source documentation

    Exact abstract form of §08's geometric estimate. b is selected parked mass, d its held key size, B=1+mass(B(y,r)), A=1+mass(B(y,67r)). The assumptions here are pointwise capacity data, not stochastic or policy-existence interfaces.

    theorem park_coefficients {b d A B : ℕ → ℝ} {n : ℕ} {C K ρ R L : ℝ}
    (hC : 0 ≤ C) (hρ : 0 < ρ) (hR : 0 ≤ R)
    (hb : ∀ i < n, 0 ≤ b i) (hd : ∀ i < n, 0 < d i)
    (hA : ∀ i ≤ n, A i ∈ Set.Icc 1 K)
    (hB : ∀ i < n, B i ∈ Set.Icc 1 (A i))
    (hdec : ∀ i < n, A (i+1) ≤ A i)
    (hcap : ∀ i ≤ n, tail b n i ≤ C*A i)
    (hnorm : ∀ i < n, B i ≤ ρ*d i)
    (hbound : ∀ i < n, b i/d i ≤ R)
    (hlog : ∑ i ∈ range n, Real.log (A i/B i) ≤ L) :
    ∑ i ∈ range n, b i/d i ≤ R*L/Real.log 2+2*ρ*C*(1+Real.log K) := by
…

    Mentions: OAI.KServer.ParkedCoefficients.tail

  107. lemma OAI.KServer.ParkedCoefficients.scale_log_telescope line 1118

    Source documentation

    The exact fixed-offset telescope; scales shorter than the offset are included.

    lemma scale_log_telescope {A B : ℕ → ℝ} {n p : ℕ} {K : ℝ}
    (hK : 1 ≤ K) (hA : ∀ i < n, A i ∈ Set.Icc 1 K)
    (hB : ∀ i < n, B i ∈ Set.Icc 1 K)
    (hshift : ∀ i < n, p ≤ i → A i ≤ B (i-p)) :
    ∑ i ∈ range n, Real.log (A i/B i) ≤ (p:ℝ)*Real.log K := by
…
  108. theorem OAI.KServer.ParkedCoefficients.seven_scale_park_coefficients line 1170

    Source documentation

    Source offset p=7 gives an absolute height-independent bound. The capacity estimate is slightly relaxed from C*(A-1) to C*A, but the conclusion is the exact O(1+log K) needed and the stronger source capacity implies this premise.

    theorem seven_scale_park_coefficients {b d A B : ℕ → ℝ} {n : ℕ} {C K ρ R : ℝ}
    (hC : 0 ≤ C) (hρ : 0 < ρ) (hR : 0 ≤ R) (hK : 1 ≤ K)
    (hb : ∀ i < n, 0 ≤ b i) (hd : ∀ i < n, 0 < d i)
    (hA : ∀ i ≤ n, A i ∈ Set.Icc 1 K)
    (hB : ∀ i < n, B i ∈ Set.Icc 1 (A i))
    (hdec : ∀ i < n, A (i+1) ≤ A i)
    (hcap : ∀ i ≤ n, tail b n i ≤ C*(A i-1))
    (hnorm : ∀ i < n, B i ≤ ρ*d i)
    (hbound : ∀ i < n, b i/d i ≤ R)
    (hshift : ∀ i < n, 7 ≤ i → A i ≤ B (i-7)) :
    ∑ i ∈ range n, b i/d i ≤ (7*R/Real.log 2+2*ρ*C)*(1+Real.log K) := by
…

    Mentions: OAI.KServer.ParkedCoefficients.tail

  109. def OAI.KServer.ParkedCoefficients.ballMass line 1203

    Source documentation

    The manuscript's posterior measure of a closed metric ball, as a finite counting sum. We do not restrict to distinct hidden locations.

    def ballMass (μ : Y → ℝ) (y : Y) (r : ℝ) : ℝ :=
…
  110. lemma OAI.KServer.ParkedCoefficients.ballMass_nonneg line 1206
  111. lemma OAI.KServer.ParkedCoefficients.ballMass_total line 1212
  112. lemma OAI.KServer.ParkedCoefficients.ballMass_mono line 1218
  113. def OAI.KServer.ParkedCoefficients.radius line 1224
  114. lemma OAI.KServer.ParkedCoefficients.radius_pos line 1226
  115. lemma OAI.KServer.ParkedCoefficients.radius_antitone line 1229
  116. lemma OAI.KServer.ParkedCoefficients.radius_seven line 1235
  117. theorem OAI.KServer.ParkedCoefficients.metric_park_coefficients line 1254

    Source documentation

    The pointwise coefficient bound now for the actual metric ball masses and geometric scales of §07-08, not an assumed logarithmic telescope. b is zero on unselected levels. Cumulative subcapacity is supplied by Tree.geometric_park_capacity; held normalization and individual domination are the exact local invariants.

    theorem metric_park_coefficients {μ : Y → ℝ} (hμ : ∀ z, 0 ≤ μ z)
    (y : Y) {k C ρ R r₀ τ : ℝ} {n : ℕ} {b d : ℕ → ℝ}
    (hmass : ∑ z, μ z=k) (hC : 0 ≤ C) (hρ : 0 < ρ) (hR : 0 ≤ R)
    (hr : 0 ≤ r₀) (hτ : 2 ≤ τ)
    (hb : ∀ i < n, 0 ≤ b i) (hd : ∀ i < n, 0 < d i)
    (hcap : ∀ i ≤ n, tail b n i ≤ C*ballMass μ y (67*radius r₀ τ i))
    (hnorm : ∀ i < n, 1+ballMass μ y (radius r₀ τ i) ≤ ρ*d i)
    (hbound : ∀ i < n, b i/d i ≤ R) :
    ∑ i ∈ range n, b i/d i ≤ (7*R/Real.log 2+2*ρ*C)*(1+Real.log (k+1)) := by
…

    Mentions: OAI.KServer.ParkedCoefficients.tail, OAI.KServer.ParkedCoefficients.ballMass, OAI.KServer.ParkedCoefficients.radius

  118. def OAI.KServer.PrefixTree.selectedBand line 1309
  119. def OAI.KServer.PrefixTree.selectedMass line 1312
  120. lemma OAI.KServer.PrefixTree.selected_depth line 1315
  121. lemma OAI.KServer.PrefixTree.selected_disjoint line 1322
  122. lemma OAI.KServer.PrefixTree.selected_tail line 1331
  123. theorem OAI.KServer.PrefixTree.selected_capacity line 1342
  124. lemma OAI.KServer.PrefixTree.selected_mass_nonneg line 1418
  125. lemma OAI.KServer.PrefixTree.ballMass_eq line 1421
  126. def OAI.KServer.PrefixTree.selectedDenominator line 1425
  127. theorem OAI.KServer.PrefixTree.selected_coefficients line 1428
  128. abbrev OAI.KServer.JointAllocation.Ω line 1503
  129. abbrev OAI.KServer.JointAllocation.A line 1504
  130. def OAI.KServer.JointAllocation.quota line 1507
  131. def OAI.KServer.JointAllocation.park line 1511
  132. def OAI.KServer.JointAllocation.band line 1514
  133. def OAI.KServer.JointAllocation.size line 1517
  134. def OAI.KServer.JointAllocation.reference line 1520
  135. lemma OAI.KServer.JointAllocation.quota_nonneg line 1523
  136. lemma OAI.KServer.JointAllocation.park_nonneg line 1528
  137. lemma OAI.KServer.JointAllocation.band_nonneg line 1533
  138. lemma OAI.KServer.JointAllocation.band_capacity line 1536
  139. lemma OAI.KServer.JointAllocation.size_range line 1547
  140. lemma OAI.KServer.JointAllocation.reference_range line 1552
  141. lemma OAI.KServer.JointAllocation.reference_pos line 1556
  142. lemma OAI.KServer.JointAllocation.reference_comparison line 1559
  143. lemma OAI.KServer.JointAllocation.coefficient_bounds line 1565
  144. lemma OAI.KServer.JointAllocation.quota_adapted line 1574
  145. lemma OAI.KServer.JointAllocation.band_adapted line 1580
  146. lemma OAI.KServer.JointAllocation.reference_adapted line 1585
  147. lemma OAI.KServer.JointAllocation.size_mass_joint line 1590
  148. lemma OAI.KServer.JointAllocation.size_mass line 1597
  149. def OAI.KServer.HierarchicalQuota.keyCross line 1628
  150. def OAI.KServer.HierarchicalQuota.keyTransport line 1631
  151. def OAI.KServer.HierarchicalQuota.prefixTransport line 1634
  152. lemma OAI.KServer.HierarchicalQuota.prefixCross_zero line 1638
  153. lemma OAI.KServer.HierarchicalQuota.prefixCross_step line 1646
  154. lemma OAI.KServer.HierarchicalQuota.prefix_transport_bound line 1667
  155. lemma OAI.KServer.HierarchicalQuota.tree_drift_bound line 1681
  156. lemma OAI.KServer.ActualCharges.total_sum line 1707
  157. lemma OAI.KServer.ActualCharges.avg_const_one line 1711