OAI/Analysis/FourierLLogL/Dyadic/Discrete.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Cyclic grid, characters and averaged Fourier coefficients

  1. lemma OAI.FourierLLogL.Dyadic.card_side line 17
  2. lemma OAI.FourierLLogL.Dyadic.uniform_side line 22
  3. lemma OAI.FourierLLogL.Dyadic.side_pow_two line 25
  4. lemma OAI.FourierLLogL.Dyadic.expU_ex line 27
  5. lemma OAI.FourierLLogL.Dyadic.expU_cx line 31
  6. lemma OAI.FourierLLogL.Dyadic.expU_prod line 36
  7. lemma OAI.FourierLLogL.Dyadic.expU_sum line 43
  8. lemma OAI.FourierLLogL.Dyadic.expU_add line 48
  9. lemma OAI.FourierLLogL.Dyadic.expU_translate line 53
  10. lemma OAI.FourierLLogL.Dyadic.expU_reflect line 60
  11. lemma OAI.FourierLLogL.Dyadic.expU_lmul line 66
  12. lemma OAI.FourierLLogL.Dyadic.expU_real line 69
  13. def OAI.FourierLLogL.Dyadic.phaseChar line 73

    Source documentation

    Wrap grid characters as an AddChar.

    def phaseChar (u : Grid M) : AddChar (Grid M) ℂ := ZMod.stdAddChar.mulShift u

    Mentions: OAI.FourierLLogL.Dyadic.Grid

  14. lemma OAI.FourierLLogL.Dyadic.phaseChar_apply line 75
  15. lemma OAI.FourierLLogL.Dyadic.chi_comm line 77
  16. lemma OAI.FourierLLogL.Dyadic.chi_zero_right line 80
  17. lemma OAI.FourierLLogL.Dyadic.chi_zero_left line 81
  18. lemma OAI.FourierLLogL.Dyadic.chi_add line 83
  19. lemma OAI.FourierLLogL.Dyadic.chi_add' line 86
  20. lemma OAI.FourierLLogL.Dyadic.chi_neg line 89
  21. lemma OAI.FourierLLogL.Dyadic.chi_neg' line 96
  22. lemma OAI.FourierLLogL.Dyadic.chi_sub line 97
  23. lemma OAI.FourierLLogL.Dyadic.chi_nsmul line 100
  24. lemma OAI.FourierLLogL.Dyadic.expU_chi line 106
  25. def OAI.FourierLLogL.Dyadic.fc line 118

    Source documentation

    Averages against conj character. Evaluation form instead of linear notation.

    def fc (f : Grid M → ℂ) (u : Grid M) : ℂ := expU fun x => f x * chi (-u) x

    Mentions: OAI.FourierLLogL.Dyadic.Grid, OAI.FourierLLogL.Dyadic.expU, OAI.FourierLLogL.Dyadic.chi

  26. lemma OAI.FourierLLogL.Dyadic.fc_lmul line 120
  27. lemma OAI.FourierLLogL.Dyadic.fc_add line 125
  28. lemma OAI.FourierLLogL.Dyadic.fc_sum line 130
  29. lemma OAI.FourierLLogL.Dyadic.fc_chi line 135
  30. lemma OAI.FourierLLogL.Dyadic.expU_coeff line 138
  31. lemma OAI.FourierLLogL.Dyadic.fc_neg_even line 141
  32. lemma OAI.FourierLLogL.Dyadic.fc_neg_real line 148
  33. lemma OAI.FourierLLogL.Dyadic.real_fc_even line 153
  34. lemma OAI.FourierLLogL.Dyadic.invert_fc line 165
  35. lemma OAI.FourierLLogL.Dyadic.fc_mul_chi line 180
  36. lemma OAI.FourierLLogL.Dyadic.fc_prod line 184
  37. lemma OAI.FourierLLogL.Dyadic.fc_right_translate line 192
  38. lemma OAI.FourierLLogL.Dyadic.fc_parseval line 199