OAI/NumberTheory/Ostmann/QuadraticCenter/LocalCorrelationInterval.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.residue_grid_linear_sum_bound line 9
2. theorem OAI.Ostmann.QuadraticCenter.interval_fourier_expansion line 29
3. theorem OAI.Ostmann.QuadraticCenter.periodic_interval_twist_bound line 53