OAI/Analysis/IrrationalRotation/Rotation/ContinuousWeightOperatorBridge.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CircleParameterLaws.measurable_complexParameterWeight line 14
2. theorem OAI.Invariant233.CircleParameterLaws.norm_complexParameterWeight_le_one line 18
3. theorem OAI.Invariant233.CircleParameterLaws.continuousWeight_parameter_factor_ae line 23
4. theorem OAI.Invariant233.CircleParameterLaws.parameter_weightedOperator_mem_algebra line 37
5. theorem OAI.Invariant233.CircleParameterLaws.continuousWeight_natural_intertwining line 44
6. theorem OAI.Invariant233.CircleParameterLaws.continuousTransfer_operator_properties line 69