OAI/Combinatorics/PolynomialVacuum/Bridge/HalfPlaneArchMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PolynomialVacuumBridge.Corridor.ArchWord line 9
2. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.ext line 17
3. def OAI.PolynomialVacuumBridge.Corridor.ArchWord.mass line 23
4. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.mass_pos line 24
5. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.finite_sum_bound line 26
6. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.mass_summable line 65
7. theorem OAI.PolynomialVacuumBridge.Corridor.ArchWord.mass_le line 68