OAI/Combinatorics/FiniteCircle/Fourier.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.characterBasis line 12
  2. theorem OAI.FiniteCircle.characterBasis_apply line 17
  3. def OAI.FiniteCircle.characterCoeff line 21
  4. theorem OAI.FiniteCircle.character_expansion line 24
  5. theorem OAI.FiniteCircle.wInner_sum_left line 28
  6. theorem OAI.FiniteCircle.wInner_sum_right line 35
  7. theorem OAI.FiniteCircle.characterCoeff_eq_wInner line 42
  8. theorem OAI.FiniteCircle.character_parseval_complex line 50
  9. theorem OAI.FiniteCircle.character_parseval line 58
  10. theorem OAI.FiniteCircle.characterCoeff_translate line 66
  11. theorem OAI.FiniteCircle.characterCoeff_sub line 81
  12. theorem OAI.FiniteCircle.character_displacement line 86
  13. def OAI.FiniteCircle.cutDistance line 101
  14. theorem OAI.FiniteCircle.cutDistance_self line 104
  15. theorem OAI.FiniteCircle.cutDistance_nonneg line 107
  16. theorem OAI.FiniteCircle.cutDistance_le_one line 110
  17. theorem OAI.FiniteCircle.cutDistance_symm line 113
  18. def OAI.FiniteCircle.HasCutRepresentation line 116
  19. theorem OAI.FiniteCircle.HasCutRepresentation.zero line 124
  20. theorem OAI.FiniteCircle.HasCutRepresentation.congr line 128
  21. theorem OAI.FiniteCircle.HasCutRepresentation.add line 133
  22. theorem OAI.FiniteCircle.HasCutRepresentation.mul line 141
  23. theorem OAI.FiniteCircle.HasCutRepresentation.cut line 148
  24. theorem OAI.FiniteCircle.HasCutRepresentation.sum line 154
  25. theorem OAI.FiniteCircle.finite_scalar_cuts line 165
  26. theorem OAI.FiniteCircle.scalar_cuts line 206
  27. theorem OAI.FiniteCircle.finite_l1_cuts line 211
  28. theorem OAI.FiniteCircle.spectral_square_inequality line 215
  29. theorem OAI.FiniteCircle.spectral_cut_inequality line 229
  30. theorem OAI.FiniteCircle.cut_representation_inequality line 240
  31. theorem OAI.FiniteCircle.lp_one_norm line 258
  32. theorem OAI.FiniteCircle.lp_one_summable line 261
  33. theorem OAI.FiniteCircle.spectral_l1_inequality line 264