OAI/Combinatorics/StripMass/TailIntegrals.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.integral_le_of_power_tail line 13
  2. theorem OAI.CriticalStrip.integrable_of_power_tail line 69
  3. theorem OAI.CriticalStrip.integral_inverse_le_of_small_tail line 103
  4. theorem OAI.CriticalStrip.laguerre_inverse_bound_of_small_coordinate_bound line 147
  5. theorem OAI.CriticalStrip.laguerreDomain_cons_iff line 165
  6. theorem OAI.CriticalStrip.pairProduct_cons line 172
  7. theorem OAI.CriticalStrip.laguerreDensity_cons line 190
  8. theorem OAI.CriticalStrip.laguerreDensity_succ_parameter line 198
  9. theorem OAI.CriticalStrip.laguerreDensity_cons_le line 209
  10. def OAI.CriticalStrip.laguerreCut line 232
  11. def OAI.CriticalStrip.laguerreCutIntegral line 235
  12. theorem OAI.CriticalStrip.measurableSet_laguerreCut line 238
  13. theorem OAI.CriticalStrip.laguerreCut_zero line 245
  14. theorem OAI.CriticalStrip.integral_fin_cons_eq line 249
  15. theorem OAI.CriticalStrip.integrable_fin_cons line 256
  16. theorem OAI.CriticalStrip.integral_Ioo_rpow_sub_one line 262
  17. theorem OAI.CriticalStrip.integrable_laguerreCut_indicator line 268
  18. theorem OAI.CriticalStrip.laguerreCut_indicator_nonneg line 273
  19. theorem OAI.CriticalStrip.laguerreCutIntegral_succ_le line 282
  20. theorem OAI.CriticalStrip.laguerreCutIntegral_le_product line 322
  21. def OAI.CriticalStrip.laguerreDimension line 343
  22. theorem OAI.CriticalStrip.laguerreDimension_succ line 345
  23. theorem OAI.CriticalStrip.product_coordinate_power_quotient line 350
  24. theorem OAI.CriticalStrip.laguerreCutIntegral_le_normalizer_ratio line 361
  25. theorem OAI.CriticalStrip.laguerreCut_eq_coordinate_cut line 368
  26. theorem OAI.CriticalStrip.laguerreLaw_small_coordinate_eq line 378
  27. theorem OAI.CriticalStrip.laguerreLaw_small_coordinate_le_normalizer_ratio line 391
  28. def OAI.CriticalStrip.laguerreSmallCoefficient line 406
  29. theorem OAI.CriticalStrip.laguerreSmallCoefficient_pos line 410
  30. theorem OAI.CriticalStrip.laguerreDimension_pos line 415