OAI/Combinatorics/Progressions/Fourier/VerticalFrequencyIdentification.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieBCHGroup.central_span_character line 17
2. theorem OAI.Erdos3.NilpotentLieFiltration.realSquareObservable_relative_character line 71
3. theorem OAI.Erdos3.NilpotentLieFiltration.realSquare_descent_relative_character line 90
4. theorem OAI.Erdos3.vertical_frequency_integral_on_lattice line 133
5. theorem OAI.Erdos3.real_frequency_eq_of_character_multiples line 164
6. theorem OAI.Erdos3.vertical_frequency_on_real_direction line 186
7. theorem OAI.Erdos3.NilpotentLieFiltration.square_mode_relative_frequency line 220
8. theorem OAI.Erdos3.NilpotentLieFiltration.descended_square_mode_frequency_restriction line 263
9. theorem OAI.Erdos3.vertical_frequency_eq_of_real_line line 303
10. theorem OAI.Erdos3.vertical_frequency_eq_one_of_real_line line 315