OAI/Analysis/GroupDeterminants/LogSeries.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GroupRingDeterminant.trace_power_derivative line 16
2. lemma OAI.GroupRingDeterminant.hasDerivAt_trace_pow_div line 29
3. lemma OAI.GroupRingDeterminant.summable_trace_pow_div line 42
4. lemma OAI.GroupRingDeterminant.hasDerivAt_trace_logSeries line 54
5. lemma OAI.GroupRingDeterminant.hasDerivAt_trace_logSeries_local line 77
6. lemma OAI.GroupRingDeterminant.norm_pow_div_le_geom line 101
7. lemma OAI.GroupRingDeterminant.summable_pow_div line 108
8. lemma OAI.GroupRingDeterminant.hasSum_pow_div_cfc_log line 114