OAI/Analysis/IrrationalRotation/Sampling/ProductInfiniteSamplingMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductSampling.measurePreserving_finset_restrict line 13
2. theorem OAI.Invariant233.ProductSampling.integral_integral_finset_restrict line 21
3. theorem OAI.Invariant233.ProductSampling.integrable_average_coordinate_error_sq line 51
4. theorem OAI.Invariant233.ProductSampling.expected_integral_infinite_average_products_sub_sq_le line 71
5. theorem OAI.Invariant233.ProductSampling.ae_summable_spatial_integral_sq_of_summable_bound line 108
6. theorem OAI.Invariant233.ProductSampling.ae_memLp_and_tendsto_norm_of_summable_expected_sq line 127
7. theorem OAI.Invariant233.ProductSampling.ae_all_memLp_and_tendsto_norm_of_summable_expected_sq line 157
8. theorem OAI.Invariant233.ProductSampling.ae_memLp_and_tendsto_norm_of_eventually_expected_sq line 176
9. theorem OAI.Invariant233.ProductSampling.ae_all_memLp_and_tendsto_norm_of_eventually_expected_sq line 196