OAI/Combinatorics/Progressions/Polynomial/StepOneScalarPhase.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_stepOne_row_phase_budget line 12
2. theorem OAI.Erdos3.exists_fourier_of_stepOne_cross_correlation line 117
3. theorem OAI.Erdos3.exists_stepOne_scalar_phase_budget line 166