OAI/Analysis/IrrationalRotation/Sampling/SyndeticSampling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.SyndeticSampling.card_hits_in_blocks line 9
2. theorem OAI.Invariant233.SyndeticSampling.card_hits_in_half_interval line 43
3. theorem OAI.Invariant233.SyndeticSampling.exists_uniform_hitting_window line 84
4. theorem OAI.Invariant233.SyndeticSampling.exists_uniform_phase_hitting_window line 100
5. theorem OAI.Invariant233.SyndeticSampling.tendsto_sampling_horizon line 134
6. theorem OAI.Invariant233.SyndeticSampling.eventually_exists_prescribed_phase_sampling_powers line 143
7. theorem OAI.Invariant233.SyndeticSampling.eventually_exists_simultaneous_phase_sampling_powers line 204