OAI/Computability/PerfectCompleteness/Sampling/BoundedListSamplingLemmas.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.BoundedListSampling.listLaw line 20
  2. theorem OAI.PerfectCompleteness.BoundedListSampling.listLaw_of_nonempty line 24
  3. theorem OAI.PerfectCompleteness.BoundedListSampling.listLaw_empty_weight line 28
  4. theorem OAI.PerfectCompleteness.BoundedListSampling.listLaw_weight_mem line 32
  5. theorem OAI.PerfectCompleteness.BoundedListSampling.listLaw_weight_lower line 37
  6. theorem OAI.PerfectCompleteness.BoundedListSampling.list_success_lower line 45
  7. def OAI.PerfectCompleteness.BoundedListSampling.jointLaw line 55
  8. theorem OAI.PerfectCompleteness.BoundedListSampling.jointLaw_weight line 58
  9. theorem OAI.PerfectCompleteness.BoundedListSampling.jointLaw_probability line 62
  10. theorem OAI.PerfectCompleteness.BoundedListSampling.jointLaw_index_law line 68
  11. theorem OAI.PerfectCompleteness.BoundedListSampling.jointLaw_weight_ge_of_mem line 85
  12. theorem OAI.PerfectCompleteness.BoundedListSampling.joint_success_lower line 93
  13. theorem OAI.PerfectCompleteness.BoundedListSampling.joint_success_lower_of_indices line 101
  14. def OAI.PerfectCompleteness.BoundedListSampling.outputLaw line 125
  15. theorem OAI.PerfectCompleteness.BoundedListSampling.outputLaw_probability line 129
  16. theorem OAI.PerfectCompleteness.BoundedListSampling.output_success_lower line 135
  17. theorem OAI.PerfectCompleteness.BoundedListSampling.output_weight_ge_of_mem line 144
  18. theorem OAI.PerfectCompleteness.BoundedListSampling.independent_match_lower line 153
  19. def OAI.PerfectCompleteness.LegalUniform.enumeratedWeights line 184
  20. theorem OAI.PerfectCompleteness.LegalUniform.transport_weight_eq_enumerated line 191
  21. def OAI.PerfectCompleteness.LegalUniform.uniformWeights line 200
  22. theorem OAI.PerfectCompleteness.LegalUniform.uniformWeights_weight line 214
  23. theorem OAI.PerfectCompleteness.LegalUniform.transport_uniform_weight line 218
  24. theorem OAI.PerfectCompleteness.LegalUniform.equivFin_uniform_weight line 226
  25. theorem OAI.PerfectCompleteness.LegalUniform.exists_uniform_weights line 233