OAI/Probability/ClassicalON/ProfileEstimates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClassicalON.squareStep line 10
2. theorem OAI.ClassicalON.squareStep_distance line 13
3. theorem OAI.ClassicalON.profiles_uniform_bound line 17
4. theorem OAI.ClassicalON.theta_trapezoid_bound line 35
5. theorem OAI.ClassicalON.squareCutoff_near_gradient line 48
6. theorem OAI.ClassicalON.squareProfile_product_difference line 75
7. theorem OAI.ClassicalON.squareTheta_step_error line 92