OAI/Analysis/IrrationalRotation/Spectral/ProductPolarDiffuse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.polarConjugate_multiplier_hasCountablyAtomicSpectralType line 14
2. theorem OAI.Invariant233.ProductModel.coefficient_fiber_null_of_orbit_fiber_null line 44
3. theorem OAI.Invariant233.ProductModel.jointEigenspace_polarConjugates_eq_bot_of_null_fibers line 55
4. theorem OAI.Invariant233.ProductModel.fullPolarAlgebra_multiplier_diffuse_of_null_fibers line 93
5. theorem OAI.Invariant233.ProductModel.fullPolarAlgebra_weight_diffuse line 107