OAI/Computability/PerfectCompleteness/Sampling/UniformLatent.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.UniformLatent.probability_uniform_singleton line 15
  2. abbrev OAI.PerfectCompleteness.UniformLatent.Raw line 25
  3. def OAI.PerfectCompleteness.UniformLatent.latentKernel line 27
  4. def OAI.PerfectCompleteness.UniformLatent.zeroEvent line 33
  5. theorem OAI.PerfectCompleteness.UniformLatent.probability_latentKernel_zero line 36
  6. theorem OAI.PerfectCompleteness.UniformLatent.probability_latentKernel_zero_pos line 50
  7. theorem OAI.PerfectCompleteness.UniformLatent.probability_latentKernel_zero_constant line 57
  8. def OAI.PerfectCompleteness.UniformLatent.projectedKernel line 68
  9. def OAI.PerfectCompleteness.UniformLatent.projectedZero line 74
  10. theorem OAI.PerfectCompleteness.UniformLatent.probability_projectedKernel_zero line 78
  11. theorem OAI.PerfectCompleteness.UniformLatent.probability_projectedKernel_zero_constant line 87
  12. theorem OAI.PerfectCompleteness.UniformLatent.probability_projectedKernel_zero_binary line 96
  13. theorem OAI.PerfectCompleteness.UniformLatent.source_condition_projected line 107