OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingNumericalMajorant.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductSampling.eventually_const_mul_log_le_rpow line 14
2. theorem OAI.Invariant233.ProductSampling.diagonal_sampling_term_le line 23
3. theorem OAI.Invariant233.ProductSampling.eventually_diagonal_sampling_term_le line 56
4. theorem OAI.Invariant233.ProductSampling.sampling_product_factor_le_exp line 65
5. theorem OAI.Invariant233.ProductSampling.sampling_product_error_le line 99
6. theorem OAI.Invariant233.ProductSampling.eventually_sampling_moment_majorant line 130
7. theorem OAI.Invariant233.ProductSampling.summable_of_sampling_moment_bound line 145
8. theorem OAI.Invariant233.ProductScaleLaws.summable_sampling_error_of_moment_bound line 168