OAI/NumberTheory/ShortEgyptian/WindowDiscrepancy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ShortEgyptian.spectral_error_bound line 10
2. theorem OAI.ShortEgyptian.window_mass_lower line 51
3. theorem OAI.ShortEgyptian.charSum_norm_le_card line 74
4. theorem OAI.ShortEgyptian.uniform_mass_lower line 80
5. def OAI.ShortEgyptian.residueWindow line 110
6. theorem OAI.ShortEgyptian.residueWindow_size line 113
7. theorem OAI.ShortEgyptian.mem_residueWindow line 119
8. theorem OAI.ShortEgyptian.finite_residue_discrepancy line 133