OAI/NumberTheory/DirichletL/IdealLogDerivative.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.IdealLogDerivative.coeff line 13
  2. theorem OAI.SevenEighths.IdealLogDerivative.norm_coeff_le line 16
  3. theorem OAI.SevenEighths.IdealLogDerivative.norm_coeff_le_two_vonMangoldt line 25
  4. theorem OAI.SevenEighths.IdealLogDerivative.coeff_summable line 31
  5. theorem OAI.SevenEighths.IdealLogDerivative.primePow_coprime_factor line 43
  6. theorem OAI.SevenEighths.IdealLogDerivative.value_mul_coprime line 58
  7. theorem OAI.SevenEighths.IdealLogDerivative.idealDivisors_one line 73
  8. theorem OAI.SevenEighths.IdealLogDerivative.idealDivisors_prime_pow line 78
  9. theorem OAI.SevenEighths.IdealLogDerivative.sum_value_prime_pow line 89
  10. theorem OAI.SevenEighths.IdealLogDerivative.sum_value_mul line 102
  11. theorem OAI.SevenEighths.IdealLogDerivative.sum_value_divisors line 129
  12. theorem OAI.SevenEighths.IdealLogDerivative.value_le_log_norm line 148
  13. theorem OAI.SevenEighths.IdealLogDerivative.weighted_eq_term line 159
  14. theorem OAI.SevenEighths.IdealLogDerivative.weighted_hasDerivAt line 169
  15. theorem OAI.SevenEighths.IdealLogDerivative.log_weighted_hasSum line 179
  16. theorem OAI.SevenEighths.IdealLogDerivative.mangoldt_weighted_summable_norm line 197
  17. theorem OAI.SevenEighths.IdealLogDerivative.mangoldt_series_eq_LSeries line 206
  18. theorem OAI.SevenEighths.IdealLogDerivative.mulFiber_value_sum line 222
  19. theorem OAI.SevenEighths.IdealLogDerivative.coeff_LSeries_mul_series line 235
  20. theorem OAI.SevenEighths.IdealLogDerivative.coeff_LSeries_eq_neg_logDeriv line 277
  21. theorem OAI.SevenEighths.IdealLogDerivative.coeff_LSeries_eq_neg_logDeriv_of_eq line 283