OAI/Computability/PerfectCompleteness/Repetition/CleanConditioning.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CleanConditioning.allEvent line 21
  2. theorem OAI.PerfectCompleteness.CleanConditioning.product_filter line 25
  3. theorem OAI.PerfectCompleteness.CleanConditioning.probability_law_all line 36
  4. theorem OAI.PerfectCompleteness.CleanConditioning.coordinate_probability_positive line 47
  5. theorem OAI.PerfectCompleteness.CleanConditioning.condition_law_all line 59
  6. theorem OAI.PerfectCompleteness.CleanConditioning.pushforward_law line 76
  7. theorem OAI.PerfectCompleteness.CleanConditioning.condition_clean_mask line 96
  8. def OAI.PerfectCompleteness.CleanConditioning.kernelJoint line 110
  9. theorem OAI.PerfectCompleteness.CleanConditioning.probability_kernelJoint line 119
  10. theorem OAI.PerfectCompleteness.CleanConditioning.probability_kernelJoint_fiber line 131
  11. theorem OAI.PerfectCompleteness.CleanConditioning.probability_kernelJoint_constant line 143
  12. theorem OAI.PerfectCompleteness.CleanConditioning.source_condition_of_constant line 151
  13. theorem OAI.PerfectCompleteness.CleanConditioning.designated_source_condition line 171