OAI/Analysis/RotationWeights/ReturnSamples.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CircleSampling.phase_success_eventually line 51
2. lemma OAI.CircleSampling.phase_cover_eventually line 65
3. lemma OAI.CircleSampling.cube_interval_eventually line 84
4. def OAI.CircleSampling.phaseRange line 96
5. lemma OAI.CircleSampling.mem_phaseRange line 98
6. lemma OAI.CircleSampling.phaseRange_bound line 106
7. lemma OAI.CircleSampling.phaseRange_lower line 118
8. lemma OAI.CircleSampling.rotation_syndetic line 125
9. lemma OAI.CircleSampling.return_samples line 154
10. lemma OAI.CircleSampling.finite_separated_subset line 195
11. lemma OAI.CircleSampling.linear_filter_card line 238
12. lemma OAI.CircleSampling.separated_integer_samples line 254
13. lemma OAI.CircleSampling.separated_return_samples line 321
14. lemma OAI.CircleSampling.greedy_degree_bound line 357
15. lemma OAI.CircleSampling.eventually_sampling_length line 372
16. lemma OAI.CircleSampling.eventually_separated_returns line 421