OAI/Combinatorics/Progressions/Fourier/NativeMixedFourierProfiles.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.cyclicRealLinearPhase line 11
2. theorem OAI.Erdos3.norm_cyclicRealLinearPhase line 14
3. theorem OAI.Erdos3.cyclicRealLinearPhase_unit_shift_error line 17
4. theorem OAI.Erdos3.mean_twisted_nat_translate_error line 53
5. theorem OAI.Erdos3.exists_fourier_of_twisted_unit_shift line 85
6. theorem OAI.Erdos3.exists_fourier_of_real_linear_phase line 156
7. theorem OAI.Erdos3.exists_fourier_of_stepOne_expansion line 180
8. theorem OAI.Erdos3.exists_cubic_fixed_fourier_correlation line 223
9. theorem OAI.Erdos3.exists_cubic_frequency_correlation line 278
10. theorem OAI.Erdos3.NativeMixedCorrelation.exists_cube_residual_fourier_profiles line 314