OAI/Computability/PerfectCompleteness/Decoding/FixedLowerUniformCollision.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.FixedLowerUniformCollision.expectation_uniform_eq_expect line 19
2. def OAI.PerfectCompleteness.FixedLowerUniformCollision.uniformLaw line 30
3. def OAI.PerfectCompleteness.FixedLowerUniformCollision.uniformCollision line 36
4. theorem OAI.PerfectCompleteness.FixedLowerUniformCollision.uniform_collision_eq line 41
5. theorem OAI.PerfectCompleteness.FixedLowerUniformCollision.supported_collision_lt line 88