OAI/Analysis/IrrationalRotation/Operators/TracialPowerDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.TracialState.power_derivative_term line 12
2. theorem OAI.Invariant233.TracialState.power_derivative_sum line 21
3. theorem OAI.Invariant233.TracialState.hasDerivAt_power line 33
4. theorem OAI.Invariant233.TracialState.hasDerivAt_re_power line 44
5. theorem OAI.Invariant233.TracialState.hasDerivAt_logarithmic_power line 51
6. theorem OAI.Invariant233.TracialState.hasDerivAt_logarithmic_partialSum line 61