OAI/Combinatorics/HoneycombCorridor/RaySeparation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.positiveWordMass line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.phasedWordMass line 12
  3. def OAI.PolynomialVacuumBridge.Corridor.phase line 14
  4. theorem OAI.PolynomialVacuumBridge.Corridor.phase_norm line 16
  5. theorem OAI.PolynomialVacuumBridge.Corridor.phase_add line 19
  6. theorem OAI.PolynomialVacuumBridge.Corridor.phase_zero line 22
  7. theorem OAI.PolynomialVacuumBridge.Corridor.wordWeight_norm line 24
  8. theorem OAI.PolynomialVacuumBridge.Corridor.positiveWordMass_nonneg line 29
  9. theorem OAI.PolynomialVacuumBridge.Corridor.phasedWordMass_norm_le line 32
  10. theorem OAI.PolynomialVacuumBridge.Corridor.positiveWordMass_mono line 36
  11. def OAI.PolynomialVacuumBridge.Corridor.rayContraction line 40
  12. theorem OAI.PolynomialVacuumBridge.Corridor.rayContraction_range line 43
  13. theorem OAI.PolynomialVacuumBridge.Corridor.separated_rays_contract line 55