OAI/Computability/PerfectCompleteness/Sampling/RecordSeedSamplingLemmas.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.RecordSeedSampling.freshLaw line 20
  2. theorem OAI.PerfectCompleteness.RecordSeedSampling.probability_eq_table_mean line 25
  3. theorem OAI.PerfectCompleteness.RecordSeedSampling.supported_row line 52
  4. theorem OAI.PerfectCompleteness.RecordSeedSampling.probability_supported_guard line 59
  5. theorem OAI.PerfectCompleteness.RecordSeedSampling.probability_le_of_supported_tables line 69
  6. abbrev OAI.PerfectCompleteness.RecursiveSampler.OffPath line 96
  7. def OAI.PerfectCompleteness.RecursiveSampler.DrawIndex line 98
  8. instance OAI.PerfectCompleteness.RecursiveSampler.drawIndexFintype line 103
  9. instance OAI.PerfectCompleteness.RecursiveSampler.drawIndexDecidableEq line 112
  10. def OAI.PerfectCompleteness.RecursiveSampler.DrawSpace line 123
  11. abbrev OAI.PerfectCompleteness.RecursiveSampler.Tape line 132
  12. def OAI.PerfectCompleteness.RecursiveSampler.zeroDraw line 136
  13. def OAI.PerfectCompleteness.RecursiveSampler.zeroTape line 145
  14. instance OAI.PerfectCompleteness.RecursiveSampler.drawSpaceNonempty line 149
  15. instance OAI.PerfectCompleteness.RecursiveSampler.tapeNonempty line 154
  16. theorem OAI.PerfectCompleteness.RecursiveSampler.drawSpace_finite line 158
  17. instance OAI.PerfectCompleteness.RecursiveSampler.drawSpaceFinite line 177
  18. instance OAI.PerfectCompleteness.RecursiveSampler.drawSpaceFintype line 182
  19. def OAI.PerfectCompleteness.RecursiveSampler.subTape line 187
  20. theorem OAI.PerfectCompleteness.RecursiveSampler.recursive_locations_distinct line 193
  21. def OAI.PerfectCompleteness.RecursiveSampler.combineFunction line 204
  22. theorem OAI.PerfectCompleteness.RecursiveSampler.combineFunction_mem line 211
  23. def OAI.PerfectCompleteness.RecursiveSampler.combine line 225
  24. theorem OAI.PerfectCompleteness.RecursiveSampler.combine_zero line 232
  25. def OAI.PerfectCompleteness.RecursiveSampler.evaluate line 239
  26. theorem OAI.PerfectCompleteness.RecursiveSampler.evaluate_refl line 250
  27. theorem OAI.PerfectCompleteness.RecursiveSampler.evaluate_step line 254
  28. theorem OAI.PerfectCompleteness.RecursiveSampler.evaluate_mem line 264
  29. theorem OAI.PerfectCompleteness.RecursiveSampler.evaluate_zeroTape line 269
  30. def OAI.PerfectCompleteness.RecursiveSampler.tapeLaw line 287
  31. theorem OAI.PerfectCompleteness.RecursiveSampler.tapeLaw_eq_uniform line 292
  32. theorem OAI.PerfectCompleteness.RecursiveSampler.tapeLaw_marginal line 297
  33. def OAI.PerfectCompleteness.RecursiveSampler.law line 303
  34. theorem OAI.PerfectCompleteness.RecursiveSampler.law_refl_uniform line 308
  35. theorem OAI.PerfectCompleteness.RecursiveSampler.probability_law line 315