OAI/Combinatorics/StripMass/QuarticIntegrals.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.quartic_weighted_integral_sqrt line 13
  2. def OAI.CriticalStrip.minusBranch line 25
  3. theorem OAI.CriticalStrip.minusBranch_zero line 27
  4. theorem OAI.CriticalStrip.transformed_omega line 43
  5. theorem OAI.CriticalStrip.omega_resolvent line 58
  6. theorem OAI.CriticalStrip.stieltjes_omega line 85
  7. def OAI.CriticalStrip.lBranch line 111
  8. theorem OAI.CriticalStrip.stieltjes_lBranch line 113
  9. def OAI.CriticalStrip.squareWeight line 128
  10. theorem OAI.CriticalStrip.lBranch_mul_omega line 130
  11. theorem OAI.CriticalStrip.scaled_cauchy_Ioi line 149
  12. def OAI.CriticalStrip.squareUniformizer line 160
  13. theorem OAI.CriticalStrip.squareUniformizer_deriv line 162
  14. theorem OAI.CriticalStrip.squareUniformizer_inj line 170
  15. theorem OAI.CriticalStrip.squareUniformizer_image line 178
  16. theorem OAI.CriticalStrip.squareWeight_uniformizer line 197
  17. theorem OAI.CriticalStrip.transformed_squareWeight line 209
  18. theorem OAI.CriticalStrip.squareWeight_resolvent line 219
  19. theorem OAI.CriticalStrip.stieltjes_omega_square line 251
  20. theorem OAI.CriticalStrip.integrableOn_lBranch_omega line 282
  21. theorem OAI.CriticalStrip.integrableOn_continuous_mul line 301
  22. def OAI.CriticalStrip.realStieltjes line 309
  23. def OAI.CriticalStrip.offCut line 312
  24. theorem OAI.CriticalStrip.integrableOn_stieltjes line 314
  25. theorem OAI.CriticalStrip.integrableOn_polynomial_weight line 321
  26. theorem OAI.CriticalStrip.realStieltjes_const_mul line 326
  27. theorem OAI.CriticalStrip.realStieltjes_add line 331
  28. theorem OAI.CriticalStrip.realStieltjes_mul_variable line 339
  29. theorem OAI.CriticalStrip.polynomial_mul_realStieltjes line 356
  30. theorem OAI.CriticalStrip.abs_mul_le_one line 395
  31. theorem OAI.CriticalStrip.offCut_of_abs_large line 400
  32. theorem OAI.CriticalStrip.norm_realStieltjes_le line 408