OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingEstimates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductSampling.abs_prod_sub_prod_le line 9
2. theorem OAI.Invariant233.ProductSampling.abs_prod_add_error_sub_prod_le line 55
3. theorem OAI.Invariant233.ProductSampling.abs_prod_add_error_sub_prod_le_exp line 73
4. theorem OAI.Invariant233.ProductSampling.abs_prod_add_error_sub_prod_le_of_total_le line 92
5. theorem OAI.Invariant233.ProductSampling.mul_rpow_le_one line 103
6. theorem OAI.Invariant233.ProductSampling.growing_product_error_bound line 110