OAI/Analysis/IrrationalRotation/Spectral/PolarAlgebraSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.finitePolarAlgebra_le_fullPolarAlgebra line 13
2. theorem OAI.Invariant233.not_isDiffuse_of_isAtomic line 20
3. theorem OAI.Invariant233.ProductPolarStructure.finitePolarAlgebra_lt_fullPolarAlgebra line 26
4. theorem OAI.Invariant233.ProductModel.finitePolarAlgebra_lt_fullPolarAlgebra_of_logIntegral line 39