OAI/Analysis/IrrationalRotation/Operators/TracialLogDerivative.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CFCLogSeries.trace_pow_derivative_sum line 13
2. theorem OAI.Invariant233.CFCLogSeries.hasDerivAt_trace_term line 30
3. theorem OAI.Invariant233.CFCLogSeries.hasDerivAt_trace_log_one_sub line 50
4. theorem OAI.Invariant233.CFCLogSeries.hasDerivAt_trace_log_of_scaled_ball line 96
5. theorem OAI.Invariant233.CFCLogSeries.hasDerivAt_trace_log_of_normalization line 128