OAI/Computability/PerfectCompleteness/Construction/BucketQuotientAgreement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.collision_indicator_eq line 20
  2. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.probability_collision_eq_expectation line 26
  3. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.expectation_uniform_eq_expect line 37
  4. def OAI.PerfectCompleteness.BucketQuotientAgreement.directionCollision line 46
  5. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.directionCollision_eq line 56
  6. def OAI.PerfectCompleteness.BucketQuotientAgreement.agreement line 70
  7. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.agreement_eq_projectedAgreement line 74
  8. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.agreement_eq_nonzeroAgreement line 84
  9. theorem OAI.PerfectCompleteness.BucketQuotientAgreement.uniform_bucket_collision_probability line 90