OAI/Computability/DepthThree/MomentBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DepthThreeLowerBound.UniformBitsUpTo line 18
2. theorem OAI.DepthThreeLowerBound.sign_not line 23
3. theorem OAI.DepthThreeLowerBound.abs_sign_mul_indicator_le_one line 26
4. def OAI.DepthThreeLowerBound.flipCoordinate line 30
5. theorem OAI.DepthThreeLowerBound.uniform_product_zero_of_singleton line 41
6. theorem OAI.DepthThreeLowerBound.tuple_product_avg_zero line 75
7. theorem OAI.DepthThreeLowerBound.sign_indicator_product_le_one line 95
8. theorem OAI.DepthThreeLowerBound.even_moment_le line 103
9. theorem OAI.DepthThreeLowerBound.even_moment_le_manuscript line 145