OAI/Combinatorics/PolynomialVacuum/Cylinder/ArcDecay.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.summable_height_tail_tendsto line 13
  2. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinderHeightTail line 29
  3. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinderHeightMass line 31
  4. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinder_height_tail_tendsto line 34
  5. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinder_height_mass_tendsto line 39
  6. def OAI.PolynomialVacuumBridge.Corridor.ArchWord.height line 56
  7. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.layer_lt_height line 59
  8. def OAI.PolynomialVacuumBridge.Corridor.ArchWord.CylinderSafe line 66
  9. abbrev OAI.PolynomialVacuumBridge.Corridor.ArchWord.CylinderArch line 68
  10. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.cylinder_arch_mass_summable line 70
  11. def OAI.PolynomialVacuumBridge.Corridor.ArchWord.cylinderHeightTail line 73
  12. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.cylinder_height_tail_tendsto line 76