OAI/Analysis/IrrationalRotation/Model/ProductPrefixDomination.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.OrderedProductCoupling.PrefixIndex line 12
2. abbrev OAI.Invariant233.OrderedProductCoupling.TailIndex line 13
3. abbrev OAI.Invariant233.OrderedProductCoupling.PrefixPairs line 14
4. abbrev OAI.Invariant233.OrderedProductCoupling.TailValues line 15
5. def OAI.Invariant233.OrderedProductCoupling.assemblePrefixPair line 17
6. def OAI.Invariant233.OrderedProductCoupling.prefixPairLaw line 21
7. def OAI.Invariant233.OrderedProductCoupling.prefixPairsLaw line 25
8. def OAI.Invariant233.OrderedProductCoupling.leftTailLaw line 29
9. def OAI.Invariant233.OrderedProductCoupling.baseTailLaw line 33
10. def OAI.Invariant233.OrderedProductCoupling.prefixReferenceLaw line 36
11. def OAI.Invariant233.OrderedProductCoupling.prefixReferencePairLaw line 41