OAI/Combinatorics/UniformKServer/EpochShadow.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniformKServer.EpochShadow.Selector line 10
2. def OAI.UniformKServer.EpochShadow.StronglyLazy line 12
3. def OAI.UniformKServer.EpochShadow.shadowTrace line 16
4. def OAI.UniformKServer.EpochShadow.bookStep line 21
5. def OAI.UniformKServer.EpochShadow.blockCount line 25

   Source documentation

   Number of portions, including an inherited nonempty raw block.

   def blockCount {n k : ℕ} : Finset (Fin n) → List (Fin n) → ℕ
     | seen, [] => if seen.Nonempty then 1 else 0
     | seen, r :: w => (if k < (insert r seen).card then 1 else 0) +
         blockCount (k:=k) (bookStep (k:=k) seen r) w

   Mentions: OAI.UniformKServer.EpochShadow.bookStep

6. def OAI.UniformKServer.EpochShadow.keptTail line 30
7. def OAI.UniformKServer.EpochShadow.nextEntry line 35
8. def OAI.UniformKServer.EpochShadow.trace line 41

   Source documentation

   The literal one-epoch virtual routine. The deterministic filter continues independently through fallback; its discarded final state has no effect on service. Its full kept word is provided separately by keptTail.

   def trace {n k : ℕ} (hk : 0 < k) (M : ℕ) (T : Selector n k) :
       FilterState n k → Entry n k → Finset (Fin n) → List (Fin n) → History n k
     | _, _, _, [] => []
     | f, e, seen, r :: w =>
         let seen' := bookStep (k:=k) seen r
   …

   Mentions: OAI.UniformKServer.EpochShadow.Selector, OAI.UniformKServer.FilterState, OAI.UniformKServer.Entry, OAI.UniformKServer.History, OAI.UniformKServer.EpochShadow.bookStep

9. theorem OAI.UniformKServer.EpochShadow.raw_count line 58
10. theorem OAI.UniformKServer.EpochShadow.book_card line 68
11. theorem OAI.UniformKServer.EpochShadow.block_tail_le line 75
12. theorem OAI.UniformKServer.EpochShadow.kept_tail_snoc line 80
13. theorem OAI.UniformKServer.EpochShadow.kept_tail_full line 90
14. theorem OAI.UniformKServer.EpochShadow.next_lazy line 94
15. theorem OAI.UniformKServer.EpochShadow.next_cost line 109
16. theorem OAI.UniformKServer.EpochShadow.fallback_bound line 120
17. theorem OAI.UniformKServer.EpochShadow.trace_ledger line 134

    Source documentation

    Paying for fallback by an already accumulated unconditioned shadow prefix; the comparison never conditions on the event of reaching the cap.

    theorem trace_ledger {n k : ℕ} (hk : 0 < k) (d : RationalMetric n)
        (T : Selector n k) (hT : StronglyLazy T) (u : Configuration n k)
        (hu : Function.Injective u) (M R : ℕ) (D δ : ℝ)
        (hD : 0 ≤ D) (hδ : 0 ≤ δ)
        (hdiam : ∀ x y, (d.distance x y : ℝ) ≤ D)
        (hsep : ∀ x y, x ≠ y → δ ≤ (d.distance x y : ℝ))
        (hcap : R * (k+1) * D ≤ (M+1) * δ)
        (raw : List (Fin n)) (f : FilterState n k) (e : Entry n k)
        (seen : Finset (Fin n)) (paid : ℝ)
        (hf : Represents M u f) (hp : LazyPath u f.kept e) (hm : e.moves ≤ M)
        (hs : seen.card ≤ k) (hR : blockCount (k:=k) seen raw ≤ R)
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.EpochShadow.Selector, OAI.UniformKServer.EpochShadow.StronglyLazy, OAI.UniformKServer.Configuration, OAI.UniformKServer.FilterState, OAI.UniformKServer.Entry, OAI.UniformKServer.Represents, OAI.UniformKServer.LazyPath, OAI.UniformKServer.EpochShadow.blockCount

18. theorem OAI.UniformKServer.EpochShadow.epoch_virtual_bound line 222
19. theorem OAI.UniformKServer.EpochShadow.epoch_actual_bound line 238