OAI/Computability/DepthThree/HardSliceParameters.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DepthThreeLowerBound.sparseMomentBound_at_quarter line 15
2. theorem OAI.DepthThreeLowerBound.sparseMomentBound_quarter_le line 38
3. theorem OAI.DepthThreeLowerBound.exists_hashDimension_dominates line 52
4. theorem OAI.DepthThreeLowerBound.hard_slice_error_bound_eventually line 75
5. theorem OAI.DepthThreeLowerBound.hash_collision_ratio_eq line 118
6. theorem OAI.DepthThreeLowerBound.actual_hard_slice_error_bound_eventually line 123