OAI/Analysis/IrrationalRotation/Product/ProductPowerIdentity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.WeightedShift.fieldShift_one_pow line 13
2. theorem OAI.Invariant233.WeightedShift.fieldOperator_pow_eq_shift_mul_of_coeff line 22
3. theorem OAI.Invariant233.ProductModel.ae_weight_orbit_product_eq_cocycleVersion line 51
4. theorem OAI.Invariant233.ProductModel.weightedOperator_pow_coordinate_ae line 72
5. theorem OAI.Invariant233.ProductModel.weightedOperator_pow_eq_shift_mul_positiveCocycleMultiplier line 100
6. theorem OAI.Invariant233.ProductModel.positiveCocycleMultiplier_mem_factor line 116