OAI/Combinatorics/UniformKServer/EpochExpectation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniformKServer.EpochExpectation.BState line 10
  2. def OAI.UniformKServer.EpochExpectation.next line 12
  3. def OAI.UniformKServer.EpochExpectation.charge line 15
  4. def OAI.UniformKServer.EpochExpectation.selector line 18
  5. def OAI.UniformKServer.EpochExpectation.extend line 22
  6. def OAI.UniformKServer.EpochExpectation.epochTrace line 27

    Source documentation

    Exact finite product of the fresh bits assigned to the deterministic kept word. Extra shadow bits after a switch are analytical only.

    def epochTrace {n k b : ℕ} (hk : 0 < k) (M : ℕ)
    (N : BState n k → Fin n → Fin k → ℕ) (hN : ∀ s r, ∑ j, N s r j = 2^b)
    (u : Configuration n k) (raw : List (Fin n))
    (coins : Fin (keptTail M (initial u) raw).length → Fin b → Bool) : History n k :=
…

    Mentions: OAI.UniformKServer.EpochExpectation.BState, OAI.UniformKServer.Configuration, OAI.UniformKServer.initial, OAI.UniformKServer.History

  7. theorem OAI.UniformKServer.EpochExpectation.selector_lazy line 33
  8. theorem OAI.UniformKServer.EpochExpectation.shadow_cost line 44
  9. theorem OAI.UniformKServer.EpochExpectation.shadow_full line 64
  10. theorem OAI.UniformKServer.EpochExpectation.kept_sublist line 74
  11. theorem OAI.UniformKServer.EpochExpectation.mean_mono line 84
  12. theorem OAI.UniformKServer.EpochExpectation.mean_mul line 88
  13. theorem OAI.UniformKServer.EpochExpectation.comparison line 95