OAI/Combinatorics/UniformKServer/FiniteTable.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.FiniteTable.fallback line 11

   Source documentation

   The source's least allowed serving label, including zero marginal rows.

   def fallback {n k : ℕ} [NeZero k] (c : Config n k) (r : Fin n) : Fin k :=
   …

2. def OAI.UniformKServer.FiniteTable.next line 14
3. def OAI.UniformKServer.FiniteTable.globalFlow line 17
4. def OAI.UniformKServer.FiniteTable.charge line 24
5. def OAI.UniformKServer.FiniteTable.row line 27
6. theorem OAI.UniformKServer.FiniteTable.labels_nonempty line 31
7. theorem OAI.UniformKServer.FiniteTable.fallback_mem line 39
8. theorem OAI.UniformKServer.FiniteTable.sum_labels line 44
9. theorem OAI.UniformKServer.FiniteTable.global_valid line 49
10. theorem OAI.UniformKServer.FiniteTable.flowCost_prefix line 93
11. theorem OAI.UniformKServer.FiniteTable.flowCost_exact line 104
12. theorem OAI.UniformKServer.FiniteTable.realize_proof line 122
13. theorem OAI.UniformKServer.FiniteTable.realize line 146

    Source comment

    The exact new obligation: actual causal rows from the source finite LP, including all zero-marginal rows and zero optimum words.

    theorem realize {n k H : ℕ} [NeZero k]
        (d : RationalMetric n) (u : Config n k) (F : BoundedFlow n k H ℚ) (a : ℚ)
        (hF : EffectiveLP.Valid d u F a) :
        (∀ w r c j, 0 ≤ row F w r c j) ∧
        (∀ w r c, ∑ j, row F w r c j = 1) ∧
        (∀ w r c j, j ∉ labels c r → row F w r c j = 0) ∧
        (∀ w, w.length ≤ H →
          FiniteFlow.cost (row F) next (charge d) [] u w ≤
            a * OfflineDynamic.optRat d u.val w) := by
    …

    Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.EffectiveLP.Valid, OAI.UniformKServer.FiniteTable.row, OAI.UniformKServer.FiniteFlow.cost, OAI.UniformKServer.FiniteTable.next, OAI.UniformKServer.FiniteTable.charge, OAI.UniformKServer.OfflineDynamic.optRat