OAI/Combinatorics/UniformKServer/CausalTier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Causality of the realized live roster and its labeled key, with the entire independent random tape held fixed.

  1. lemma OAI.UniformKServer.CausalRosters.active_congr line 19
  2. lemma OAI.UniformKServer.CausalRosters.compulsory_congr line 26
  3. lemma OAI.UniformKServer.CausalRosters.live_subset line 33
  4. lemma OAI.UniformKServer.CausalRosters.live_inputs line 49
  5. lemma OAI.UniformKServer.CausalRosters.key_inputs line 75
  6. lemma OAI.UniformKServer.CausalRosters.labeled_inputs line 89