OAI/Analysis/IrrationalRotation/Couplings/ProductConditionalData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.ProductModel.sourceUnitVector line 15
2. def OAI.Invariant233.ProductModel.sourceLeftVector line 17
3. def OAI.Invariant233.ProductModel.sourceRightVector line 20
4. def OAI.Invariant233.ProductModel.sourceLeftCocycle line 23
5. def OAI.Invariant233.ProductModel.sourceRightCocycle line 26
6. theorem OAI.Invariant233.ProductModel.conditionalData_of_sourceTail line 29