OAI/Computability/PerfectCompleteness/Foundations/HierarchicalAgreementMean.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.HierarchicalAgreementMean.probability_product line 20
  2. abbrev OAI.PerfectCompleteness.HierarchicalAgreementMean.Background line 31
  3. abbrev OAI.PerfectCompleteness.HierarchicalAgreementMean.Matrix line 32
  4. abbrev OAI.PerfectCompleteness.HierarchicalAgreementMean.PairRecord line 44
  5. abbrev OAI.PerfectCompleteness.HierarchicalAgreementMean.BucketSample line 48
  6. def OAI.PerfectCompleteness.HierarchicalAgreementMean.bucketLaw line 53
  7. def OAI.PerfectCompleteness.HierarchicalAgreementMean.pairRecord line 62
  8. def OAI.PerfectCompleteness.HierarchicalAgreementMean.referenceLaw line 71
  9. def OAI.PerfectCompleteness.HierarchicalAgreementMean.collision line 82
  10. theorem OAI.PerfectCompleteness.HierarchicalAgreementMean.reference_collision_eq_mean line 90
  11. theorem OAI.PerfectCompleteness.HierarchicalAgreementMean.mean_nonzeroAgreement_ge_of_collision line 107
  12. theorem OAI.PerfectCompleteness.HierarchicalAgreementMean.mean_nonzeroAgreement_ge_sixteenth line 123