OAI/Combinatorics/UniformKServer/PiFirstHit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Chronological first-hit experiments are the actual marginal of one fixed independent tape; no product-law identity is supplied as a hypothesis.

  1. def OAI.UniformKServer.FirstHit.firstPi line 18
  2. theorem OAI.UniformKServer.FirstHit.firstPi_dep line 23
  3. theorem OAI.UniformKServer.FirstHit.pi_recurrence line 30
  4. theorem OAI.UniformKServer.FirstHit.pi_expect_first line 55