OAI/Combinatorics/PolynomialVacuum/Cylinder/ArcPool.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialVacuumCylinder.ArcShape line 7
  2. def OAI.PolynomialVacuumCylinder.ArcShape.word line 10
  3. def OAI.PolynomialVacuumCylinder.ArcShape.mass line 13
  4. theorem OAI.PolynomialVacuumCylinder.ArcShape.word_injective line 15
  5. theorem OAI.PolynomialVacuumCylinder.ArcShape.mass_nonneg line 33
  6. theorem OAI.PolynomialVacuumCylinder.ArcShape.mass_summable line 35
  7. abbrev OAI.PolynomialVacuumCylinder.ArcChoice line 41
  8. def OAI.PolynomialVacuumCylinder.ArcChoice.mass line 44
  9. theorem OAI.PolynomialVacuumCylinder.ArcChoice.mass_nonneg line 48
  10. theorem OAI.PolynomialVacuumCylinder.ArcChoice.mass_summable line 53
  11. theorem OAI.PolynomialVacuumCylinder.summable_fin_product line 61
  12. theorem OAI.PolynomialVacuumCylinder.summable_finite_product line 70
  13. def OAI.PolynomialVacuumCylinder.arcChoiceMajorant line 79
  14. theorem OAI.PolynomialVacuumCylinder.arcChoice_summable line 81