OAI/Analysis/IrrationalRotation/Operators/TracialLogNormSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.CFCLogSeries.hasDerivAt_re_trace_log_normSquare_of_normalization line 13
2. theorem OAI.Invariant233.CFCLogSeries.hasDerivAt_re_trace_log_normSquare line 31