OAI/Combinatorics/KServer/Partitions.lean

GitHub source file

223 declarations, 0 contain sorry, 0 declared as axioms

The actual true-prefix heavy-center recursion of §07. All physical and filtering steps are included in its potential budget, not only edit steps.

  1. lemma OAI.KServer.Pilot.filtered_potential line 18

    Source documentation

    Exact filtering for a profile chosen from the old observation history. The old compact minimizer is a single admissible competitor on each old fiber.

    lemma filtered_potential (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω)
    (H H' : Ω → ℕ) (hr : ∀ ω ν, H' ω = H' ν → H ω = H ν)
    (T : Template) (r : ℝ) (f g : Ω → Y → ℝ)
    (hg : ∀ y, Adapted H (fun ω => g ω y)) :
    avg w (fun ω => potential T r (fun y => posterior w H' (fun ν => f ν y) ω) (g ω)) ≤
      avg w (fun ω => potential T r (fun y => posterior w H (fun ν => f ν y) ω) (g ω)) := by
…

    Mentions: OAI.KServer.Pilot.Template, OAI.KServer.Pilot.potential

  2. lemma OAI.KServer.FiniteExperiment.requestHistory_refines line 70
  3. lemma OAI.KServer.FiniteExperiment.pilot_filtering line 82

    Source documentation

    The precise signed filtering contribution of the actual hidden optimum.

    lemma pilot_filtering (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (T : Pilot.Template) (r : ℝ) (t : Fin H) (g : (Fin H → Y) → Y → ℝ)
    (hg : ∀ y, Adapted (requestHistory t.val) (fun σ => g σ y)) :
    avg law.val (fun σ => potential T r (muBefore s law t σ) (g σ)) ≤
      avg law.val (fun σ => potential T r (mu s law t.val σ) (g σ)) :=
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.Pilot.Template, OAI.KServer.FiniteExperiment.requestHistory, OAI.KServer.FiniteExperiment.muBefore, OAI.KServer.FiniteExperiment.mu

  4. lemma OAI.KServer.FiniteExperiment.pilot_physical line 92

    Source documentation

    Each realized physical update obeys the literal compact-pilot drift bound.

    lemma pilot_physical (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (T : Pilot.Template) {γ δ r₀ τ : ℝ} (t : Fin H) (σ : Fin H → Y)
    (g : ℕ → Y → ℝ) (n p : ℕ) (hσ : 0 < law.val σ)
    (hr : 0 < r₀) (hτ : 2 ≤ τ) (hγ0 : 0 < γ)
    (hγ : γ ≤ min (T.σ/64) (1/(1+T.L))) (hδ0 : 0 < δ) (hδ : δ ≤ 1/4112)
    (hpow : 100*T.R ≤ γ*(2:ℝ)^p)
    (hg : ∀ j<n, ∀ y, g j y ∈ Set.Icc 0 1)
    (hgLip : ∀ j<n, ∀ y z, |g j y-g j z| ≤ T.L*(dist y z/radius r₀ τ j)) :
    ∑ j ∈ range n, max (potential T (radius r₀ τ j) (mu s law (t.val+1) σ) (g j)-
      potential T (radius r₀ τ j) (muBefore s law t σ) (g j)) 0 ≤
        driftConstant T γ δ p*(1+Real.log ((k:ℝ)+1)) *
          ∑ y, nu s law t σ y * dist y (σ t) := by
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.Pilot.Template, OAI.KServer.FiniteExperiment.mu, OAI.KServer.FiniteExperiment.muBefore, OAI.KServer.FiniteExperiment.nu

  5. theorem OAI.KServer.FiniteExperiment.pilot_physical_budget line 122

    Source documentation

    The actual expected physical pilot increments are paid entirely by OPT.

    theorem pilot_physical_budget (s : Configuration k Y)
    (law : FiniteDistribution (Fin H → Y)) (T : Pilot.Template)
    {γ δ r₀ τ : ℝ} (g : Fin H → (Fin H → Y) → ℕ → Y → ℝ) (n p : ℕ)
    (hr : 0 < r₀) (hτ : 2 ≤ τ) (hγ0 : 0 < γ)
    (hγ : γ ≤ min (T.σ/64) (1/(1+T.L))) (hδ0 : 0 < δ) (hδ : δ ≤ 1/4112)
    (hpow : 100*T.R ≤ γ*(2:ℝ)^p)
    (hg : ∀ t σ j, j<n → ∀ y, g t σ j y ∈ Set.Icc 0 1)
    (hgLip : ∀ t σ j, j<n → ∀ y z,
      |g t σ j y-g t σ j z| ≤ T.L*(dist y z/radius r₀ τ j)) :
    (∑ t : Fin H, avg law.val (fun σ => ∑ j ∈ range n,
      max (potential T (radius r₀ τ j) (mu s law (t.val+1) σ) (g t σ j)-
        potential T (radius r₀ τ j) (muBefore s law t σ) (g t σ j)) 0)) ≤
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.Pilot.Template, OAI.KServer.FiniteExperiment.mu, OAI.KServer.FiniteExperiment.muBefore

  6. theorem OAI.KServer.FiniteExperiment.pilot_edit_budget line 157

    Source documentation

    All-step signed filtering plus physical drift, before any decision to edit. The edit charge is the literal difference of two achieved pilot minima.

    theorem pilot_edit_budget (s : Configuration k Y)
    (law : FiniteDistribution (Fin H → Y)) (T : Pilot.Template)
    {γ δ r₀ τ : ℝ} (g : ℕ → (Fin H → Y) → ℕ → Y → ℝ) (n p : ℕ)
    (hr : 0 < r₀) (hτ : 2 ≤ τ) (hγ0 : 0 < γ)
    (hγ : γ ≤ min (T.σ/64) (1/(1+T.L))) (hδ0 : 0 < δ) (hδ : δ ≤ 1/4112)
    (hpow : 100*T.R ≤ γ*(2:ℝ)^p)
    (hg : ∀ t σ j, j<n → ∀ y, g t σ j y ∈ Set.Icc 0 1)
    (hgLip : ∀ t σ j, j<n → ∀ y z,
      |g t σ j y-g t σ j z| ≤ T.L*(dist y z/radius r₀ τ j))
    (hga : ∀ t j, j<n → ∀ y,
      Adapted (requestHistory t) (fun σ => g t σ j y)) :
    (∑ t : Fin H, avg law.val (fun σ => ∑ j ∈ range n,
…

    Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.Pilot.Template, OAI.KServer.FiniteExperiment.requestHistory

  7. def OAI.KServer.HeavyCenters.template line 242
  8. def OAI.KServer.HeavyCenters.annulus line 252

    Source documentation

    The exact annulus charged at a heavy update.

    def annulus (x : Y) (r : ℝ) : Finset Y :=
…
  9. lemma OAI.KServer.HeavyCenters.annulus_bump_one line 255
  10. lemma OAI.KServer.HeavyCenters.profile_weight_nonneg line 272
  11. lemma OAI.KServer.HeavyCenters.profile_residual_bound line 283
  12. lemma OAI.KServer.HeavyCenters.edit_integrand_drop line 301

    Source documentation

    Pointwise objective decrease from the literal center replacement.

    lemma edit_integrand_drop {r : ℝ} (hr : 0<r) (C : Finset Y) (x : Y)
    {z : Y → ℝ} (hz : Feasible template r z)
    (hfar : ∀ a∈C,8*r<dist a x)
    (hmiddle : ∀ i,r/4 ≤ dist i x → dist i x ≤ 256*r → z i=0)
    (hnear : ∃ s,dist s x<r/4 ∧ (1/2:ℝ) ≤ z s) (p : Y) :
    127*(if p∈annulus x r then (1:ℝ) else 0) ≤
      integrand template r (profile r C) z p-
        integrand template r (profile r (replace r C x)) z p := by
…

    Mentions: OAI.KServer.HeavyCenters.template, OAI.KServer.HeavyCenters.annulus, OAI.KServer.HeavyCenters.profile, OAI.KServer.HeavyCenters.replace

  13. theorem OAI.KServer.HeavyCenters.pilot_edit_drop line 352

    Source documentation

    The genuine heavy edit decrease, from compact minimizer local structure; no pilot decrease is posed as a hypothesis.

    theorem pilot_edit_drop {r γ δ : ℝ} (hr : 0<r) (C : Finset Y) (x : Y)
    {μ : Y → ℝ} (hμ : ∀ y,0≤μ y) (hγ0 : 0≤γ) (hγ : γ≤1/64)
    (hδ : δ≤1/4112) (hM : 0<Pilot.mass μ (Pilot.ball x (γ*r)))
    (hheavy : Pilot.mass μ (Pilot.ball x (51200*r)) ≤
      (1+δ)*Pilot.mass μ (Pilot.ball x (γ*r)))
    (hfar : ∀ a∈C,8*r<dist a x) :
    127*r*Pilot.mass μ (annulus x r) ≤
      potential template r μ (profile r C)-potential template r μ (profile r (replace r C x)) := by
…

    Mentions: OAI.KServer.Pilot.mass, OAI.KServer.Pilot.ball, OAI.KServer.HeavyCenters.annulus, OAI.KServer.HeavyCenters.template, OAI.KServer.HeavyCenters.profile, OAI.KServer.HeavyCenters.replace

  14. def OAI.KServer.HeavyCenters.Active line 422
  15. def OAI.KServer.HeavyCenters.step line 426
  16. lemma OAI.KServer.HeavyCenters.step_separated line 429
  17. def OAI.KServer.HeavyCenters.centers line 447

    Source documentation

    Initially empty. End-of-input states are frozen; requests before then use the genuine posterior at the new true prefix.

    def centers (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (r γ δ : ℝ) (σ : Fin H → Y) : ℕ → Finset Y
  | 0 => ∅
  | t+1 => if ht : t<H then
      step r γ δ (centers s law r γ δ σ t) (mu s law (t+1) σ) (σ ⟨t,ht⟩)
    else centers s law r γ δ σ t

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

  18. lemma OAI.KServer.HeavyCenters.centers_zero line 454
  19. lemma OAI.KServer.HeavyCenters.centers_succ line 456
  20. lemma OAI.KServer.HeavyCenters.centers_separated line 462
  21. lemma OAI.KServer.HeavyCenters.centers_adapted line 473
  22. lemma OAI.KServer.HeavyCenters.inner_mass_pos line 489
  23. def OAI.KServer.HeavyCenters.charge line 501

    Source documentation

    Exact annular charge made by a real center edit, zero on non-edit steps.

    def charge (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    (r γ δ : ℝ) (t : Fin H) (σ : Fin H → Y) : ℝ :=
…

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

  24. lemma OAI.KServer.HeavyCenters.charge_nonneg line 506
  25. lemma OAI.KServer.HeavyCenters.charge_le_drop line 514
  26. theorem OAI.KServer.HeavyCenters.annulus_budget line 531

    Source documentation

    The source's all-step heavy-annulus budget for the actual adaptive construction, with a finite endpoint bound independent of law and horizon.

    theorem annulus_budget (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    {γ δ r₀ τ : ℝ} (n p : ℕ)
    (hr : 0<r₀) (hτ : 2≤τ) (hγ0 : 0<γ) (hγ : γ≤1/64)
    (hδ0 : 0<δ) (hδ : δ≤1/4112) (hpow : 51200≤γ*(2:ℝ)^p) :
    (∑ t : Fin H,avg law.val (fun σ => ∑ j∈range n,
      charge s law (radius r₀ τ j) γ δ t σ)) ≤
      driftConstant template γ δ 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.HeavyCenters.charge, OAI.KServer.HeavyCenters.template

  27. lemma OAI.KServer.OnlineLabels.unused_exists line 576
  28. def OAI.KServer.OnlineLabels.stage line 587

    Source documentation

    A finite coloring chosen at each insertion using only earlier colors.

    def stage (hM : 0<M) (conflict : ℕ → Finset ℕ)
    (hcard : ∀ t, (conflict t).card<M) : ℕ → ℕ → Fin M
  | 0 => fun _ => ⟨0,hM⟩
  | t+1 => fun j => if j=t then
      (unused_exists (conflict t) (stage hM conflict hcard t) (hcard t)).choose
      else stage hM conflict hcard t j

    Mentions: OAI.KServer.OnlineLabels.unused_exists

  29. lemma OAI.KServer.OnlineLabels.stage_step_old line 594
  30. lemma OAI.KServer.OnlineLabels.stage_stable line 599
  31. def OAI.KServer.OnlineLabels.color line 610

    Source documentation

    Permanent color of a chronological record; later stages never modify it.

    def color (hM : 0<M) (conflict : ℕ → Finset ℕ)
    (hcard : ∀ t, (conflict t).card<M) (i : ℕ) : Fin M :=
…
  32. lemma OAI.KServer.OnlineLabels.color_avoids line 614
  33. theorem OAI.KServer.OnlineLabels.color_injective_on line 625

    Source documentation

    If each simultaneous or cooldown pair was included when the later record was inserted, the fixed pool colors it injectively. This local premise is on record geometry, not an assumed random algorithm or cost estimate.

    theorem color_injective_on (hM : 0<M) (conflict : ℕ → Finset ℕ)
    (hcard : ∀ t, (conflict t).card<M)
    (hbefore : ∀ t, ∀ j ∈ conflict t, j<t) (S : Set ℕ)
    (hpairs : ∀ i ∈ S, ∀ j ∈ S, j < i → j ∈ conflict i) :
    Set.InjOn (color hM conflict hcard) S := by
…

    Mentions: OAI.KServer.OnlineLabels.color

  34. lemma OAI.KServer.OnlineLabels.cooldown_card line 638

    Source documentation

    The source's 4M+4 pool has strictly more slots than the two reserved sets and two new records excluded by a one-step cooldown.

    lemma cooldown_card (A B fresh : Finset ℕ) {N : ℕ}
    (hA : A.card ≤ N) (hB : B.card ≤ N) (hf : fresh.card ≤ 2) :
    (A∪B∪fresh).card < 4*N+4 := by
…
  35. abbrev OAI.KServer.HeavyLabels.Pool line 661
  36. def OAI.KServer.HeavyLabels.overlap line 662
  37. lemma OAI.KServer.HeavyLabels.overlap_distance line 665
  38. lemma OAI.KServer.HeavyLabels.overlap_unique line 673
  39. lemma OAI.KServer.HeavyLabels.unused line 686
  40. def OAI.KServer.HeavyLabels.fresh line 697
  41. lemma OAI.KServer.HeavyLabels.fresh_avoids line 699
  42. def OAI.KServer.HeavyLabels.insertedLabel line 703
  43. def OAI.KServer.HeavyLabels.updatedLabel line 706
  44. lemma OAI.KServer.HeavyLabels.inserted_reuses line 709
  45. lemma OAI.KServer.HeavyLabels.existing_match line 717
  46. lemma OAI.KServer.HeavyLabels.inserted_diff_kept line 726
  47. lemma OAI.KServer.HeavyLabels.update_injective line 735

    Source documentation

    An actual update preserves injective active heavy labels.

    lemma update_injective {C D : Finset Y} {rad : Y → ℝ} {label prev : Y → Pool Y} {x : Y} {r R : ℝ}
    (hr : 0<r) (hrad : ∀ a∈C,rad a≤20*r) (hR : R≤20*r)
    (hl : Set.InjOn label (C:Set Y)) :
    Set.InjOn (updatedLabel C D rad label prev x R) (replace r C x:Set Y) := by
…

    Mentions: OAI.KServer.HeavyLabels.Pool, OAI.KServer.HeavyLabels.updatedLabel

  48. lemma OAI.KServer.HeavyLabels.common_anchor line 763

    Source documentation

    Every common coordinate label keeps its anchor, except for a genuine intersecting-ball reuse; in that case it moves at most40r.

    lemma common_anchor {C D : Finset Y} {rad : Y → ℝ} {label prev : Y → Pool Y} {x a b : Y} {r R : ℝ}
    (hrad : ∀ a∈C,rad a≤20*r) (hR : R≤20*r)
    (hl : Set.InjOn label (C:Set Y)) (ha : a∈C) (hb : b∈replace r C x)
    (he : label a=updatedLabel C D rad label prev x R b) : a=b ∨ dist a b≤40*r := by
…

    Mentions: OAI.KServer.HeavyLabels.Pool, OAI.KServer.HeavyLabels.updatedLabel

  49. def OAI.KServer.PartitionProbabilities.position line 790

    Source documentation

    Normalized clipped position in the source radius interval [r,2*r].

    def position (r a : ℝ) : ℝ := min (max (a/r-1) 0) 1
  50. lemma OAI.KServer.PartitionProbabilities.position_range line 792
  51. lemma OAI.KServer.PartitionProbabilities.position_mono line 796
  52. lemma OAI.KServer.PartitionProbabilities.position_difference line 800
  53. def OAI.KServer.PartitionProbabilities.tail line 822

    Source documentation

    The exact tail of the density in eq. tier-radius-density. The clipped formula includes both support endpoints (which have zero atom).

    def tail (lam r a : ℝ) : ℝ :=
…
  54. lemma OAI.KServer.PartitionProbabilities.tail_range line 825
  55. lemma OAI.KServer.PartitionProbabilities.tail_antitone line 834
  56. lemma OAI.KServer.PartitionProbabilities.position_of_le line 841
  57. lemma OAI.KServer.PartitionProbabilities.position_of_ge line 845
  58. lemma OAI.KServer.PartitionProbabilities.tail_of_le line 849
  59. lemma OAI.KServer.PartitionProbabilities.tail_of_ge line 853
  60. lemma OAI.KServer.PartitionProbabilities.exp_difference_le line 857

    Source documentation

    Elementary exponential secant bound, including arbitrary negative inputs.

    lemma exp_difference_le (u v : ℝ) : Real.exp u-Real.exp v ≤ (u-v)*Real.exp u := by
…
  61. theorem OAI.KServer.PartitionProbabilities.tail_interval_bound line 867

    Source documentation

    The source first-hit tail inequality, valid even if the interval crosses one or both endpoints of the radius support.

    theorem tail_interval_bound {lam r a b : ℝ} (hlam : 0 < lam) (hr : 0 < r) (hab : a ≤ b) :
    tail lam r a-tail lam r b ≤
      (lam*(b-a)/r)*(tail lam r a+1/(Real.exp lam-1)) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.tail

  62. def OAI.KServer.PartitionProbabilities.prefixMiss line 887

    Source documentation

    Prefix miss probabilities for independent records in chronological order.

    def prefixMiss (p : ℕ → ℝ) (n : ℕ) : ℝ := ∏ i ∈ range n, (1-p i)
  63. lemma OAI.KServer.PartitionProbabilities.prefixMiss_zero line 889
  64. lemma OAI.KServer.PartitionProbabilities.prefixMiss_succ line 890
  65. lemma OAI.KServer.PartitionProbabilities.prefixMiss_range line 893
  66. theorem OAI.KServer.PartitionProbabilities.first_hit_sum line 903

    Source documentation

    Exact first-hit partition of the probability of at least one hit.

    theorem first_hit_sum (p : ℕ → ℝ) (n : ℕ) :
    (∑ i ∈ range n, prefixMiss p i*p i)=1-prefixMiss p n := by
…

    Mentions: OAI.KServer.PartitionProbabilities.prefixMiss

  67. theorem OAI.KServer.PartitionProbabilities.first_hit_bound line 911

    Source documentation

    First-hit separation bound after conditioning on presences. It sums the individual tail coefficients, rather than paying for all K² hits separately.

    theorem first_hit_bound {p s : ℕ → ℝ} {c ε : ℝ} (n : ℕ)
    (hp : ∀ i, p i ∈ Set.Icc (0:ℝ) 1) (hc : 0 ≤ c) (hε : 0 ≤ ε)
    (hs : ∀ i < n, s i ≤ c*(p i+ε)) :
    (∑ i ∈ range n, prefixMiss p i*s i) ≤ c*(1+ε*n) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.prefixMiss

  68. def OAI.KServer.PartitionProbabilities.productWeight line 939

    Source documentation

    Literal independent product tape; independence is proved by multiplication, not postulated as an assumption about adaptive states.

    def productWeight (w : ∀ i, Ω i → ℝ) (o : ∀ i, Ω i) : ℝ := ∏ i, w i (o i)
  69. def OAI.KServer.PartitionProbabilities.probability line 941
  70. lemma OAI.KServer.PartitionProbabilities.productWeight_nonneg line 946
  71. lemma OAI.KServer.PartitionProbabilities.productWeight_sum line 949
  72. lemma OAI.KServer.PartitionProbabilities.product_expectation line 955
  73. lemma OAI.KServer.PartitionProbabilities.rectangle_probability line 961
  74. lemma OAI.KServer.PartitionProbabilities.probability_range line 974
  75. lemma OAI.KServer.PartitionProbabilities.complement_probability line 991
  76. def OAI.KServer.PartitionProbabilities.firstSeparation line 1007

    Source documentation

    Exactly the source separating-first-hit event in chronological order.

    def firstSeparation (hit sep : ∀ i, Ω i → Prop) (o : ∀ i, Ω i) : Prop :=
…
  77. def OAI.KServer.PartitionProbabilities.firstAt line 1010
  78. lemma OAI.KServer.PartitionProbabilities.firstAt_unique line 1014
  79. lemma OAI.KServer.PartitionProbabilities.firstSeparation_probability line 1021
  80. lemma OAI.KServer.PartitionProbabilities.firstAt_probability line 1045

    Source documentation

    Evaluation of one first-hit rectangle under the constructed product tape.

    lemma firstAt_probability {hit sep : ∀ i, Ω i → Prop}
    (w : ∀ i, Ω i → ℝ) (hw : ∀ i, ∑ a, w i a=1) (i : Fin n) :
    probability w (firstAt hit sep i)=
      (∑ a, if sep i a then w i a else 0) *
        ∏ j ∈ univ.filter (fun j : Fin n => j < i), (1 - ∑ a, if hit j a then w j a else 0) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.probability, OAI.KServer.PartitionProbabilities.firstAt

  81. theorem OAI.KServer.PartitionProbabilities.independent_first_hit_bound line 1084

    Source documentation

    The chronological first-hit estimate under the literal finite product law. No independence is asserted for an adaptive filtration: this theorem applies only after its deterministic schedule and surviving indices have been fixed.

    theorem independent_first_hit_bound {hit sep : ∀ i, Ω i → Prop}
    (w : ∀ i, Ω i → ℝ) (hw : ∀ i a, 0 ≤ w i a)
    (hw1 : ∀ i, ∑ a, w i a=1) (hsep : ∀ i a, sep i a → hit i a)
    {c ε : ℝ} (hc : 0 ≤ c) (hε : 0 ≤ ε)
    (hm : ∀ i, (∑ a, if sep i a then w i a else 0) ≤
      c*((∑ a, if hit i a then w i a else 0)+ε)) :
    probability w (firstSeparation hit sep) ≤ c*(1+ε*n) := by
…

    Mentions: OAI.KServer.PartitionProbabilities.probability, OAI.KServer.PartitionProbabilities.firstSeparation

  82. def OAI.KServer.FiniteSurvival.weight line 1140

    Source documentation

    A finite lifetime d is alive at ages 0,...,d.

    def weight (s : ℕ → ℝ) {N : ℕ} (d : Fin N) : ℝ := s d-s (d+1)
  83. def OAI.KServer.FiniteSurvival.probability line 1142
  84. lemma OAI.KServer.FiniteSurvival.weight_nonneg line 1146
  85. lemma OAI.KServer.FiniteSurvival.weight_sum line 1149
  86. lemma OAI.KServer.FiniteSurvival.probability_living line 1153
  87. theorem OAI.KServer.FiniteSurvival.inverse_tail line 1180

    Source documentation

    An actual finite probability law realizes every prescribed decreasing survival tail exactly; this is the finite inverse-tail construction, not an independence or randomness assumption.

    theorem inverse_tail {s : ℕ → ℝ} {N : ℕ} (hs : Antitone s)
    (hs0 : s 0=1) (hsN : s N=0) :
    (∀ d : Fin N, 0 ≤ weight s d) ∧ (∑ d : Fin N, weight s d=1) ∧
      ∀ a ≤ N, probability s (fun d : Fin N => a ≤ (d:ℕ))=s a := by
…

    Mentions: OAI.KServer.FiniteSurvival.weight, OAI.KServer.FiniteSurvival.probability

  88. lemma OAI.KServer.FiniteSurvival.probability_crossing line 1190

    Source documentation

    The exact probability of a single-bin threshold crossing.

    lemma probability_crossing (s : ℕ → ℝ) (N a b : ℕ) (hab : a ≤ b) (hb : b ≤ N) :
    probability s (fun d : Fin N => a ≤ (d:ℕ) ∧ (d:ℕ)<b)=s a-s b := by
…

    Mentions: OAI.KServer.FiniteSurvival.probability

  89. def OAI.KServer.FiniteRadius.grid line 1219
  90. lemma OAI.KServer.FiniteRadius.grid_pos line 1221
  91. def OAI.KServer.FiniteRadius.point line 1224
  92. lemma OAI.KServer.FiniteRadius.point_mono line 1227
  93. lemma OAI.KServer.FiniteRadius.point_range line 1230
  94. lemma OAI.KServer.FiniteRadius.point_zero line 1240
  95. def OAI.KServer.FiniteRadius.survival line 1247
  96. lemma OAI.KServer.FiniteRadius.survival_fin line 1250
  97. lemma OAI.KServer.FiniteRadius.survival_zero line 1253
  98. lemma OAI.KServer.FiniteRadius.survival_last line 1258
  99. lemma OAI.KServer.FiniteRadius.survival_nonneg line 1261
  100. lemma OAI.KServer.FiniteRadius.survival_antitone line 1267
  101. def OAI.KServer.FiniteRadius.weights line 1278

    Source documentation

    Weights of the actual finite radius outcome.

    def weights (D : Finset ℝ) (lam r : ℝ) (i : Fin (grid D r).card) : ℝ :=
…

    Mentions: OAI.KServer.FiniteRadius.grid

  102. lemma OAI.KServer.FiniteRadius.weights_nonneg line 1281
  103. lemma OAI.KServer.FiniteRadius.weights_sum line 1285
  104. lemma OAI.KServer.FiniteRadius.grid_tail line 1291
  105. def OAI.KServer.FiniteUniform.tail line 1323
  106. lemma OAI.KServer.FiniteUniform.tail_nonneg line 1325
  107. lemma OAI.KServer.FiniteUniform.tail_le_one line 1326
  108. lemma OAI.KServer.FiniteUniform.tail_of_le line 1327
  109. lemma OAI.KServer.FiniteUniform.tail_of_ge line 1330
  110. lemma OAI.KServer.FiniteUniform.tail_antitone line 1333
  111. lemma OAI.KServer.FiniteUniform.tail_lipschitz line 1336
  112. def OAI.KServer.FiniteUniform.survival line 1345
  113. lemma OAI.KServer.FiniteUniform.survival_fin line 1347
  114. lemma OAI.KServer.FiniteUniform.survival_zero line 1349
  115. lemma OAI.KServer.FiniteUniform.survival_last line 1352
  116. lemma OAI.KServer.FiniteUniform.survival_nonneg line 1353
  117. lemma OAI.KServer.FiniteUniform.survival_antitone line 1357
  118. def OAI.KServer.FiniteUniform.weights line 1366
  119. lemma OAI.KServer.FiniteUniform.weights_nonneg line 1367
  120. lemma OAI.KServer.FiniteUniform.weights_sum line 1369
  121. lemma OAI.KServer.FiniteUniform.grid_tail line 1373
  122. lemma OAI.KServer.FiniteUniform.query_tail line 1389
  123. def OAI.KServer.FiniteUniform.thresholds line 1406
  124. lemma OAI.KServer.FiniteUniform.dist_threshold line 1407
  125. abbrev OAI.KServer.FiniteUniform.Outcome line 1409
  126. def OAI.KServer.FiniteUniform.radius line 1410
  127. def OAI.KServer.FiniteUniform.law line 1411
  128. lemma OAI.KServer.FiniteUniform.radius_range line 1412
  129. lemma OAI.KServer.FiniteUniform.law_nonneg line 1415
  130. lemma OAI.KServer.FiniteUniform.law_sum line 1416
  131. lemma OAI.KServer.FiniteUniform.ball_probability line 1417
  132. def OAI.KServer.FiniteUniform.separates line 1426
  133. lemma OAI.KServer.FiniteUniform.separates_comm line 1429
  134. lemma OAI.KServer.FiniteUniform.separation_ordered line 1431
  135. theorem OAI.KServer.FiniteUniform.one_ball_bound line 1443
  136. structure OAI.KServer.HeavySchedule.Data line 1476
  137. def OAI.KServer.HeavySchedule.initial line 1481
  138. def OAI.KServer.HeavySchedule.run line 1484
  139. lemma OAI.KServer.HeavySchedule.run_valid line 1500
  140. def OAI.KServer.HeavySchedule.birth line 1531
  141. lemma OAI.KServer.HeavySchedule.radius_birth line 1540
  142. lemma OAI.KServer.HeavySchedule.present_birth line 1558
  143. lemma OAI.KServer.FiniteBallLaw.query_tail line 1598
  144. def OAI.KServer.FiniteBallLaw.thresholds line 1617
  145. lemma OAI.KServer.FiniteBallLaw.dist_threshold line 1619
  146. abbrev OAI.KServer.FiniteBallLaw.Outcome line 1622
  147. def OAI.KServer.FiniteBallLaw.radius line 1625
  148. def OAI.KServer.FiniteBallLaw.law line 1627
  149. lemma OAI.KServer.FiniteBallLaw.law_nonneg line 1629
  150. lemma OAI.KServer.FiniteBallLaw.law_sum line 1632
  151. lemma OAI.KServer.FiniteBallLaw.radius_range line 1635
  152. lemma OAI.KServer.FiniteBallLaw.ball_probability line 1638
  153. def OAI.KServer.FiniteBallLaw.hit line 1642
  154. def OAI.KServer.FiniteBallLaw.separates line 1645
  155. lemma OAI.KServer.FiniteBallLaw.separation_hit line 1649
  156. lemma OAI.KServer.FiniteBallLaw.hit_min line 1654
  157. lemma OAI.KServer.FiniteBallLaw.separation_interval line 1658
  158. lemma OAI.KServer.FiniteBallLaw.min_threshold line 1675
  159. lemma OAI.KServer.FiniteBallLaw.max_threshold line 1680
  160. lemma OAI.KServer.FiniteBallLaw.hit_probability line 1685
  161. lemma OAI.KServer.FiniteBallLaw.separation_probability line 1691
  162. lemma OAI.KServer.FiniteBallLaw.width_distance line 1707
  163. lemma OAI.KServer.FiniteBallLaw.one_ball_bound line 1711
  164. theorem OAI.KServer.FiniteBallLaw.chronological_bound line 1724

    Source documentation

    The finite radius tape realizes the exact source truncated-exponential first-hit bound for any fixed chronological list of present candidates.

    theorem chronological_bound {n : ℕ} {lam r : ℝ} (hlam : 0 < lam) (hr : 0 < r)
    (centers : Fin n → Y) (x y : Y) :
    probability (fun _ : Fin n => law (Y:=Y) lam r)
…

    Mentions: OAI.KServer.FiniteBallLaw.law

  165. lemma OAI.KServer.FiniteBallLaw.lambda_pos line 1737
  166. theorem OAI.KServer.FiniteBallLaw.bounded_roster line 1744

    Source documentation

    With at most K² potentially hitting records the chronological estimate is 2λd/r, independent of the total number of previous insertions.

    theorem bounded_roster {n K : ℕ} (hK : 1 ≤ K) (hn : n ≤ K^2) {r : ℝ} (hr : 0 < r)
    (centers : Fin n → Y) (x y : Y) :
    probability (fun _ : Fin n => law (Y:=Y) (Real.log (1+(K:ℝ)^2)) r)
…

    Mentions: OAI.KServer.FiniteBallLaw.law

  167. def OAI.KServer.Chronological.age line 1778

    Source documentation

    Number of later insertions in the fixed-radius neighbourhood of an entry.

    def age (center : ℕ → Y) (I : Finset ℕ) (R : ℝ) (i : ℕ) : ℕ := by
…
  168. def OAI.KServer.Chronological.young line 1783

    Source documentation

    Chronological, not surviving, entries below an age cutoff.

    def young (center : ℕ → Y) (I : Finset ℕ) (R : ℝ) (A : ℕ) : Finset ℕ := by
…
  169. lemma OAI.KServer.Chronological.mem_young line 1787
  170. lemma OAI.KServer.Chronological.age_mono line 1792
  171. lemma OAI.KServer.Chronological.age_insert line 1801

    Source documentation

    Adding the next insertion increments precisely neighbouring old entries.

    lemma age_insert (center : ℕ → Y) (I : Finset ℕ) (R : ℝ) {i t : ℕ}
    (ht : t ∉ I) (hit : i < t) :
    age center (insert t I) R i = age center I R i +
      if dist (center i) (center t) ≤ R then 1 else 0 := by
…

    Mentions: OAI.KServer.Chronological.age

  172. lemma OAI.KServer.Chronological.age_new line 1814
  173. theorem OAI.KServer.Chronological.local_age_count line 1828

    Source documentation

    Actual age-count lemma. No independence or surviving-record assumption is used, and repeated centers are allowed.

    theorem local_age_count (center : ℕ → Y) (I S : Finset ℕ) (R : ℝ) (A : ℕ)
    (hSI : S ⊆ I) (hyoung : ∀ i ∈ S, age center I R i < A)
    (hdiam : ∀ i ∈ S, ∀ j ∈ S, dist (center i) (center j) ≤ R) :
    S.card ≤ A := by
…

    Mentions: OAI.KServer.Chronological.age

  174. def OAI.KServer.Chronological.insertTest line 1852

    Source documentation

    The exact test in the manuscript. Its input is a qualifying request, not a condition involving lifetimes, radii, allocation, or rounding.

    def insertTest (center : ℕ → Y) (I : Finset ℕ) (r : ℝ) (K t : ℕ)
    (qualifies : Prop) : Prop :=
…
  175. def OAI.KServer.Chronological.schedule line 1858

    Source documentation

    Chronological insertion history after t requests. qualifies will be computed from the actual true-prefix posterior and the fixed tier parameter.

    def schedule (request : ℕ → Y) (r : ℝ) (K : ℕ) (qualifies : ℕ → Prop) : ℕ → Finset ℕ
  | 0 => ∅
  | t+1 => by
      classical
      let I := schedule request r K qualifies t
…
  176. lemma OAI.KServer.Chronological.schedule_before line 1865
  177. lemma OAI.KServer.Chronological.qualified_coverage line 1879
  178. theorem OAI.KServer.Chronological.reserved_count line 1907

    Source documentation

    Reservation count for the complete chronological roster, by applying the local bound separately to each center in the finite metric.

    theorem reserved_count [Fintype Y] (center : ℕ → Y) (I : Finset ℕ) {R : ℝ}
    (hR : 0 ≤ R) (A : ℕ) : (young center I R A).card ≤ Fintype.card Y * A := by
…

    Mentions: OAI.KServer.Chronological.young

  179. theorem OAI.KServer.SparseFirstHit.sparse_bound line 1942

    Source documentation

    An error is paid only on indices that can hit a queried point. This permits a preallocated horizon-size tape without a horizon-size bound.

    theorem sparse_bound {n : ℕ} {Ω : Fin n → Type*} [∀ i, Fintype (Ω i)]
    {hit sep : ∀ i, Ω i → Prop} (w : ∀ i, Ω i → ℝ)
    (hw : ∀ i a, 0 ≤ w i a) (hw1 : ∀ i, ∑ a, w i a=1)
    (hsep : ∀ i a, sep i a → hit i a) {c : ℝ} (ε : Fin n → ℝ)
    (hc : 0 ≤ c) (hε : ∀ i, 0 ≤ ε i)
    (hm : ∀ i, (∑ a, if sep i a then w i a else 0) ≤
      c*((∑ a, if hit i a then w i a else 0)+ε i)) :
    probability w (firstSeparation hit sep) ≤ c*(1+∑ i, ε i) := by
…
  180. def OAI.KServer.SparseFirstHit.candidates line 1984
  181. lemma OAI.KServer.SparseFirstHit.absent_hit line 1987
  182. theorem OAI.KServer.SparseFirstHit.present_bound line 1994

    Source documentation

    All previous insertion ordinals, with nonpresent records literally suppressed. Only potential hitters contribute the truncation error.

    theorem present_bound {lam r : ℝ} (hlam : 0 < lam) (hr : 0 < r)
    (center : Fin H → Y) (present : Fin H → Prop) (x y : Y) :
    probability (fun _ : Fin H => law (Y:=Y) lam r)
…
  183. lemma OAI.KServer.SparseFirstHit.close_centers line 2027
  184. lemma OAI.KServer.SparseFirstHit.candidate_count line 2045
  185. theorem OAI.KServer.SparseFirstHit.chronological_roster_bound line 2068

    Source documentation

    Conditional on any actual presence pattern, the horizon-size radius tape has the stated K²-independent first-hit bound, by the literal age count.

    theorem chronological_roster_bound {K : ℕ} (hK : 1 ≤ K) {r : ℝ} (hr : 0 < r)
    (center : ℕ → Y) (I : Finset ℕ) (present : Fin H → Prop)
    (hp : ∀ i, present i → (i:ℕ)∈I ∧ age center I (20*r) i<K^2)
    (x y : Y) (hxy : dist x y ≤ r) :
    probability (fun _ : Fin H => law (Y:=Y) (Real.log (1+(K:ℝ)^2)) r)
…
  186. def OAI.KServer.RosterLifetimes.survive line 2103

    Source documentation

    Survival through N independent retirement trials of rate q.

    def survive (q : ℝ) (N : ℕ) : ℝ := (1-q)^N
  187. lemma OAI.KServer.RosterLifetimes.survive_range line 2105
  188. lemma OAI.KServer.RosterLifetimes.survive_mono line 2110
  189. lemma OAI.KServer.RosterLifetimes.survive_exp line 2114
  190. lemma OAI.KServer.RosterLifetimes.cubic_decay line 2120
  191. lemma OAI.KServer.RosterLifetimes.actual_exponential_bound line 2129

    Source documentation

    Explicit uniform version of K² exp(-(K-1))=O(1/K).

    lemma actual_exponential_bound {x : ℝ} (hx : 2 ≤ x) :
    x^2*Real.exp (-(x-1)) ≤ 48/x := by
…
  192. lemma OAI.KServer.RosterLifetimes.short_exponential_bound line 2142

    Source documentation

    Explicit uniform auxiliary tail estimate. The denominator really is √K, not K; the two tapes are never identified.

    lemma short_exponential_bound {x : ℝ} (hx : 2 ≤ x) :
    x*Real.exp (-((x-1)/Real.sqrt x)) ≤ 48/Real.sqrt x := by
…
  193. def OAI.KServer.RosterLifetimes.actualPresence line 2165

    Source documentation

    Actual lifetime: ages 0,...,K-1 certain, trials K,...,K²-1, compulsory retirement at K².

    def actualPresence (K a : ℕ) : ℝ :=
…
  194. def OAI.KServer.RosterLifetimes.shortPresence line 2170

    Source documentation

    Auxiliary short lifetime: a trial on each positive age increment, compulsory retirement at K. It does not define the actual partition.

    def shortPresence (K a : ℕ) : ℝ :=
…
  195. lemma OAI.KServer.RosterLifetimes.actual_guaranteed line 2173
  196. lemma OAI.KServer.RosterLifetimes.actual_cutoff line 2176
  197. lemma OAI.KServer.RosterLifetimes.short_new line 2180
  198. lemma OAI.KServer.RosterLifetimes.short_cutoff line 2183
  199. theorem OAI.KServer.RosterLifetimes.actual_retirement_bound line 2189

    Source documentation

    The source unconditional actual-first-coverer retirement estimate, including both stochastic and compulsory terms. The factor K² is the geometric roster count proved from chronological ages, not the total history.

    theorem actual_retirement_bound (K : ℕ) (hK : 2 ≤ K) :
    1/(K:ℝ)+(K:ℝ)^2*survive (1/(K:ℝ)) (K^2-K) ≤ 49/(K:ℝ) := by
…

    Mentions: OAI.KServer.RosterLifetimes.survive

  200. theorem OAI.KServer.RosterLifetimes.short_retirement_bound line 2205

    Source documentation

    The auxiliary ramp can increase by at most this amount; its complete retirement calculation has a uniform 49/√K bound.

    theorem short_retirement_bound (K : ℕ) (hK : 2 ≤ K) :
    1/Real.sqrt K+(K:ℝ)*survive (1/Real.sqrt K) (K-1) ≤ 49/Real.sqrt K := by
…

    Mentions: OAI.KServer.RosterLifetimes.survive

  201. lemma OAI.KServer.ActualRoster.rate_range line 2235
  202. lemma OAI.KServer.ActualRoster.survival_range line 2239
  203. lemma OAI.KServer.ActualRoster.survival_antitone line 2246
  204. abbrev OAI.KServer.ActualRoster.Lifetime line 2260
  205. def OAI.KServer.ActualRoster.lifetimeLaw line 2262
  206. lemma OAI.KServer.ActualRoster.lifetime_nonneg line 2264
  207. lemma OAI.KServer.ActualRoster.lifetime_sum line 2267
  208. def OAI.KServer.ActualRoster.alive line 2274

    Source documentation

    Certain initial ages are included even on zero-weight tape outcomes; this makes deterministic coverage a pathwise property, not just an almost-sure one.

    def alive (K a : ℕ) (d : Lifetime K) : Prop := a<K ∨ a≤(d:ℕ)

    Mentions: OAI.KServer.ActualRoster.Lifetime

  209. lemma OAI.KServer.ActualRoster.alive_young line 2276
  210. lemma OAI.KServer.ActualRoster.alive_certain line 2282
  211. lemma OAI.KServer.ActualRoster.alive_probability line 2284
  212. lemma OAI.KServer.ActualRoster.alive_antitone line 2305
  213. lemma OAI.KServer.ActualRoster.death_probability line 2310
  214. lemma OAI.KServer.ActualRoster.ordinary_death_bound line 2323

    Source documentation

    Before the compulsory age, the inverse-tail tape has exactly the source hazard 1/K once independent trials have begun.

    lemma ordinary_death_bound {K a : ℕ} (hK : 1 ≤ K) (ha : a+1<K^2) :
    actualPresence K a-actualPresence K (a+1) ≤ (1/(K:ℝ))*actualPresence K a := by
…
  215. def OAI.KServer.ActualRoster.present line 2346
  216. lemma OAI.KServer.ActualRoster.present_young line 2349
  217. lemma OAI.KServer.ActualRoster.young_present line 2353
  218. def OAI.KServer.ActualRoster.covered line 2360
  219. def OAI.KServer.ActualRoster.first line 2364
  220. lemma OAI.KServer.ActualRoster.first_some_iff line 2369
  221. lemma OAI.KServer.ActualRoster.first_none_iff line 2396
  222. lemma OAI.KServer.ActualRoster.qualified_covered line 2403

    Source documentation

    Deterministic source coverage on a qualifying insertion step, including zero-weight lifetime outcomes.

    lemma qualified_covered (center : ℕ → Y) {r : ℝ} (hr : 0 < r) (hK : 0<K)
    (qualifies : ℕ → Prop) (t : ℕ) (ht : t<H) (hq : qualifies t)
    (life : Fin H → Lifetime K) (radii : Fin H → Outcome Y r) :
    ∃ i, covered center (schedule center r K qualifies (t+1)) r life radii (center t) i := by
…

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

  223. theorem OAI.KServer.ActualRoster.first_hit_estimate line 2414

    Source documentation

    Actual fixed-schedule first-hit probability under the complete finite radius tape, with the independently sampled lifetime tape fixed arbitrarily.

    theorem first_hit_estimate (center : ℕ → Y) (I : Finset ℕ) {r : ℝ} (hr : 0 < r)
    (hK : 1 ≤ K) (life : Fin H → Lifetime K) (x y : Y) (hxy : dist x y ≤ r) :
    PartitionProbabilities.probability (fun _ : Fin H => law (Y:=Y) (Real.log (1+(K:ℝ)^2)) r)
…

    Mentions: OAI.KServer.ActualRoster.Lifetime, OAI.KServer.PartitionProbabilities.probability