OAI/Combinatorics/StripMass/ColumnGeometry.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.columnVertex_adjacent line 12
  2. def OAI.CriticalStrip.diagonalBridge line 17
  3. theorem OAI.CriticalStrip.diagonalBridge_length line 19
  4. theorem OAI.CriticalStrip.diagonalBridge_spec line 22
  5. theorem OAI.CriticalStrip.diagonalBridge_weight line 43
  6. theorem OAI.CriticalStrip.bridgeMass_lower_bound line 51
  7. theorem OAI.CriticalStrip.bridgeMass_pos_of_finite line 62
  8. theorem OAI.CriticalStrip.moment_lower_bound line 65
  9. theorem OAI.CriticalStrip.moment_pos_of_finite line 70
  10. def OAI.CriticalStrip.laguerreDomain line 84
  11. def OAI.CriticalStrip.laguerreWeight line 87
  12. def OAI.CriticalStrip.laguerreDensity line 89
  13. def OAI.CriticalStrip.laguerreNormalizer line 93
  14. def OAI.CriticalStrip.laguerreExpectation line 96
  15. theorem OAI.CriticalStrip.laguerreWeight_pos line 99
  16. theorem OAI.CriticalStrip.measurable_laguerreWeight line 103
  17. theorem OAI.CriticalStrip.laguerreDensity_pos line 107
  18. theorem OAI.CriticalStrip.measurable_laguerreDensity line 117
  19. theorem OAI.CriticalStrip.isOpen_laguerreDomain line 129
  20. theorem OAI.CriticalStrip.laguerreDomain_nonempty line 147
  21. theorem OAI.CriticalStrip.pairKernel_le_right line 155
  22. theorem OAI.CriticalStrip.prod_pair_right line 162
  23. theorem OAI.CriticalStrip.laguerreDensity_le_product line 181
  24. theorem OAI.CriticalStrip.integrableOn_laguerreWeight line 208
  25. theorem OAI.CriticalStrip.integral_laguerreWeight line 213
  26. theorem OAI.CriticalStrip.integrableOn_laguerre_product line 217
  27. theorem OAI.CriticalStrip.integrableOn_laguerreDensity line 225
  28. theorem OAI.CriticalStrip.laguerreNormalizer_pos line 235
  29. theorem OAI.CriticalStrip.integral_laguerre_product line 251
  30. theorem OAI.CriticalStrip.laguerreNormalizer_le_gamma_product line 259
  31. theorem OAI.CriticalStrip.integrableOn_laguerre_inverse_coordinate line 279
  32. theorem OAI.CriticalStrip.integrableOn_laguerre_inverseQuarterSum line 327
  33. def OAI.CriticalStrip.laguerreLaw line 357
  34. theorem OAI.CriticalStrip.laguerreLaw_isProbabilityMeasure line 362
  35. theorem OAI.CriticalStrip.ae_laguerreDomain line 372
  36. theorem OAI.CriticalStrip.integral_laguerreLaw line 379
  37. theorem OAI.CriticalStrip.integrable_laguerreLaw line 392
  38. theorem OAI.CriticalStrip.integrable_laguerreLaw_inverse_coordinate line 404
  39. theorem OAI.CriticalStrip.integrable_laguerreLaw_inverseQuarterSum line 409