OAI/Combinatorics/UniformKServer/LinearProgram.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.EffectiveLP.enumerate line 11

   Source documentation

   Computable increasing-code enumeration. No finite-choice oracle.

   def enumerate {A : Type*} [Fintype A] [Encodable A] : List A :=
   …

2. def OAI.UniformKServer.EffectiveLP.index line 15
3. theorem OAI.UniformKServer.EffectiveLP.mem_enumerate line 19
4. def OAI.UniformKServer.EffectiveLP.words line 25

   Source documentation

   Exactly the finite source word-prefix set, explicitly enumerated.

   def words (n : ℕ) : ℕ → Finset (List (Fin n))
     | 0 => {[]}
     | H+1 => insert [] (Finset.univ.biUnion fun r => (words n H).image (r::·))

5. def OAI.UniformKServer.EffectiveLP.Word line 29
6. instance OAI.UniformKServer.EffectiveLP.(instance at line 30) line 30
7. instance OAI.UniformKServer.EffectiveLP.(instance at line 31) line 31
8. instance OAI.UniformKServer.EffectiveLP.(instance at line 32) line 32
9. def OAI.UniformKServer.EffectiveLP.Config line 34
10. instance OAI.UniformKServer.EffectiveLP.(instance at line 35) line 35
11. instance OAI.UniformKServer.EffectiveLP.(instance at line 36) line 36
12. instance OAI.UniformKServer.EffectiveLP.(instance at line 37) line 37
13. def OAI.UniformKServer.EffectiveLP.labels line 40

    Source documentation

    The source allowed-label set, not a relaxed transition relation.

    def labels {n k : ℕ} (c : Config n k) (r : Fin n) : Finset (Fin k) :=
    …

    Mentions: OAI.UniformKServer.EffectiveLP.Config

14. def OAI.UniformKServer.EffectiveLP.Label line 43
15. instance OAI.UniformKServer.EffectiveLP.(instance at line 44) line 44
16. instance OAI.UniformKServer.EffectiveLP.(instance at line 46) line 46
17. instance OAI.UniformKServer.EffectiveLP.(instance at line 48) line 48
18. def OAI.UniformKServer.EffectiveLP.Short line 51
19. instance OAI.UniformKServer.EffectiveLP.(instance at line 52) line 52
20. instance OAI.UniformKServer.EffectiveLP.(instance at line 53) line 53
21. instance OAI.UniformKServer.EffectiveLP.(instance at line 54) line 54
22. abbrev OAI.UniformKServer.EffectiveLP.Edge line 57

    Source comment

    A finite free variable for each displayed source p and allowed f.

    abbrev Edge (n k H : ℕ) := (_ : Short n H) × (r : Fin n) × (c : Config n k) × Label c r

    Mentions: OAI.UniformKServer.EffectiveLP.Short, OAI.UniformKServer.EffectiveLP.Config, OAI.UniformKServer.EffectiveLP.Label

23. abbrev OAI.UniformKServer.EffectiveLP.Variable line 58
24. structure OAI.UniformKServer.EffectiveLP.BoundedFlow line 60
25. def OAI.UniformKServer.EffectiveLP.toAssignment line 64
26. def OAI.UniformKServer.EffectiveLP.ofAssignment line 68
27. abbrev OAI.UniformKServer.EffectiveLP.Form.RowV line 75
28. def OAI.UniformKServer.EffectiveLP.Form.var line 77
29. def OAI.UniformKServer.EffectiveLP.Form.objective line 79
30. def OAI.UniformKServer.EffectiveLP.Form.constant line 80
31. def OAI.UniformKServer.EffectiveLP.Form.sum line 81
32. def OAI.UniformKServer.EffectiveLP.Form.eqRows line 84
33. def OAI.UniformKServer.EffectiveLP.Form.vector line 85
34. def OAI.UniformKServer.EffectiveLP.Form.recover line 87
35. theorem OAI.UniformKServer.EffectiveLP.mem_words line 91
36. theorem OAI.UniformKServer.EffectiveLP.label_injective line 107
37. def OAI.UniformKServer.EffectiveLP.step line 134
38. def OAI.UniformKServer.EffectiveLP.rootWord line 137
39. def OAI.UniformKServer.EffectiveLP.extend line 138
40. def OAI.UniformKServer.EffectiveLP.prefixNode line 141
41. abbrev OAI.UniformKServer.EffectiveLP.Row line 148
42. def OAI.UniformKServer.EffectiveLP.massRow line 150
43. def OAI.UniformKServer.EffectiveLP.flowRow line 152
44. def OAI.UniformKServer.EffectiveLP.costRow line 156
45. def OAI.UniformKServer.EffectiveLP.constraints line 162
46. def OAI.UniformKServer.EffectiveLP.Valid line 185

    Source comment

    Exact interpretation of the source constraints, over either rationals or reals.

    def Valid {n k H : ℕ} {K : Type*} [Field K] [LinearOrder K]
        (d : RationalMetric n) (u : Config n k) (F : BoundedFlow n k H K) (a : K)
        [NeZero k] : Prop :=
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.EffectiveLP.Config, OAI.UniformKServer.EffectiveLP.BoundedFlow

47. theorem OAI.UniformKServer.EffectiveLP.Form.recover_vector line 202
48. theorem OAI.UniformKServer.EffectiveLP.Form.objective_vector line 206
49. theorem OAI.UniformKServer.EffectiveLP.Form.eval_var line 212
50. theorem OAI.UniformKServer.EffectiveLP.Form.eval_objective line 217
51. theorem OAI.UniformKServer.EffectiveLP.Form.eval_constant line 221
52. theorem OAI.UniformKServer.EffectiveLP.Form.eval_sum line 227
53. theorem OAI.UniformKServer.EffectiveLP.Form.eqRows_iff line 234
54. theorem OAI.UniformKServer.EffectiveLP.satisfies_append line 247
55. theorem OAI.UniformKServer.EffectiveLP.satisfies_flatMap line 256
56. theorem OAI.UniformKServer.EffectiveLP.satisfies_singleton line 262
57. theorem OAI.UniformKServer.EffectiveLP.eval_costRow line 266
58. theorem OAI.UniformKServer.EffectiveLP.eval_if line 282
59. theorem OAI.UniformKServer.EffectiveLP.constraints_iff line 287
60. theorem OAI.UniformKServer.EffectiveLP.rational_attainment line 326