OAI/Combinatorics/StripMass/Trigonometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.C_c_facts line 13
  2. theorem OAI.CriticalStrip.harmonic_eval line 25
  3. theorem OAI.CriticalStrip.branch_rescaled_tendsto line 30
  4. theorem OAI.CriticalStrip.eventually_small_inverse line 52
  5. theorem OAI.CriticalStrip.highBranch_rescaled line 57
  6. theorem OAI.CriticalStrip.lowBranch_rescaled line 67
  7. theorem OAI.CriticalStrip.lower_rescaling_zero line 78
  8. theorem OAI.CriticalStrip.homogeneousQ_high_decay line 92
  9. theorem OAI.CriticalStrip.homogeneousQ_low_limit line 110
  10. theorem OAI.CriticalStrip.tilde_projection_eval line 125
  11. theorem OAI.CriticalStrip.tilde_F_decay line 137
  12. theorem OAI.CriticalStrip.tilde_D_limit line 158
  13. theorem OAI.CriticalStrip.harmonic_natDegree line 187
  14. theorem OAI.CriticalStrip.degree_lt_natDegree_le_pred line 191
  15. theorem OAI.CriticalStrip.projection_natDegree_le line 199
  16. theorem OAI.CriticalStrip.projection_J_degree_lt line 219
  17. theorem OAI.CriticalStrip.homogeneousQ_lower_degree line 257
  18. theorem OAI.CriticalStrip.stieltjes_polynomial_basis line 274
  19. theorem OAI.CriticalStrip.homogeneous_projection_zero line 302
  20. def OAI.CriticalStrip.rootPolynomial line 384
  21. theorem OAI.CriticalStrip.rootPolynomial_monic line 387
  22. theorem OAI.CriticalStrip.rootPolynomial_natDegree line 390
  23. theorem OAI.CriticalStrip.rootPolynomial_degree line 395
  24. abbrev OAI.CriticalStrip.ProjectionSpace line 398
  25. def OAI.CriticalStrip.projectionMap line 401
  26. def OAI.CriticalStrip.projectionRemainder line 411
  27. theorem OAI.CriticalStrip.projectionSpace_finrank line 422