OAI/Combinatorics/PolynomialVacuum/Cylinder/LimitFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumCylinder.codedWeight_factor line 9
  2. theorem OAI.PolynomialVacuumCylinder.limitingCodedWeight_factor line 27
  3. def OAI.PolynomialVacuumCylinder.joinCode line 37
  4. def OAI.PolynomialVacuumCylinder.halfCodeEquiv line 39
  5. theorem OAI.PolynomialVacuumCylinder.cut_join_false line 47
  6. theorem OAI.PolynomialVacuumCylinder.cut_join_true line 51
  7. def OAI.PolynomialVacuumCylinder.lowerAmplitude line 55
  8. def OAI.PolynomialVacuumCylinder.upperAmplitude line 57
  9. theorem OAI.PolynomialVacuumCylinder.limitingCodedWeight_norm_summable line 60
  10. theorem OAI.PolynomialVacuumCylinder.arcLimit_factor line 66