OAI/Combinatorics/SumProduct/Alignment/WeylInverse01.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeylInverse.density_of_large_average line 19
2. theorem OAI.WeylInverse.exists_dense_fiber line 38
3. theorem OAI.WeylInverse.exists_dense_derivatives line 54
4. def OAI.WeylInverse.LeadingInverse line 83
5. theorem OAI.WeylInverse.leading_inverse_one line 91
6. theorem OAI.WeylInverse.leading_inverse_step_at_length line 116
7. theorem OAI.WeylInverse.leading_inverse_succ line 199
8. theorem OAI.WeylInverse.leading_inverse line 281