OAI/Computability/PerfectCompleteness/Sampling/WholeArraySampler.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeArraySampler.StepIndex line 19
  2. def OAI.PerfectCompleteness.WholeArraySampler.StepFactor line 22
  3. instance OAI.PerfectCompleteness.WholeArraySampler.stepFactorFintype line 28
  4. abbrev OAI.PerfectCompleteness.WholeArraySampler.StepTape line 34
  5. instance OAI.PerfectCompleteness.WholeArraySampler.spaceFintype line 38
  6. abbrev OAI.PerfectCompleteness.WholeArraySampler.RootTape line 42
  7. def OAI.PerfectCompleteness.WholeArraySampler.Tape line 46
  8. def OAI.PerfectCompleteness.WholeArraySampler.tapeFintypeAux line 55
  9. instance OAI.PerfectCompleteness.WholeArraySampler.tapeFintype line 73
  10. def OAI.PerfectCompleteness.WholeArraySampler.zeroTape line 77
  11. instance OAI.PerfectCompleteness.WholeArraySampler.tapeNonempty line 89
  12. def OAI.PerfectCompleteness.WholeArraySampler.leafTapeEquivUnit line 93
  13. def OAI.PerfectCompleteness.WholeArraySampler.assemble line 103
  14. def OAI.PerfectCompleteness.WholeArraySampler.childrenAt line 109
  15. theorem OAI.PerfectCompleteness.WholeArraySampler.childrenAt_selected line 116
  16. theorem OAI.PerfectCompleteness.WholeArraySampler.childrenAt_ordinary line 123
  17. def OAI.PerfectCompleteness.WholeArraySampler.evaluate line 132
  18. theorem OAI.PerfectCompleteness.WholeArraySampler.evaluate_refl line 145
  19. theorem OAI.PerfectCompleteness.WholeArraySampler.evaluate_root line 150
  20. theorem OAI.PerfectCompleteness.WholeArraySampler.evaluate_selected line 158
  21. theorem OAI.PerfectCompleteness.WholeArraySampler.evaluate_ordinary line 168
  22. def OAI.PerfectCompleteness.WholeArraySampler.tapeLaw line 179
  23. def OAI.PerfectCompleteness.WholeArraySampler.componentLaw line 200
  24. theorem OAI.PerfectCompleteness.WholeArraySampler.component_marginal line 212
  25. theorem OAI.PerfectCompleteness.WholeArraySampler.component_image line 225
  26. theorem OAI.PerfectCompleteness.WholeArraySampler.components_independent line 238
  27. theorem OAI.PerfectCompleteness.WholeArraySampler.components_expectation_product line 258
  28. def OAI.PerfectCompleteness.WholeArraySampler.law line 273
  29. theorem OAI.PerfectCompleteness.WholeArraySampler.probability_law line 278
  30. theorem OAI.PerfectCompleteness.WholeArraySampler.root_array_marginal line 286
  31. theorem OAI.PerfectCompleteness.WholeArraySampler.selected_arrays_marginal line 297
  32. theorem OAI.PerfectCompleteness.WholeArraySampler.uniform_arrays_eq_product line 307
  33. theorem OAI.PerfectCompleteness.WholeArraySampler.uniform_arrays_node line 315
  34. theorem OAI.PerfectCompleteness.WholeArraySampler.uniform_arrays_expectation_product line 323
  35. theorem OAI.PerfectCompleteness.WholeArraySampler.ordinary_node_marginal line 335