OAI/Combinatorics/PolynomialVacuum/Bridge/BridgeWordMass.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.mass line 7
2. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.mass_one line 8
3. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.mass_mul line 9
4. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.mass_pos line 10
5. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.mass_prod line 11
6. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.massConstant line 14
7. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cos_sigma_pos line 16
8. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.massConstant_pos line 19
9. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.fixed_height_mass_bound line 21
10. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.bounded_height_mass_bound line 74