OAI/Combinatorics/UniformKServer/ShortRoster.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.ShortRoster.costValue line 19

   Source documentation

   A clipped distance-to-set ramp, expressed as the minimum of all live center costs and the empty-roster cost one.

   def costValue (a : I → ℝ) (H : Finset I) : ℝ :=
   …

2. def OAI.UniformKServer.ShortRoster.retained line 25

   Source documentation

   Continue all old lifetime trials using fresh independent keep bits; compulsory cutoffs apply on the same age increment. The new entry's ramp value is supplied separately so duplicates of physical centers are harmless.

   def retained (inc kill : I → Prop) (H : Finset I) (τ : I → Bool) : Finset I :=
   …

3. def OAI.UniformKServer.ShortRoster.editedValue line 28
4. def OAI.UniformKServer.ShortRoster.fresh line 31
5. theorem OAI.UniformKServer.ShortRoster.cost_bounds line 35
6. theorem OAI.UniformKServer.ShortRoster.cost_le line 47
7. theorem OAI.UniformKServer.ShortRoster.le_cost line 51
8. theorem OAI.UniformKServer.ShortRoster.cost_witness line 61
9. theorem OAI.UniformKServer.ShortRoster.cost_close line 70
10. theorem OAI.UniformKServer.ShortRoster.edited_bounds line 91
11. theorem OAI.UniformKServer.ShortRoster.edited_le_retained line 97
12. theorem OAI.UniformKServer.ShortRoster.conditional_increase line 102
13. structure OAI.UniformKServer.ShortRoster.State line 164

    Source documentation

    The finite random experiment is part of the constructed state, not an assumed randomized-policy interface.

    structure State (I : Type) where
    …

14. def OAI.UniformKServer.ShortRoster.ramp line 174
15. def OAI.UniformKServer.ShortRoster.State.parameter line 176
16. def OAI.UniformKServer.ShortRoster.State.Valid line 179
17. def OAI.UniformKServer.ShortRoster.State.next line 185
18. theorem OAI.UniformKServer.ShortRoster.mean_increase line 200
19. theorem OAI.UniformKServer.ShortRoster.ramp_bounds line 254
20. theorem OAI.UniformKServer.ShortRoster.ramp_zero line 258
21. theorem OAI.UniformKServer.ShortRoster.ramp_one line 262
22. theorem OAI.UniformKServer.ShortRoster.ramp_lip line 268
23. theorem OAI.UniformKServer.ShortRoster.cost_insert line 279
24. theorem OAI.UniformKServer.ShortRoster.parameter_bounds line 287
25. theorem OAI.UniformKServer.ShortRoster.parameter_lip line 296
26. theorem OAI.UniformKServer.ShortRoster.next_parameter line 309
27. theorem OAI.UniformKServer.ShortRoster.parameter_unit_drop line 330
28. theorem OAI.UniformKServer.ShortRoster.parameter_far line 365
29. theorem OAI.UniformKServer.ShortRoster.parameter_increase line 390
30. theorem OAI.UniformKServer.ShortRoster.short_edit line 424

    Source documentation

    Exact source short-roster edit, with the finite lifetime experiment constructed by State.next. No drift or gain hypothesis is present.

    theorem short_edit (D : State I) (S : Finset I) (c : I → X) (r : ℝ) (hr : 0 < r)
        (K : ℕ) (_hK : 0 < K) (q : ℝ) (hq : q ∈ Set.Icc (0:ℝ) 1) (n : I)
        (hD : D.Valid S c r K q) (_hn : ∀ i ∈ S, i < n)
        (htest : ∀ i ∈ young S c r K, r/2 < dist (c n) (c i)) :
        TierPilot.Edit r (q+(K:ℝ)*(1-q)^(K-1)) (c n)
          (D.parameter c r) ((D.next S c r K q hq n).parameter c r) := by
    …

    Mentions: OAI.UniformKServer.ShortRoster.State, OAI.UniformKServer.TierPilot.Edit