OAI/Combinatorics/HoneycombChords/LaurentTransfer.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

Laurent and cosine polynomial forms of the strip transfer.

This development follows the finite strip transfer calculation for critical honeycomb walks in the companion paper on uniform marked polygon estimates.

  1. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.qNum line 15
  2. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.aNum line 16
  3. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.hNum line 17
  4. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.vNum line 18
  5. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cNum line 19
  6. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.dNum line 20
  7. abbrev OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.LPLocal line 21
  8. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rNum line 22
  9. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_qNum line 44
  10. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_local_coefficients line 47
  11. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_rNum line 59
  12. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.local_bands line 65
  13. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rNum_band0 line 76
  14. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rNum_band1 line 90
  15. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rNum_band2 line 103
  16. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rNum_band line 117
  17. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.kNum line 123
  18. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.kNum_band line 129
  19. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_kNum line 143
  20. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.qPlus line 160
  21. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.qMinus line 161
  22. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.leadWeight line 162
  23. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.backWeight line 163
  24. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.v_top_plus line 164
  25. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.c_top_plus line 168
  26. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.d_top_plus line 173
  27. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.q_top_plus line 177
  28. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.v_top_minus line 181
  29. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.c_top_minus line 185
  30. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.d_top_minus line 189
  31. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.q_top_minus line 194
  32. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.a_top_zero line 199
  33. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.h_top_zero line 201
  34. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_18 line 203
  35. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_20 line 205
  36. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_22 line 207
  37. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_24 line 209
  38. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_26 line 211
  39. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_28 line 213
  40. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.root_30 line 215
  41. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.r_top_plus_small line 217
  42. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.r_top_minus_small line 227
  43. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.qPlus_mul_qMinus line 237
  44. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.leadWeight_zpow line 241
  45. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.backWeight_zpow line 244
  46. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rowNum line 257
  47. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rowNum_band line 260
  48. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_rNum_scaled line 274
  49. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_rowNum line 279
  50. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.bulkNum line 297
  51. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.bulkNum_band line 299
  52. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_bulkNum line 304
  53. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.rowNum_top_step line 335
  54. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.space_eq_iff line 345
  55. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.weightProd line 351
  56. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.weightProd_succ line 352
  57. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.row_top_plus_small line 357
  58. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.row_top_minus_small line 371
  59. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.columnCharge_succ line 385
  60. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.weightProd_lead_zpow line 390
  61. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.weightProd_back_zpow line 398
  62. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.den line 413
  63. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.sine_pair line 415
  64. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.boundary_den_cos line 424
  65. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.Q_pair_cos line 429
  66. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.den_cos line 439
  67. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.den_star line 448
  68. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.den_reflection line 450
  69. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.den_periodicity line 453
  70. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coefficientNum line 463
  71. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coefficientNum_band line 465
  72. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.homogeneous_nonsingular_iff line 471
  73. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_coefficientNum line 484
  74. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.den_ne_zero line 500
  75. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.pairNum line 503
  76. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.pairNum_band line 508
  77. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.both_pair_form line 514
  78. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_pairNum line 519
  79. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.scalarNum line 529
  80. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.scalarNum_band line 532
  81. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_scalarNum line 536
  82. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.bulkNum_top line 554
  83. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.bulkNum_top_small line 564
  84. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.kNum_true line 590
  85. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coefficientNum_TT line 595
  86. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.wall_top_product line 602
  87. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.wall_bulk_wall_top line 617
  88. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coefficientNum_TT_top line 629
  89. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.coefficientNum_TT_top_zeroCharge line 648
  90. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalP_reflection line 661
  91. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalP_periodicity line 665
  92. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.homogeneous_nonsingular_den line 668
  93. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.dense_homogeneous_nonsingular line 679
  94. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.flip_coeff line 691
  95. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.flip_C line 693
  96. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.flip_T line 696
  97. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.ev_flip line 699
  98. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.scalarNum_flip line 710
  99. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.scalarNum_coeff_reflection line 717
  100. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.cosinePoly_physical line 719
  101. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.pairNum_bottom line 743
  102. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.spinCharge_rev line 753
  103. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.reflectedSites_charge line 755
  104. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.base_normalizedDual line 761
  105. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.base_markedEigenvector line 764
  106. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physical_pair_bottom line 766
  107. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.scalarNum_bottom line 782
  108. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.scalarNum_top line 786
  109. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalNumerator line 788
  110. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalNumerator_degree line 790
  111. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalNumerator_top line 794
  112. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.drop_top_degree line 814
  113. def OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.polePoly line 821
  114. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.polePoly_monic line 823
  115. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.polePoly_degree line 825
  116. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.polePoly_top line 830
  117. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.polynomial_linear_decomposition line 833
  118. lemma OAI.CriticalHoneycomb.Transfer.SpectralFamily.Trig.physicalNumerator_decomposition line 865