OAI/Combinatorics/PolynomialVacuum/Cylinder/ArcMajorant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumCylinder.ArcChoice.length line 11
  2. def OAI.PolynomialVacuumCylinder.arcChoiceLength line 15
  3. def OAI.PolynomialVacuumCylinder.arcChoiceMass line 16
  4. def OAI.PolynomialVacuumCylinder.arcChoiceTail line 17
  5. theorem OAI.PolynomialVacuumCylinder.arcChoiceMajorant_nonneg line 20
  6. theorem OAI.PolynomialVacuumCylinder.arcChoice_tail_tendsto line 23
  7. theorem OAI.PolynomialVacuumCylinder.arcChoice_tail_summable line 27
  8. theorem OAI.PolynomialVacuumCylinder.ArcSystem.word_le_code_length line 35
  9. theorem OAI.PolynomialVacuumCylinder.ArcSystem.sum_norm_le line 40
  10. theorem OAI.PolynomialVacuumCylinder.ArcSystem.sum_norm_large_le line 47
  11. theorem OAI.PolynomialVacuumAlgebra.physicalTransfer_powers_bounded line 62