OAI/Combinatorics/HoneycombCorridor/LateralMass.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.reachesRight line 11
  2. def OAI.PolynomialVacuumBridge.Corridor.rightDistanceMass line 14
  3. def OAI.PolynomialVacuumBridge.Corridor.tailRate line 18
  4. def OAI.PolynomialVacuumBridge.Corridor.tailConstant line 19
  5. theorem OAI.PolynomialVacuumBridge.Corridor.tailRate_pos line 22
  6. theorem OAI.PolynomialVacuumBridge.Corridor.tailConstant_pos line 26
  7. theorem OAI.PolynomialVacuumBridge.Corridor.rightDistanceMass_mono line 32
  8. theorem OAI.PolynomialVacuumBridge.Corridor.rightDistanceMass_geometric line 40
  9. theorem OAI.PolynomialVacuumBridge.Corridor.rightDistanceMass_exp line 65
  10. theorem OAI.PolynomialVacuumBridge.Corridor.reachesRight_mirror line 105
  11. theorem OAI.PolynomialVacuumBridge.Corridor.lateralMass_le_sides line 116
  12. theorem OAI.PolynomialVacuumBridge.Corridor.lateralMass_exp line 139