OAI/Analysis/IrrationalRotation/Sampling/TestedSamplingMoments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ScalarSampling.TestedSampling.dominated_boundedKernel_moments line 11
2. def OAI.Invariant233.ScalarSampling.TestedSampling.firstKernel line 44
3. def OAI.Invariant233.ScalarSampling.TestedSampling.secondKernel line 48
4. theorem OAI.Invariant233.ScalarSampling.TestedSampling.first_measurable line 52
5. theorem OAI.Invariant233.ScalarSampling.TestedSampling.second_measurable line 60
6. def OAI.Invariant233.ScalarSampling.TestedSampling.MomentBounds line 68
7. theorem OAI.Invariant233.ScalarSampling.TestedSampling.momentBounds_of_domination line 79
8. theorem OAI.Invariant233.ScalarSampling.TestedSampling.firstKernel_moment_bounds line 105
9. theorem OAI.Invariant233.ScalarSampling.TestedSampling.secondKernel_moment_bounds line 121
10. theorem OAI.Invariant233.ScalarSampling.TestedSampling.firstKernel_univ_univ line 137
11. theorem OAI.Invariant233.ScalarSampling.TestedSampling.secondKernel_univ_univ line 140
12. theorem OAI.Invariant233.ScalarSampling.TestedSampling.secondKernel_eq_literal line 143