OAI/Analysis/IrrationalRotation/Sampling/ProductSamplingAsymptotics.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductSampling.eventually_const_log_le_rpow line 13
2. theorem OAI.Invariant233.ProductSampling.diagonal_product_le_source_power line 22
3. theorem OAI.Invariant233.ProductSampling.diagonal_sampling_ratio_le line 46
4. theorem OAI.Invariant233.ProductSampling.eventually_diagonal_sampling_ratio_le line 63
5. theorem OAI.Invariant233.ProductSampling.dimension_error_le line 73
6. theorem OAI.Invariant233.ProductSampling.eventually_sampling_error_le line 85
7. theorem OAI.Invariant233.ProductSampling.sampling_moment_majorant_summable line 97
8. theorem OAI.Invariant233.ProductSampling.growing_moment_power_le_exp line 122
9. theorem OAI.Invariant233.ProductSampling.exact_moment_error_le line 153
10. theorem OAI.Invariant233.ProductSampling.eventually_exact_second_moment_le line 175
11. theorem OAI.Invariant233.ProductScaleLaws.sampling_moment_majorant_summable line 192