Rosters.lean`

76 declarations, 0 contain sorry, 0 declared as axioms

Heavy keys of the constructed finite schedule and their exact full-input spatial estimate; label reuse does not impose or assume a probability law.

lemma OAI.KServer.ActualRoster.probability_mono line 13
lemma OAI.KServer.ActualRoster.separates_iff_cover line 28
lemma OAI.KServer.ActualRoster.hit_iff_cover line 42

theorem OAI.KServer.ActualRoster.first_ne_iff line 50

Source documentation

The first-hit event is literally the event that the actual two chronological keys differ, including absence on either or both sides.

theorem first_ne_iff (center : ℕ → Y) (I : Finset ℕ) (r : ℝ)
    (life : Fin H → Lifetime K) (rad : Fin H → Outcome Y r) (x y : Y) :
    first center I r life rad x ≠ first center I r life rad y ↔
      firstSeparation (fun j d=>present center I r life j ∧ hit r (center j) x y d)
        (fun j d=>present center I r life j ∧ separates r (center j) x y d) rad := by
…

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

theorem OAI.KServer.ActualRoster.spatial_bound line 106

Source documentation

Uniform-in-history spatial bound for the actual fixed-lifetime keys.

theorem spatial_bound (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

theorem OAI.KServer.ActualRoster.averaged_spatial_bound line 121

Source documentation

Averaging independent lifetimes preserves the bound. No conditional independence of any adaptive allocation state is used.

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

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

def OAI.KServer.HeavyKeys.hits line 157
def OAI.KServer.HeavyKeys.centerKey line 160
lemma OAI.KServer.HeavyKeys.hit_unique line 163
lemma OAI.KServer.HeavyKeys.centerKey_some line 174
lemma OAI.KServer.HeavyKeys.centerKey_none line 191
def OAI.KServer.HeavyKeys.candidates line 203
lemma OAI.KServer.HeavyKeys.candidate_unique line 206
lemma OAI.KServer.HeavyKeys.ne_separates line 223
lemma OAI.KServer.HeavyKeys.cylinder line 243
def OAI.KServer.HeavyKeys.key line 260
theorem OAI.KServer.HeavyKeys.spatial_bound line 268
Source documentation
The source's d/(4r) bound for the actual heavy key, conditioned only on full input, with deterministic birth times and a genuine product radius tape.
```
theorem spatial_bound (s : Configuration k Y) (law : FiniteDistribution (Fin H → Y))
    {r : ℝ} (hr : 0<r) (γ δ : ℝ) (σ : Fin H → Y) (t : ℕ) (x y : Y)
    (hxy : 4*dist x y<r) :
    probability (fun _ : Fin H=>FiniteUniform.law (Y:=Y) r)
…
```
Mentions: OAI.KServer.Configuration, OAI.KServer.FiniteDistribution, OAI.KServer.FiniteUniform.law
lemma OAI.KServer.RosterExpectation.product_pushforward line 322
lemma OAI.KServer.RosterExpectation.product_marginal line 344
def OAI.KServer.RosterExpectation.bernoulli line 359
Source documentation
Bernoulli weights, with true denoting that the record survives.
```
def bernoulli (q : ℝ) (b : Bool) : ℝ := if b then q else 1-q
```
lemma OAI.KServer.RosterExpectation.bernoulli_sum line 360
lemma OAI.KServer.RosterExpectation.bernoulli_nonneg line 362
lemma OAI.KServer.RosterExpectation.bernoulli_thinning line 366
lemma OAI.KServer.RosterExpectation.paired_expectation line 381
def OAI.KServer.RosterExpectation.minimum line 399
Source documentation
Finite minimum of the clipped ramps, with value 1 for an empty roster.
```
def minimum (v : I → ℝ) (a : I → Bool) : ℝ :=
…
```
lemma OAI.KServer.RosterExpectation.minimum_le_one line 401
lemma OAI.KServer.RosterExpectation.minimum_le line 403
lemma OAI.KServer.RosterExpectation.le_minimum line 405
lemma OAI.KServer.RosterExpectation.minimum_nonneg line 413
lemma OAI.KServer.RosterExpectation.minimum_cases line 415
def OAI.KServer.RosterExpectation.profile line 424
Source documentation
Expected ramp under independent survival probabilities.
```
def profile (q v : I → ℝ) : ℝ := ∑ a,productWeight (fun i=>bernoulli (q i)) a*minimum v a
```
Mentions: OAI.KServer.RosterExpectation.bernoulli, OAI.KServer.RosterExpectation.minimum
lemma OAI.KServer.RosterExpectation.profile_bounds line 425
lemma OAI.KServer.RosterExpectation.profile_thinning line 434
Source documentation
Continuing independent trials gives exactly the new survival marginal.
```
lemma profile_thinning (q d v : I → ℝ) :
    profile (fun i=>q i*(1-d i)) v=
      ∑ a,productWeight (fun i=>bernoulli (q i)) a*
        ∑ b,productWeight (fun i=>bernoulli (d i)) b*minimum v (fun i=>a i && !b i) := by
…
```
Mentions: OAI.KServer.RosterExpectation.profile, OAI.KServer.RosterExpectation.bernoulli, OAI.KServer.RosterExpectation.minimum
lemma OAI.KServer.RosterExpectation.minimum_retirement line 441

lemma OAI.KServer.RosterExpectation.conditional_retirement line 453

Source documentation

The selected old nearest survivor is tested by a fresh independent trial. Compulsory deaths are charged without conditioning on survival.

lemma conditional_retirement {v d : I → ℝ} (hv : ∀ i,0 ≤ v i)
    (hd : ∀ i,d i∈Set.Icc 0 1) (a : I → Bool) {α : ℝ} (hα : 0 ≤ α)
    (C : Finset I) (hnc : ∀ i,i∉C → d i ≤ α) :
    (∑ b,productWeight (fun i=>bernoulli (d i)) b*minimum v (fun i=>a i && !b i))-
      minimum v a ≤ α+∑ i∈C,if a i then 1 else 0 := by
…

Mentions: OAI.KServer.RosterExpectation.bernoulli, OAI.KServer.RosterExpectation.minimum

lemma OAI.KServer.RosterExpectation.profile_retirement_bound line 490
lemma OAI.KServer.RosterExpectation.minimum_force_le line 512
lemma OAI.KServer.RosterExpectation.forced_expectation line 521
lemma OAI.KServer.RosterExpectation.profile_insertion_le line 538
lemma OAI.KServer.RosterExpectation.weight_zero_at line 546
lemma OAI.KServer.RosterExpectation.profile_one line 549
lemma OAI.KServer.RosterExpectation.profile_zero_of_certain line 565
lemma OAI.KServer.RosterExpectation.minimum_lipschitz line 574
lemma OAI.KServer.RosterExpectation.profile_lipschitz line 585
lemma OAI.KServer.RosterExpectation.minimum_cut line 601
lemma OAI.KServer.RosterExpectation.profile_cut line 614
lemma OAI.KServer.RosterExpectation.profile_irrelevant line 627

lemma OAI.KServer.RosterExpectation.profile_retirement_local line 635

Source documentation

Only compulsory candidates whose ramps are below one need be counted.

lemma profile_retirement_local {q d v : I → ℝ} (hq : ∀ i,q i∈Set.Icc 0 1)
    (hd : ∀ i,d i∈Set.Icc 0 1) (hv : ∀ i,v i∈Set.Icc 0 1) {α : ℝ} (hα : 0 ≤ α)
    (C : Finset I) (hnc : ∀ i,i∉C → v i<1 → d i ≤ α) :
    profile (fun i=>q i*(1-d i)) v-profile q v ≤ α+∑ i∈C,q i := by
…

Mentions: OAI.KServer.RosterExpectation.profile

lemma OAI.KServer.RosterExpectation.profile_values_congr line 658
Source documentation
Coordinates with zero presence probability carry no information about an expected profile. This is the exact causality fact for unused ordinals.
```
lemma profile_values_congr {q v w : I → ℝ}
    (h : ∀ i,q i≠0 → v i=w i) : profile q v=profile q w := by
…
```
Mentions: OAI.KServer.RosterExpectation.profile
def OAI.KServer.ShortRoster.ramp line 693
Source documentation
Exact increasing clipped ramp on [1/8,1/4].
```
def ramp (u : ℝ) : ℝ := min 1 (max 0 (8*u-1))
```
lemma OAI.KServer.ShortRoster.ramp_bounds line 694
lemma OAI.KServer.ShortRoster.ramp_zero line 696
lemma OAI.KServer.ShortRoster.ramp_one line 698
lemma OAI.KServer.ShortRoster.ramp_lipschitz line 700
lemma OAI.KServer.ShortRoster.rate_bounds line 705
lemma OAI.KServer.ShortRoster.short_bounds line 708
def OAI.KServer.ShortRoster.probability line 716
def OAI.KServer.ShortRoster.values line 719
def OAI.KServer.ShortRoster.profile line 721
lemma OAI.KServer.ShortRoster.probability_bounds line 724
lemma OAI.KServer.ShortRoster.profile_bounds line 730
lemma OAI.KServer.ShortRoster.values_lipschitz line 734
lemma OAI.KServer.ShortRoster.profile_lipschitz line 743
def OAI.KServer.ShortRoster.death line 750
Source documentation
Death trials for one actual age increment, including the compulsory cutoff. Already absent records are assigned probability zero.
```
def death (request : ℕ → Y) (r : ℝ) (K : ℕ) (S : Finset ℕ) (t : Fin H) (i : Fin H) : ℝ :=
…
```
lemma OAI.KServer.ShortRoster.death_bounds line 754
lemma OAI.KServer.ShortRoster.probability_insert line 762
lemma OAI.KServer.ShortRoster.profile_unit_drop line 789
lemma OAI.KServer.ShortRoster.values_lt_one line 814
def OAI.KServer.ShortRoster.compulsory line 823
Source documentation
Compulsory candidates that can actually affect the ramp at a test point.
```
def compulsory (request : ℕ → Y) (r : ℝ) (K : ℕ) (S : Finset ℕ) (p : Y) : Finset (Fin H) :=
…
```
lemma OAI.KServer.ShortRoster.compulsory_count line 826
lemma OAI.KServer.ShortRoster.compulsory_mass line 853

theorem OAI.KServer.ShortRoster.profile_error line 872

Source documentation

The exact short-roster retirement bound, including compulsory deaths, is uniform in the number of chronological records and the horizon.

theorem profile_error (request : ℕ → Y) {r : ℝ} (hr : 0<r) {K : ℕ} (hK : 2 ≤ K)
    (S : Finset ℕ) (t : Fin H) (hbefore : ∀ i∈S,i<(t:ℕ)) (p : Y) :
    profile (H := H) request r K (insert (t:ℕ) S) p-profile (H := H) request r K S p ≤ 49/Real.sqrt K := by
…

Mentions: OAI.KServer.ShortRoster.profile

lemma OAI.KServer.ShortRoster.profile_outside line 909
lemma OAI.KServer.ShortRoster.profile_increase_support line 926
lemma OAI.KServer.ShortRoster.age_congr line 940
lemma OAI.KServer.ShortRoster.profile_congr line 949