OAI/Combinatorics/UniformKServer/OffsetEpoch.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.OffsetEpoch.baseLabel line 14
2. def OAI.UniformKServer.OffsetEpoch.counts line 17
3. theorem OAI.UniformKServer.OffsetEpoch.base_covers line 22
4. theorem OAI.UniformKServer.OffsetEpoch.total line 29
5. theorem OAI.UniformKServer.OffsetEpoch.forbidden line 39
6. theorem OAI.UniformKServer.OffsetEpoch.runCost_eq line 54
7. theorem OAI.UniformKServer.OffsetEpoch.construct line 93

   Source documentation

   The input is only the finite rational metric, parameters and canonical virtual tuple. No existence theorem or policy oracle appears in this result.

   theorem construct {n k : ℕ} [NeZero k] (hk2 : 2 ≤ k)
       (d : RationalMetric n) (u : Config n k) (A : ℚ) (M R : ℕ)
       (hv : OffsetLP.Valid d u A (OffsetTable.flow (H:=horizon k M) d u A) (OffsetTable.offset d u A (horizon k M)))
   …

   Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.OffsetLP.Valid, OAI.UniformKServer.OffsetTable.flow, OAI.UniformKServer.horizon, OAI.UniformKServer.OffsetTable.offset