OAI/Combinatorics/StripMass/QuarterMoments.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.laguerre_inverseQuarterSum_upper line 13
  2. lemma OAI.CriticalStrip.reciprocal_product_two_succ line 66
  3. lemma OAI.CriticalStrip.laguerreNormalizer_one_step line 80
  4. lemma OAI.CriticalStrip.laguerreNormalizer_one_ratio line 90
  5. lemma OAI.CriticalStrip.minTiltProduct_lower line 98
  6. lemma OAI.CriticalStrip.laguerre_minTiltProduct_lower line 114
  7. lemma OAI.CriticalStrip.laguerre_minTiltProduct_two_lower line 133
  8. lemma OAI.CriticalStrip.smallCoordinate_scale_lower line 151
  9. theorem OAI.CriticalStrip.laguerre_least_inverseQuarter_lower line 166
  10. lemma OAI.CriticalStrip.orderedPairProduct_snoc line 250
  11. lemma OAI.CriticalStrip.gammaSchurProduct_snoc line 267
  12. lemma OAI.CriticalStrip.laguerreNormalizer_snoc_product line 275
  13. lemma OAI.CriticalStrip.prod_nat_sub line 290
  14. lemma OAI.CriticalStrip.prod_nat_add line 297
  15. lemma OAI.CriticalStrip.laguerreNormalizer_max_half_ratio line 304
  16. lemma OAI.CriticalStrip.choose_double_le_four_pow line 321
  17. lemma OAI.CriticalStrip.elementary_exp_half_bound line 327
  18. theorem OAI.CriticalStrip.laguerreLaw_max_half_uniform line 355
  19. lemma OAI.CriticalStrip.laguerreLaw_cutoff_half_uniform line 379
  20. def OAI.CriticalStrip.referenceUpperConstant line 402
  21. lemma OAI.CriticalStrip.referenceUpperConstant_pos line 404