OAI/Computability/PerfectCompleteness/Sampling/CompletionProbability.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CompletionProbability.Illegal line 18
  2. def OAI.PerfectCompleteness.CompletionProbability.uniformProbability line 20
  3. theorem OAI.PerfectCompleteness.CompletionProbability.card_illegal line 23
  4. def OAI.PerfectCompleteness.CompletionProbability.rotate line 27
  5. def OAI.PerfectCompleteness.CompletionProbability.rotateAll line 34
  6. def OAI.PerfectCompleteness.CompletionProbability.sample line 38
  7. theorem OAI.PerfectCompleteness.CompletionProbability.sample_legal line 42
  8. theorem OAI.PerfectCompleteness.CompletionProbability.sample_exact_two line 49
  9. def OAI.PerfectCompleteness.CompletionProbability.seedEquiv line 56
  10. theorem OAI.PerfectCompleteness.CompletionProbability.sample_illegal line 63
  11. theorem OAI.PerfectCompleteness.CompletionProbability.sample_event_card line 69
  12. theorem OAI.PerfectCompleteness.CompletionProbability.sample_probability line 77
  13. theorem OAI.PerfectCompleteness.CompletionProbability.residual_fiber_le_two line 84
  14. theorem OAI.PerfectCompleteness.CompletionProbability.residual_fiber_card line 95
  15. theorem OAI.PerfectCompleteness.CompletionProbability.sample_probability_residual line 140
  16. theorem OAI.PerfectCompleteness.CompletionProbability.sample_probability_le line 157
  17. theorem OAI.PerfectCompleteness.CompletionProbability.exists_completion_sampler line 171