OAI/Combinatorics/UniformKServer/AutomaticEpoch.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.AutomaticEpoch.baseLabel line 10
2. def OAI.UniformKServer.AutomaticEpoch.counts line 13
3. theorem OAI.UniformKServer.AutomaticEpoch.base_covers line 18
4. theorem OAI.UniformKServer.AutomaticEpoch.total line 25
5. theorem OAI.UniformKServer.AutomaticEpoch.forbidden line 35
6. theorem OAI.UniformKServer.AutomaticEpoch.runCost_eq line 50
7. theorem OAI.UniformKServer.AutomaticEpoch.construct line 88

   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) (M R : ℕ) (D δ : ℝ)
       (hD : 0 ≤ D) (hδ : 0 ≤ δ) (hdiam : ∀ x y, (d.distance x y : ℝ) ≤ D)
       (hsep : ∀ x y, x ≠ y → δ ≤ (d.distance x y : ℝ))
       (hcap : R * (k+1) * D ≤ (M+1) * δ) :
       ∃ hN : ∀ s r, ∑ j, counts d u (horizon k M) s r j =
           2^(AutomaticTable.bitWidth k (horizon k M)),
         ∀ (raw : List (Fin n)), EpochShadow.blockCount (k:=k) ∅ raw ≤ R →
   …

   Mentions: OAI.UniformKServer.RationalMetric, OAI.UniformKServer.AutomaticEpoch.counts, OAI.UniformKServer.horizon, OAI.UniformKServer.AutomaticTable.bitWidth, OAI.UniformKServer.EpochShadow.blockCount