OAI/Combinatorics/Progressions/Fourier/LogCharacterBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieBCHGroup.logCharacter line 14
2. theorem OAI.Erdos3.NilpotentLieBCHGroup.logCharacter_norm line 17
3. theorem OAI.Erdos3.NilpotentLieBCHGroup.logCharacter_mul line 20
4. theorem OAI.Erdos3.NilpotentLieBCHGroup.logCharacter_inv_mul line 26
5. theorem OAI.Erdos3.NilpotentLieBCHGroup.logCharacter_of_integral line 31
6. theorem OAI.Erdos3.NilpotentLieBCHGroup.logCharacter_norm_sub_eq_relative line 49
7. def OAI.Erdos3.logCharacterMetricConstant line 77
8. theorem OAI.Erdos3.NilpotentLieBCHGroup.logCharacter_dist_one_le line 89
9. theorem OAI.Erdos3.bchLogMetricConstant_le_inverse line 127
10. theorem OAI.Erdos3.exists_logCharacterMetricConstant_exp_bound line 134