OAI/Combinatorics/Progressions/Fourier/RelativeSpectrumDimension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.realFinsetIndicator line 13
2. theorem OAI.Erdos3.RelativeSpectrumBridge.sum_realFinsetIndicator_mul_eq_const_mul_card line 23
3. theorem OAI.Erdos3.RelativeSpectrumBridge.sum_realFinsetIndicator_mul_character_eq_const_mul line 39
4. theorem OAI.Erdos3.RelativeSpectrumBridge.mem_relativeLargeSpectrum_of_eq_const_iff line 58
5. theorem OAI.Erdos3.RelativeChangSanders.card_weightedDissociated_relativeLargeSpectrum_le line 99
6. theorem OAI.Erdos3.RelativeChangSanders.card_weightedDissociated_realFinsetIndicator_le line 247