OAI/Analysis/IrrationalRotation/Product/ProductDiffuse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.ProductModel.borelSetProjection line 14
2. theorem OAI.Invariant233.ProductModel.borelSetProjection_mem line 21
3. theorem OAI.Invariant233.ProductModel.borelSetProjection_isStarProjection line 25
4. theorem OAI.Invariant233.ProductModel.vectorTrace_borelSetProjection line 44
5. theorem OAI.Invariant233.ProductModel.borelSetProjection_joint_kernel line 50
6. theorem OAI.Invariant233.ProductModel.factor_isDiffuse line 74
7. theorem OAI.Invariant233.ProductModel.factor_isTypeII1FactorWithVector line 119