OAI/Combinatorics/PolynomialVacuum/Cylinder/BridgeMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinderMassBound line 7
2. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinder_bridge_finite_sum_bound line 9
3. abbrev OAI.PolynomialVacuumBridge.Corridor.BridgeWord.CylinderBridge line 54
4. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinder_bridge_mass_summable line 56
5. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.cylinder_bridge_mass_le line 66