OAI/Combinatorics/Progressions/Estimates/CyclicRelativeChang.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.RelativeChangSanders.AddDissociatedMod line 19
  2. theorem OAI.Erdos3.RelativeChangSanders.addDissociatedMod_empty line 25
  3. theorem OAI.Erdos3.RelativeChangSanders.AddDissociatedMod.mono line 34
  4. theorem OAI.Erdos3.RelativeChangSanders.exists_maximal_addDissociatedMod line 43
  5. theorem OAI.Erdos3.RelativeChangSanders.exists_maximal_addDissociatedMod_card_le line 129
  6. def OAI.Erdos3.RelativeChangSanders.signedFrequency line 155
  7. def OAI.Erdos3.RelativeChangSanders.signedCoefficient line 158
  8. lemma OAI.Erdos3.RelativeChangSanders.rieszProduct_eq_signedExpansion line 164
  9. lemma OAI.Erdos3.RelativeChangSanders.weightedRiesz_eq_signedExpansion line 200
  10. lemma OAI.Erdos3.RelativeChangSanders.signedFrequency_not_mem line 223
  11. lemma OAI.Erdos3.RelativeChangSanders.norm_signedCoefficient_le line 237
  12. theorem OAI.Erdos3.RelativeChangSanders.AddDissociatedMod.weighted_riesz_randomisation_le line 265
  13. theorem OAI.Erdos3.RelativeChangSanders.AddDissociatedMod.isWeightedDissociated line 343
  14. theorem OAI.Erdos3.RelativeChangSanders.AddDissociatedMod.isWeightedDissociated_of_le_quarter_pow line 365
  15. theorem OAI.Erdos3.RelativeChangSanders.zero_mem_chang_largeSpectrum_half line 380
  16. theorem OAI.Erdos3.RelativeChangSanders.neg_mem_chang_largeSpectrum line 387
  17. def OAI.Erdos3.RelativeChangSanders.localChangDimension line 419
  18. def OAI.Erdos3.RelativeChangSanders.localChangCap line 422
  19. def OAI.Erdos3.RelativeChangSanders.localChangBaseScale line 425
  20. theorem OAI.Erdos3.RelativeChangSanders.exists_relativeLargeSpectrum_cover line 430