OAI/Combinatorics/HoneycombChords/LaurentPolynomials.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Laurent polynomial support, evaluation, and cosine polynomial averages.

The formulas express reflection-symmetric trigonometric polynomials in the Chebyshev basis.

  1. abbrev OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.LP line 14
  2. abbrev OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.LC line 15
  3. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev line 16
  4. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band line 18
  5. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.band_zero line 19
  6. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.band_C line 20
  7. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.band_T line 26
  8. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.mono line 33
  9. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.add line 37
  10. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.neg line 43
  11. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.sub line 45
  12. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.mul line 47
  13. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.sum line 53
  14. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.C_mul line 62
  15. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.mul_C line 64
  16. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.pow line 66
  17. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_C line 70
  18. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_T line 71
  19. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_sum line 80
  20. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn line 85
  21. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_band line 89
  22. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_sn line 94
  23. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.top_mul line 103
  24. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coeff_C_mul line 142
  25. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coeff_mul_C line 145
  26. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coeff_add line 148
  27. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coeff_sub line 149
  28. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coeff_zero line 150
  29. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coeff_sum line 151
  30. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.coeff_zero line 153
  31. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_coeff line 157
  32. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_top_plus line 161
  33. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_top_minus line 163
  34. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_pair_top line 165
  35. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.inv_two_I_sq line 168
  36. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_plus_plus line 170
  37. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_minus_minus line 174
  38. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_minus_plus line 178
  39. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sn_plus_minus line 182
  40. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.point_pair line 192
  41. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.point_even_pi line 194
  42. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.point_odd_pi line 198
  43. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cheb_cos line 206
  44. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.monomial_average line 210
  45. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cosinePoly line 228
  46. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cos_index_bound line 231
  47. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cosinePoly_degree line 239
  48. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_interval line 246
  49. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cosinePoly_eval line 254
  50. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.flip line 276
  51. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.conjugate line 277
  52. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.conjugate_coeff line 279
  53. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Band.conjugate line 282
  54. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.conjugate_single line 287
  55. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.point_star line 295
  56. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.conjugate_C line 297
  57. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.conjugate_T line 300
  58. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_conjugate line 303
  59. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.continuous_ev line 322
  60. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.point_range_infinite line 328
  61. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_toLaurent line 336
  62. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_eq_zero line 341
  63. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_ext line 355
  64. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_ext_dense line 360
  65. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cheb_coeff_top line 373
  66. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cosinePoly_top line 377