OAI/NumberTheory/DirichletL/Mellin/SixthPowerAverage.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SixthPowerAverage.exists_averaging_test line 84
  2. lemma OAI.SixthPowerAverage.prime_coprime_span_iff line 141
  3. lemma OAI.SixthPowerAverage.squarefree_sixth_row_coprime line 147
  4. theorem OAI.SixthPowerAverage.idealRowSum_sixth_eq_coprime_sum line 161
  5. def OAI.SixthPowerAverage.averagingRows line 190
  6. theorem OAI.SixthPowerAverage.mem_averagingRows line 192
  7. theorem OAI.SixthPowerAverage.averagingRows_card line 199
  8. theorem OAI.SixthPowerAverage.averagingRows_power_norm line 204
  9. theorem OAI.SixthPowerAverage.average_tsum_eq_finite line 214
  10. theorem OAI.SixthPowerAverage.average_tsum_cauchy line 232
  11. theorem OAI.SixthPowerAverage.average_remainder_small_power line 244
  12. theorem OAI.SixthPowerAverage.totient_sum_normalized_bound line 288
  13. theorem OAI.SixthPowerAverage.outside_totient_moebius_bound line 317
  14. def OAI.SixthPowerAverage.weightedMoebius line 428
  15. def OAI.SixthPowerAverage.outsideWeight line 431
  16. def OAI.SixthPowerAverage.weightedCoeff line 435
  17. theorem OAI.SixthPowerAverage.totientDensity_norm_le_one line 439
  18. theorem OAI.SixthPowerAverage.weightedMoebius_norm_le_one line 453
  19. theorem OAI.SixthPowerAverage.weightedMoebius_zero line 459
  20. theorem OAI.SixthPowerAverage.outsideWeight_norm_le_one line 465
  21. theorem OAI.SixthPowerAverage.outsideWeight_zero line 473
  22. theorem OAI.SixthPowerAverage.weightedCoeff_zero line 481
  23. theorem OAI.SixthPowerAverage.weightedCoeff_norm_bound line 491
  24. theorem OAI.SixthPowerAverage.weightedCoeff_LSeriesSummable line 511
  25. theorem OAI.SixthPowerAverage.weightedCoeff_hasSum line 520
  26. theorem OAI.SixthPowerAverage.ideal_weighted_hasSum line 549
  27. def OAI.SixthPowerAverage.weightedCompactSum line 588
  28. theorem OAI.SixthPowerAverage.weightedCompactSum_hasSum line 592
  29. theorem OAI.SixthPowerAverage.weightedCompactSum_inv_eq line 605
  30. theorem OAI.SixthPowerAverage.weightedCompactSum_eq_ideal_tsum line 613
  31. theorem OAI.SixthPowerAverage.weightedCompactSum_isBigO_of_theta line 622
  32. theorem OAI.SixthPowerAverage.weightedCompactMellin_analytic_of_theta line 643
  33. theorem OAI.SixthPowerAverage.weightedCompactMellin_eq_series line 669
  34. theorem OAI.SixthPowerAverage.weightedCompactMellin_analytic line 682
  35. theorem OAI.SixthPowerAverage.ideal_totient_moebius_bound line 701