OAI/Combinatorics/UniformKServer/Epochs.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniformKServer.Entry line 7
2. def OAI.UniformKServer.Covers line 11
3. instance OAI.UniformKServer.(instance at line 12) line 12
4. def OAI.UniformKServer.treeBudget line 16

   Source documentation

   Number of nodes in the full k-ary tree of depth m.

   def treeBudget (k : ℕ) : ℕ → ℕ
     | 0 => 1
     | m + 1 => 1 + k * treeBudget k m

5. theorem OAI.UniformKServer.treeBudget_zero line 20
6. theorem OAI.UniformKServer.treeBudget_succ line 21
7. theorem OAI.UniformKServer.treeBudget_pos line 24
8. def OAI.UniformKServer.expand line 27
9. def OAI.UniformKServer.weight line 33
10. def OAI.UniformKServer.mass line 35
11. def OAI.UniformKServer.births line 38
12. def OAI.UniformKServer.futureMass line 41
13. structure OAI.UniformKServer.FilterState line 44
14. def OAI.UniformKServer.step line 49
15. def OAI.UniformKServer.initial line 55
16. def OAI.UniformKServer.runFilter line 58
17. def OAI.UniformKServer.horizon line 62

    Source documentation

    The exact source horizon H.

    def horizon (k M : ℕ) : ℕ := ∑ i ∈ Finset.range (M+1), k^i

18. theorem OAI.UniformKServer.treeBudget_eq_horizon line 64
19. theorem OAI.UniformKServer.mass_nil line 74
20. theorem OAI.UniformKServer.mass_cons line 75
21. theorem OAI.UniformKServer.mass_append line 78
22. theorem OAI.UniformKServer.length_le_mass line 81
23. theorem OAI.UniformKServer.expand_valid line 90
24. theorem OAI.UniformKServer.mass_expand line 101
25. theorem OAI.UniformKServer.futureMass_add_length line 113
26. theorem OAI.UniformKServer.futureMass_expand line 123
27. def OAI.UniformKServer.misses line 138
28. theorem OAI.UniformKServer.misses_zero_iff line 141
29. theorem OAI.UniformKServer.mass_expansion line 148
30. theorem OAI.UniformKServer.futureMass_append line 163
31. theorem OAI.UniformKServer.futureMass_expansion line 166
32. def OAI.UniformKServer.Good line 181
33. theorem OAI.UniformKServer.step_good line 186
34. theorem OAI.UniformKServer.runFilter_good line 207
35. theorem OAI.UniformKServer.filter_bounds line 230

    Source documentation

    Source Lemma lem:filter: all created entries, the live list, and the kept word are bounded by H, for every raw finite prefix, even when the list empties. The deterministic filter and bound do not inspect any random online trajectory.

    theorem filter_bounds {n k : ℕ} (M : ℕ) (u : Configuration n k)
        (raw : List (Fin n)) :
        let s := runFilter M u raw
    …

    Mentions: OAI.UniformKServer.Configuration, OAI.UniformKServer.runFilter

36. def OAI.UniformKServer.LazyStep line 243

    Source documentation

    The source's strongly lazy rule: a hit changes nothing; a miss chooses exactly one label and counts one positive move.

    def LazyStep {n k : ℕ} (e : Entry n k) (r : Fin n) (e' : Entry n k) : Prop :=
    …

    Mentions: OAI.UniformKServer.Entry

37. inductive OAI.UniformKServer.LazyPath line 248

    Source documentation

    Endpoints of complete strongly lazy paths, with no cap imposed in the relation.

    inductive LazyPath {n k : ℕ} (u : Configuration n k) :
        List (Fin n) → Entry n k → Prop
      | nil : LazyPath u [] ⟨u, 0⟩
      | snoc {w : List (Fin n)} {e e' : Entry n k} {r : Fin n} :
          LazyPath u w e → LazyStep e r e' → LazyPath u (w ++ [r]) e'

    Mentions: OAI.UniformKServer.Configuration, OAI.UniformKServer.Entry, OAI.UniformKServer.LazyStep

38. theorem OAI.UniformKServer.lazyPath_nil_iff line 254
39. theorem OAI.UniformKServer.lazyPath_snoc_iff line 265
40. theorem OAI.UniformKServer.lazyStep_moves_mono line 280
41. theorem OAI.UniformKServer.mem_expand_iff line 288
42. def OAI.UniformKServer.Represents line 310

    Source documentation

    The representation invariant retains all capped paths, not just paths with positive probability under a particular table.

    def Represents {n k : ℕ} (M : ℕ) (u : Configuration n k)
        (s : FilterState n k) : Prop :=
    …

    Mentions: OAI.UniformKServer.Configuration, OAI.UniformKServer.FilterState

43. theorem OAI.UniformKServer.initial_represents line 314
44. theorem OAI.UniformKServer.step_represents line 320
45. theorem OAI.UniformKServer.filter_represents line 339
46. theorem OAI.UniformKServer.lazyStep_injective line 349
47. theorem OAI.UniformKServer.lazyPath_injective line 371
48. theorem OAI.UniformKServer.universal_filter line 379

    Source documentation

    Full deterministic content of the source's Universal Filter lemma.

    theorem universal_filter {n k : ℕ} (M : ℕ) (u : Configuration n k)
        (hu : Function.Injective u) (raw : List (Fin n)) :
        let s := runFilter M u raw
    …

    Mentions: OAI.UniformKServer.Configuration, OAI.UniformKServer.runFilter