OAI/Combinatorics/PolynomialVacuum/Bridge/VisitNestingComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.faceCount_cases line 8
  2. theorem OAI.PolynomialVacuumBridge.Corridor.through_power_ratio line 20
  3. def OAI.PolynomialVacuumBridge.Corridor.lowThroughRatio line 29
  4. def OAI.PolynomialVacuumBridge.Corridor.highThroughRatio line 30
  5. theorem OAI.PolynomialVacuumBridge.Corridor.lowThroughRatio_pos line 32
  6. theorem OAI.PolynomialVacuumBridge.Corridor.highThroughRatio_pos line 38
  7. theorem OAI.PolynomialVacuumBridge.Corridor.through_coefficient_two_ratios line 41
  8. def OAI.PolynomialVacuumBridge.Corridor.visitLowerConstant line 65
  9. def OAI.PolynomialVacuumBridge.Corridor.visitUpperConstant line 66
  10. theorem OAI.PolynomialVacuumBridge.Corridor.visit_constants_positive line 68
  11. theorem OAI.PolynomialVacuumBridge.Corridor.through_coefficient_bounds line 73
  12. theorem OAI.PolynomialVacuumBridge.Corridor.visitMass_incident_comparison line 94