OAI/Combinatorics/HoneycombCorridor/StripDecay.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.lostCut line 11
  2. def OAI.PolynomialVacuumBridge.Corridor.rightIndexMass line 14
  3. theorem OAI.PolynomialVacuumBridge.Corridor.phasedMass_constant_turn line 17
  4. theorem OAI.PolynomialVacuumBridge.Corridor.lostCut_phases line 26
  5. theorem OAI.PolynomialVacuumBridge.Corridor.strip_index_bounds line 52
  6. theorem OAI.PolynomialVacuumBridge.Corridor.position_index line 56
  7. theorem OAI.PolynomialVacuumBridge.Corridor.lostCut_nested line 60
  8. theorem OAI.PolynomialVacuumBridge.Corridor.lostCut_real_lower line 77
  9. theorem OAI.PolynomialVacuumBridge.Corridor.rightIndexMass_step line 89
  10. theorem OAI.PolynomialVacuumBridge.Corridor.rightIndexMass_total_bound line 100
  11. theorem OAI.PolynomialVacuumBridge.Corridor.rightIndexMass_geometric line 107