OAI/Computability/PerfectCompleteness/Sampling/FiniteListSampling.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.FiniteListSampling.uniformList line 17
  2. theorem OAI.PerfectCompleteness.FiniteListSampling.uniformList_weight_mem line 28
  3. theorem OAI.PerfectCompleteness.FiniteListSampling.probability_ge_weight line 33
  4. def OAI.PerfectCompleteness.FiniteListSampling.pairAcceptance line 41
  5. theorem OAI.PerfectCompleteness.FiniteListSampling.pairAcceptance_nonnegative line 46
  6. theorem OAI.PerfectCompleteness.FiniteListSampling.pair_weight_le_acceptance line 53
  7. theorem OAI.PerfectCompleteness.FiniteListSampling.uniform_pair_lower line 64
  8. theorem OAI.PerfectCompleteness.FiniteListSampling.bounded_uniform_pair_lower line 74
  9. theorem OAI.PerfectCompleteness.FiniteListSampling.pairAcceptance_eq_expectation line 91