OAI/Combinatorics/UniformKServer/Fallback.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniformKServer.Fallback.State line 9
2. def OAI.UniformKServer.Fallback.pick line 13
3. def OAI.UniformKServer.Fallback.coverers line 16
4. def OAI.UniformKServer.Fallback.choose line 19
5. def OAI.UniformKServer.Fallback.step line 23
6. def OAI.UniformKServer.Fallback.trace line 27
7. def OAI.UniformKServer.Fallback.run line 31
8. def OAI.UniformKServer.Fallback.Valid line 37

   Source documentation

   A raw nonendpoint portion has at most k distinct requested points. Marks are a subset of the points already seen in that same raw block.

   def Valid {n k : ℕ} (s : State n k) (S : Finset (Fin n)) : Prop :=
   …

   Mentions: OAI.UniformKServer.Fallback.State

9. theorem OAI.UniformKServer.Fallback.pick_mem line 41
10. theorem OAI.UniformKServer.Fallback.mem_coverers line 46
11. theorem OAI.UniformKServer.Fallback.misses_card_lt line 49
12. theorem OAI.UniformKServer.Fallback.free_nonempty line 63
13. theorem OAI.UniformKServer.Fallback.choice_hit_or_free line 75
14. theorem OAI.UniformKServer.Fallback.updated_injective line 85
15. theorem OAI.UniformKServer.Fallback.step_guarantee line 116

    Source documentation

    Source Lemma fallback: the exact nonendpoint marking rule is feasible.

    theorem step_guarantee {n k : ℕ} (hk : 0 < k) (s : State n k)
        (S : Finset (Fin n)) (hv : Valid s S) (r : Fin n) (hr : r ∈ S) :
        Valid (step hk s r) S ∧
        (∀ j ∈ s.marked, (step hk s r).position j = s.position j) := by
    …

    Mentions: OAI.UniformKServer.Fallback.State, OAI.UniformKServer.Fallback.Valid, OAI.UniformKServer.Fallback.step

16. theorem OAI.UniformKServer.Fallback.step_cost line 139
17. theorem OAI.UniformKServer.Fallback.nonendpoint_cost line 157

    Source documentation

    Source Lemma fallback: first appearances cost at most kD, independently of their number of repetitions. Empty and truncated portions are included.

    theorem nonendpoint_cost {n k : ℕ} (hk : 0 < k) (d : RationalMetric n)
        (D : ℝ) (hD : 0 ≤ D) (hdiam : ∀ x y, (d.distance x y : ℝ) ≤ D)
        (s : State n k) (S : Finset (Fin n)) (hv : Valid s S)
        (w : List (Fin n)) (hw : ∀ r ∈ w, r ∈ S) :
        Valid (run hk s w) S ∧ (trace hk s w).map Prod.fst = w ∧
        costAlong d s.position (trace hk s w) ≤ ((k : ℝ) - s.marked.card) * D := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Fallback.State, OAI.UniformKServer.Fallback.Valid, OAI.UniformKServer.Fallback.run, OAI.UniformKServer.Fallback.trace, OAI.UniformKServer.costAlong

18. theorem OAI.UniformKServer.cost_nonneg line 182
19. theorem OAI.UniformKServer.requests_of_small_cost line 189
20. theorem OAI.UniformKServer.completed_block_cost line 218

    Source documentation

    Source Proposition suffix: every completed raw block forces at least one positive move even from repeated initial positions.

    theorem completed_block_cost {n k : ℕ} (d : RationalMetric n)
        (δ : ℝ) (_ : 0 < δ)
        (hsep : ∀ x y, x ≠ y → δ ≤ (d.distance x y : ℝ))
        (s : Configuration n k) (h : History n k)
        (hdistinct : k < (h.map Prod.fst).toFinset.card) :
        δ ≤ costAlong d s h := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.History, OAI.UniformKServer.costAlong

21. structure OAI.UniformKServer.Fallback.RawState line 238
22. def OAI.UniformKServer.Fallback.isEndpoint line 243
23. instance OAI.UniformKServer.Fallback.(instance at line 245) line 245
24. def OAI.UniformKServer.Fallback.rawChoice line 248
25. def OAI.UniformKServer.Fallback.rawStep line 252
26. def OAI.UniformKServer.Fallback.rawTrace line 257
27. def OAI.UniformKServer.Fallback.rawRun line 261
28. def OAI.UniformKServer.Fallback.portions line 265
29. theorem OAI.UniformKServer.Fallback.endpoint_injective line 269
30. theorem OAI.UniformKServer.Fallback.raw_step_valid line 297
31. theorem OAI.UniformKServer.Fallback.raw_step_position line 309
32. def OAI.UniformKServer.Fallback.ledger line 316

    Source documentation

    Marked points pay the unfinished part of the current block; completed blocks pay their endpoint as well. This potential prevents a charge per raw request, even when an epoch is arbitrarily long.

    def ledger {n k : ℕ} (D : ℝ) (s : RawState n k) : ℝ :=
    …

    Mentions: OAI.UniformKServer.Fallback.RawState

33. theorem OAI.UniformKServer.Fallback.raw_step_cost line 319
34. theorem OAI.UniformKServer.Fallback.raw_run_ledger line 338
35. theorem OAI.UniformKServer.Fallback.ledger_le_portions line 357
36. theorem OAI.UniformKServer.Fallback.raw_fallback_bound line 376

    Source documentation

    The literal marking fallback of Section 03, including raw block endpoints, an inherited pre-switch raw block, and any finite truncation.

    theorem raw_fallback_bound {n k : ℕ} (hk : 0 < k) (d : RationalMetric n)
        (D : ℝ) (hD : 0 ≤ D) (hdiam : ∀ x y, (d.distance x y : ℝ) ≤ D)
        (c : Configuration n k) (hc : Function.Injective c)
        (seen : Finset (Fin n)) (hs : seen.card ≤ k)
        (w : List (Fin n)) (R : ℕ)
        (hR : portions (rawRun hk ⟨⟨c,∅⟩,seen,0⟩ w) ≤ R) :
        Valid (rawRun hk ⟨⟨c,∅⟩,seen,0⟩ w).marking
          (rawRun hk ⟨⟨c,∅⟩,seen,0⟩ w).seen ∧
        (rawTrace hk ⟨⟨c,∅⟩,seen,0⟩ w).map Prod.fst = w ∧
        costAlong d c (rawTrace hk ⟨⟨c,∅⟩,seen,0⟩ w) ≤ R * (k+1) * D := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.Configuration, OAI.UniformKServer.Fallback.portions, OAI.UniformKServer.Fallback.rawRun, OAI.UniformKServer.Fallback.Valid, OAI.UniformKServer.Fallback.rawTrace, OAI.UniformKServer.costAlong