OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/LocalSampling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryMellinSampling.local_sampling line 22
2. theorem OAI.OrdinaryMellinSampling.spaced_sampling line 69
3. lemma OAI.OrdinaryMellinSampling.phase_hasDerivAt line 105
4. lemma OAI.OrdinaryMellinSampling.polynomial_hasDerivAt line 115
5. lemma OAI.OrdinaryMellinSampling.shifted_polynomial_norm line 124
6. lemma OAI.OrdinaryMellinSampling.one_sided_interval_energy line 132
7. theorem OAI.OrdinaryMellinSampling.band_spaced_mean_square line 147