OAI/Combinatorics/StripMass/InverseMoments.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.laguerreExpectation_inverseSum line 13
  2. def OAI.CriticalStrip.minTilt line 42
  3. def OAI.CriticalStrip.minTiltProduct line 43
  4. def OAI.CriticalStrip.inverseSum line 44
  5. lemma OAI.CriticalStrip.minTilt_nonneg line 46
  6. lemma OAI.CriticalStrip.minTilt_le_one line 49
  7. lemma OAI.CriticalStrip.minTilt_eq_zero line 56
  8. lemma OAI.CriticalStrip.minTilt_eq_pair line 60
  9. lemma OAI.CriticalStrip.one_sub_minTilt_le line 67
  10. lemma OAI.CriticalStrip.continuousOn_minTilt line 86
  11. lemma OAI.CriticalStrip.monotoneOn_minTilt line 94
  12. lemma OAI.CriticalStrip.measurable_minTilt line 103
  13. lemma OAI.CriticalStrip.minTiltProduct_nonneg line 105
  14. lemma OAI.CriticalStrip.minTiltProduct_le_one line 108
  15. lemma OAI.CriticalStrip.minTiltProduct_eq_zero line 112
  16. lemma OAI.CriticalStrip.minTiltProduct_pair line 118
  17. lemma OAI.CriticalStrip.laguerreDensity_cons_tilt line 127
  18. lemma OAI.CriticalStrip.continuousOn_minTiltProduct line 137
  19. lemma OAI.CriticalStrip.monotoneOn_minTiltProduct line 143
  20. lemma OAI.CriticalStrip.measurable_minTiltProduct line 152
  21. lemma OAI.CriticalStrip.inverseSum_nonneg line 157
  22. lemma OAI.CriticalStrip.continuousOn_inverseSum line 160
  23. lemma OAI.CriticalStrip.antitoneOn_inverseSum line 166
  24. lemma OAI.CriticalStrip.measurable_inverseSum line 171
  25. lemma OAI.CriticalStrip.integrable_laguerreLaw_inverseSum line 173
  26. lemma OAI.CriticalStrip.integrable_laguerreLaw_minTiltProduct line 177
  27. lemma OAI.CriticalStrip.integrable_laguerreLaw_inverseSum_minTilt line 185
  28. lemma OAI.CriticalStrip.laguerre_inverseSum_minTilt_le line 195
  29. lemma OAI.CriticalStrip.laguerre_indicator_cons_tilt line 211
  30. lemma OAI.CriticalStrip.integral_laguerre_splitMin line 239
  31. lemma OAI.CriticalStrip.integrable_laguerre_splitMin line 260
  32. lemma OAI.CriticalStrip.integrableOn_laguerre_tailInverseSum line 280
  33. lemma OAI.CriticalStrip.weighted_integral_laguerre_inverseSum_minTilt_le line 289
  34. theorem OAI.CriticalStrip.laguerreExpectation_tailInverseSum_le line 300
  35. lemma OAI.CriticalStrip.reciprocal_product_succ line 336
  36. lemma OAI.CriticalStrip.laguerreNormalizer_half_step line 349
  37. lemma OAI.CriticalStrip.laguerreSmallCoefficient_half_one line 359
  38. lemma OAI.CriticalStrip.laguerre_least_inverseQuarter_upper line 370
  39. lemma OAI.CriticalStrip.rpow_quarter_le_one_add line 384
  40. lemma OAI.CriticalStrip.rpow_quarter_le_linear_scaled line 394
  41. lemma OAI.CriticalStrip.laguerre_tailInverseSum_half_upper line 401