OAI/Combinatorics/UniformKServer/OffsetSuffix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.OffsetSuffix.cost_nonneg line 14
2. abbrev OAI.UniformKServer.OffsetSuffix.Tape line 21
3. def OAI.UniformKServer.OffsetSuffix.epochTrace line 24
4. def OAI.UniformKServer.OffsetSuffix.expected line 33

   Source documentation

   Independent unbiased tapes are sampled at consecutive epochs. The actual entering configuration is retained as random state, never reset to u.

   noncomputable def expected {n k : ℕ} [NeZero k] (d : RationalMetric n) (u : Config n k) (A : ℚ)
       (M : ℕ)
       (hv : OffsetLP.Valid d u A (OffsetTable.flow (H:=horizon k M) d u A) (OffsetTable.offset d u A (horizon k M))) : Configuration n k → List (List (Fin n)) → ℝ
   …

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

5. theorem OAI.UniformKServer.OffsetSuffix.epoch_sum line 41
6. theorem OAI.UniformKServer.OffsetSuffix.suffix line 82

   Source documentation

   The offset is paid once per completed epoch, not once per kept request.

   theorem suffix {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