OAI/Combinatorics/StripMass/LaguerreTails.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.laguerreLaw_small_coordinate_le line 13
  2. theorem OAI.CriticalStrip.laguerreLaw_small_coordinate_power_bound line 25
  3. theorem OAI.CriticalStrip.integrable_inverse_of_small_tail line 39
  4. theorem OAI.CriticalStrip.integrable_laguerreLaw_inverse_coordinate_full line 69
  5. theorem OAI.CriticalStrip.laguerre_inverse_bound_normalizer_ratio line 87
  6. theorem OAI.CriticalStrip.pairProduct_snoc line 109
  7. theorem OAI.CriticalStrip.laguerreDensity_snoc line 126
  8. theorem OAI.CriticalStrip.laguerreDomain_of_snoc line 134
  9. theorem OAI.CriticalStrip.laguerreDensity_snoc_le line 146
  10. theorem OAI.CriticalStrip.integral_fin_snoc_eq line 166
  11. theorem OAI.CriticalStrip.integrable_fin_snoc line 173
  12. theorem OAI.CriticalStrip.laguerreLaw_measureReal line 179
  13. theorem OAI.CriticalStrip.laguerreLargestIntegral_le line 188
  14. theorem OAI.CriticalStrip.laguerreLaw_max_tail_le line 234
  15. theorem OAI.CriticalStrip.laguerreWeight_tail_exp_bound line 245
  16. theorem OAI.CriticalStrip.laguerreLaw_max_tail_exp_bound line 284
  17. def OAI.CriticalStrip.orderedPairKernel line 300
  18. lemma OAI.CriticalStrip.orderedPairKernel_nonneg line 302
  19. lemma OAI.CriticalStrip.orderedPairKernel_eq line 307
  20. lemma OAI.CriticalStrip.orderedPairKernel_eq_zero line 311
  21. lemma OAI.CriticalStrip.pairKernel_cross line 317
  22. lemma OAI.CriticalStrip.orderedPairKernel_logSupermodular line 341
  23. lemma OAI.CriticalStrip.product_coordinate_modular line 362
  24. lemma OAI.CriticalStrip.association_finite_product line 376
  25. def OAI.CriticalStrip.coordinateBox line 402