OAI/Computability/DepthThree/HashProbability.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.finiteProb_eq_card_div line 17
  2. theorem OAI.DepthThreeLowerBound.finiteProb_eq_card_div_decidable line 21
  3. theorem OAI.DepthThreeLowerBound.BinaryHash.normalize_hash_count line 32
  4. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_fiber_probability line 38
  5. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_collision_probability line 55
  6. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_badSeed_probability_le line 72
  7. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_badSeed_probability_le_pow line 113
  8. def OAI.DepthThreeLowerBound.BinaryHash.restrictionFixed line 121
  9. theorem OAI.DepthThreeLowerBound.BinaryHash.fill_mem_boolCoordinateCube line 125
  10. theorem OAI.DepthThreeLowerBound.BinaryHash.range_fill_eq_boolCoordinateCube line 131
  11. theorem OAI.DepthThreeLowerBound.BinaryHash.fill_injective line 145
  12. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_fill_injective_iff line 150
  13. theorem OAI.DepthThreeLowerBound.BinaryHash.card_liveSet line 164
  14. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_restriction_failure_le line 170
  15. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_restriction_failure_le_pow line 189