OAI/Computability/PerfectCompleteness/Construction/HierarchicalBucketFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.HierarchicalBucketFamily.PairRecord line 43
  2. def OAI.PerfectCompleteness.HierarchicalBucketFamily.collision line 46
  3. def OAI.PerfectCompleteness.HierarchicalBucketFamily.referencePairLaw line 51
  4. theorem OAI.PerfectCompleteness.HierarchicalBucketFamily.reference_collision_eq_mean line 58
  5. def OAI.PerfectCompleteness.HierarchicalBucketFamily.actualBackgrounds line 74
  6. def OAI.PerfectCompleteness.HierarchicalBucketFamily.actualPairLaw line 79
  7. def OAI.PerfectCompleteness.HierarchicalBucketFamily.usefulMass line 89
  8. theorem OAI.PerfectCompleteness.HierarchicalBucketFamily.collision_probability_lower_bound line 105
  9. theorem OAI.PerfectCompleteness.HierarchicalBucketFamily.collision_probability_ge_eighth line 116
  10. theorem OAI.PerfectCompleteness.HierarchicalBucketFamily.mean_agreement_ge line 130
  11. theorem OAI.PerfectCompleteness.HierarchicalBucketFamily.mean_agreement_ge_actual_background line 146