OAI/Combinatorics/HoneycombCorridor/VisitRecursion.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumBridge.Corridor.rayLeaves_balance line 11
  2. theorem OAI.PolynomialVacuumBridge.Corridor.rayExits_filter line 17
  3. theorem OAI.PolynomialVacuumBridge.Corridor.rayLeaves_split line 20
  4. theorem OAI.PolynomialVacuumBridge.Corridor.complex_visit_balance line 38
  5. theorem OAI.PolynomialVacuumBridge.Corridor.finite_visit_recursion line 50
  6. theorem OAI.PolynomialVacuumBridge.Corridor.criticalActivity_pos line 85
  7. theorem OAI.PolynomialVacuumBridge.Corridor.Polygon.ccwTurn_cases line 89
  8. theorem OAI.PolynomialVacuumBridge.Corridor.through_cos_pos line 98
  9. theorem OAI.PolynomialVacuumBridge.Corridor.recursion_coefficients_positive line 110
  10. theorem OAI.PolynomialVacuumBridge.Corridor.visitMass_ge_three line 119
  11. theorem OAI.PolynomialVacuumBridge.Corridor.polygons_mono line 144
  12. theorem OAI.PolynomialVacuumBridge.Corridor.visitMass_mono line 148
  13. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_re line 169
  14. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_re_le line 175
  15. theorem OAI.PolynomialVacuumBridge.Corridor.bounded_turn_cos line 180
  16. theorem OAI.PolynomialVacuumBridge.Corridor.convex_wordWeight_re_lower line 191
  17. theorem OAI.PolynomialVacuumBridge.Corridor.visitMass_excursion_upper line 199
  18. theorem OAI.PolynomialVacuumBridge.Corridor.visitMass_excursion_lower line 208