OAI/Combinatorics/StripMass/SpecializationPolynomial.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.RationalAt.eval₂ line 14
  2. lemma OAI.CriticalStrip.Diagram.RationalAt.eval_map line 22
  3. lemma OAI.CriticalStrip.Diagram.LastDegree.map line 29
  4. lemma OAI.CriticalStrip.Diagram.LastDegree.of_map line 35
  5. lemma OAI.CriticalStrip.Diagram.liftLaurent_eq_insert line 48
  6. lemma OAI.CriticalStrip.Diagram.lastExponent_eq_smul line 57
  7. lemma OAI.CriticalStrip.Diagram.lastCosine_eq line 61
  8. lemma OAI.CriticalStrip.Diagram.lastCosine_map line 67
  9. lemma OAI.CriticalStrip.Diagram.lastCosine_box line 73
  10. lemma OAI.CriticalStrip.Diagram.lastSine_box line 79
  11. def OAI.CriticalStrip.Diagram.lastLaurent line 86
  12. lemma OAI.CriticalStrip.Diagram.lastLaurent_map line 89
  13. lemma OAI.CriticalStrip.Diagram.lastLaurent_box line 114
  14. theorem OAI.CriticalStrip.Diagram.liftSpectral_weights_tile line 172
  15. theorem OAI.CriticalStrip.Diagram.spectralColumn_lastValue line 179
  16. theorem OAI.CriticalStrip.Diagram.rationalInterpolant_eq_lastValue line 208
  17. theorem OAI.CriticalStrip.Diagram.rationalInterpolationResidual_transfer line 217
  18. theorem OAI.CriticalStrip.Diagram.rationalInterpolationResidual_factor line 240
  19. lemma OAI.CriticalStrip.Diagram.rowDenominator_box line 260
  20. lemma OAI.CriticalStrip.Diagram.variableExponent_selfBound line 269
  21. lemma OAI.CriticalStrip.Diagram.negVariableExponent_selfBound line 273
  22. lemma OAI.CriticalStrip.Diagram.selfBound_one_add line 276
  23. lemma OAI.CriticalStrip.Diagram.rowNumerator_box line 279
  24. lemma OAI.CriticalStrip.Diagram.sum_selfBound line 292
  25. lemma OAI.CriticalStrip.Diagram.rawColumn_box line 296
  26. def OAI.CriticalStrip.Diagram.laurentResidual line 310
  27. lemma OAI.CriticalStrip.Diagram.laurentResidual_box line 313
  28. lemma OAI.CriticalStrip.Diagram.laurentResidual_map line 323
  29. lemma OAI.CriticalStrip.Diagram.signLaurent_lift line 354
  30. lemma OAI.CriticalStrip.Diagram.signSpectral_lift line 364
  31. lemma OAI.CriticalStrip.Diagram.rationalInterpolant_parity line 374
  32. lemma OAI.CriticalStrip.Diagram.signSpectral_column line 393
  33. lemma OAI.CriticalStrip.Diagram.signSpectral_rowDenominator line 401
  34. theorem OAI.CriticalStrip.Diagram.rationalInterpolationResidual_parity line 410
  35. def OAI.CriticalStrip.Diagram.LastMatrix line 438
  36. def OAI.CriticalStrip.Diagram.matrixPolynomial line 442
  37. lemma OAI.CriticalStrip.Diagram.matrixPolynomial_coeff line 446
  38. lemma OAI.CriticalStrip.Diagram.LastMatrix.degree line 451
  39. lemma OAI.CriticalStrip.Diagram.LastMatrix.lastValue line 463
  40. lemma OAI.CriticalStrip.Diagram.LastMatrix.leading line 485
  41. lemma OAI.CriticalStrip.Diagram.LastMatrix.local line 502
  42. lemma OAI.CriticalStrip.Diagram.LastMatrix.omit line 505
  43. lemma OAI.CriticalStrip.Diagram.LastMatrix.mul line 516