OAI/Combinatorics/HadwigerCounterexample/OffsetFourierBounds.lean
8 declarations, 0 contain sorry, 0 declared as axioms
Offset Fourier Bounds
- def
OAI.HadwigerCounterexample.chantline 13 - def
OAI.HadwigerCounterexample.coupledBline 19 - theorem
OAI.HadwigerCounterexample.coupledB_injline 29 - theorem
OAI.HadwigerCounterexample.tupleB_commline 43 - abbrev
OAI.HadwigerCounterexample.Bazaar.Salesline 51 - def
OAI.HadwigerCounterexample.Bazaar.discardline 54 - theorem
OAI.HadwigerCounterexample.Bazaar.beat_oneline 58 - theorem
OAI.HadwigerCounterexample.Bazaar.beat_mixline 127