OAI/Analysis/IrrationalRotation/Product/ProductDenseRange.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.weight_multiplier_selfAdjoint line 14
2. theorem OAI.Invariant233.ProductModel.weightedOperator_injective line 21
3. theorem OAI.Invariant233.ProductModel.weight_multiplier_denseRange line 30
4. theorem OAI.Invariant233.ProductModel.weightedOperator_denseRange line 36
5. theorem OAI.Invariant233.ProductModel.weightedOperator_not_surjective line 47
6. theorem OAI.Invariant233.ProductModel.weightedOperator_range_not_closed line 56
7. theorem OAI.Invariant233.ProductModel.weightedOperator_eigenvector_eq_zero line 64