OAI/Analysis/IrrationalRotation/Product/ProductTestedKernelMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ProductSamplingPhaseMoments.testedKernel line 14
2. theorem OAI.Invariant233.ProductSamplingPhaseMoments.testedKernel_measurable line 22
3. theorem OAI.Invariant233.ProductSamplingPhaseMoments.testedKernel_bounds line 40
4. theorem OAI.Invariant233.ProductSamplingPhaseMoments.realBVSize_le_of_global line 64
5. theorem OAI.Invariant233.ProductSamplingPhaseMoments.testedKernel_BV_bound line 76
6. theorem OAI.Invariant233.ProductSamplingPhaseMoments.testedKernel_momentBounds line 103
7. theorem OAI.Invariant233.ProductSamplingPhaseMoments.testedKernel_square_moment_bound line 111
8. theorem OAI.Invariant233.ProductSamplingPhaseMoments.tested_expected_average_error_le line 132