OAI/Analysis/IrrationalRotation/Model/ProductTailDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.ProductModel.Prefix line 11
2. abbrev OAI.Invariant233.ProductModel.Tail line 12
3. def OAI.Invariant233.ProductModel.prefixMeasure line 14
4. def OAI.Invariant233.ProductModel.tailMeasure line 17
5. def OAI.Invariant233.ProductModel.splitCoordinates line 20
6. def OAI.Invariant233.ProductModel.tailCoordinates line 23
7. def OAI.Invariant233.ProductModel.prefixTailDensity line 25