OAI/Combinatorics/UniformKServer/FiniteFlow.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniformKServer.FiniteFlow.Data line 8
2. structure OAI.UniformKServer.FiniteFlow.Valid line 12
3. def OAI.UniformKServer.FiniteFlow.row line 24

   Source documentation

   All rows are explicitly defined, even outside the construction horizon.

   def row (F : Data R C J) (fallback : C → R → J) (H : ℕ)
       (w : List R) (r : R) (c : C) (j : J) : ℚ :=
   …

   Mentions: OAI.UniformKServer.FiniteFlow.Data

4. def OAI.UniformKServer.FiniteFlow.cost line 29
5. def OAI.UniformKServer.FiniteFlow.flowCost line 34
6. theorem OAI.UniformKServer.FiniteFlow.zero_flow line 48
7. theorem OAI.UniformKServer.FiniteFlow.mass_row line 55
8. theorem OAI.UniformKServer.FiniteFlow.row_nonneg line 62
9. theorem OAI.UniformKServer.FiniteFlow.row_sum line 69
10. theorem OAI.UniformKServer.FiniteFlow.row_support line 76
11. theorem OAI.UniformKServer.FiniteFlow.inflow_average line 86
12. theorem OAI.UniformKServer.FiniteFlow.cost_average line 99
13. theorem OAI.UniformKServer.FiniteFlow.realization line 118

    Source documentation

    The precise finite flow realization obligation.

    theorem realization (F : Data R C J) (T : C → R → J → C)
        (allowed : C → R → J → Prop) (initial : C) (H : ℕ)
        (fallback : C → R → J) (hfallback : ∀ c r, allowed c r (fallback c r))
        (hF : Valid F T allowed initial H) :
        (∀ w r c j, 0 ≤ row F fallback H w r c j) ∧
        (∀ w r c, ∑ j, row F fallback H w r c j = 1) ∧
        (∀ w r c j, ¬allowed c r j → row F fallback H w r c j = 0) ∧
        (∀ d rs, rs.length ≤ H → cost (row F fallback H) T d [] initial rs = flowCost F d [] rs) := by
    …

    Mentions: OAI.UniformKServer.FiniteFlow.Data, OAI.UniformKServer.initial, OAI.UniformKServer.FiniteFlow.Valid, OAI.UniformKServer.FiniteFlow.row, OAI.UniformKServer.FiniteFlow.cost, OAI.UniformKServer.FiniteFlow.flowCost