OAI/Analysis/IrrationalRotation/Sampling/SamplingTestContinuity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.SamplingTests.measurable_kernel line 14
2. lemma OAI.Invariant233.SamplingTests.measurable_circleKernel line 32
3. lemma OAI.Invariant233.SamplingTests.measurable_average line 37
4. lemma OAI.Invariant233.SamplingTests.measurable_errorSq line 52
5. lemma OAI.Invariant233.SamplingTests.kernel_bounds line 56
6. lemma OAI.Invariant233.SamplingTests.average_bounds line 61
7. lemma OAI.Invariant233.SamplingTests.errorSq_bounds line 89
8. lemma OAI.Invariant233.SamplingTests.ae_joint_continuousAt_kernel line 103
9. lemma OAI.Invariant233.SamplingTests.ae_joint_continuousAt_circleKernel line 131
10. lemma OAI.Invariant233.SamplingTests.continuousAt_average_of_kernel line 150
11. lemma OAI.Invariant233.SamplingTests.ae_joint_continuousAt_average line 182
12. lemma OAI.Invariant233.SamplingTests.ae_joint_continuousAt_errorSq line 204