OAI/NumberTheory/PrimeGaps/DirichletGrowth.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.discrepancyTail line 35
  2. lemma OAI.LargePrimeGaps.discrepancyTail_integrable line 38
  3. lemma OAI.LargePrimeGaps.discrepancyTail_norm_le line 49
  4. lemma OAI.LargePrimeGaps.discrepancyTail_eq_mellin line 66
  5. lemma OAI.LargePrimeGaps.discrepancyTail_differentiableAt line 81
  6. lemma OAI.LargePrimeGaps.periodic_sum_norm_le line 110
  7. lemma OAI.LargePrimeGaps.char_sum_range_zero line 126
  8. lemma OAI.LargePrimeGaps.char_sum_Icc_norm_le line 143
  9. def OAI.LargePrimeGaps.seriesDiscrepancy line 158
  10. lemma OAI.LargePrimeGaps.measurable_seriesDiscrepancy line 161
  11. def OAI.LargePrimeGaps.regularSeries line 166
  12. lemma OAI.LargePrimeGaps.regularSeries_differentiableAt line 169
  13. lemma OAI.LargePrimeGaps.regularSeries_eq_LSeries_sub line 175
  14. lemma OAI.LargePrimeGaps.sum_Icc_zero_eq line 214
  15. lemma OAI.LargePrimeGaps.weighted_sum_abel line 219
  16. lemma OAI.LargePrimeGaps.cpow_sub_eq_mul_intervalIntegral line 259
  17. lemma OAI.LargePrimeGaps.regularSeries_cutoff line 271
  18. lemma OAI.LargePrimeGaps.sum_cpow_norm_le line 318
  19. lemma OAI.LargePrimeGaps.norm_intervalIntegral_cpow_le line 346
  20. lemma OAI.LargePrimeGaps.regularSeries_norm_cutoff line 362
  21. lemma OAI.LargePrimeGaps.regularSeries_norm_small_power line 424
  22. def OAI.LargePrimeGaps.positiveCoefficients line 454
  23. lemma OAI.LargePrimeGaps.positiveCoefficients_zero line 456
  24. lemma OAI.LargePrimeGaps.positiveCoefficients_norm_le line 458
  25. lemma OAI.LargePrimeGaps.sum_positiveCoefficients line 462
  26. lemma OAI.LargePrimeGaps.LSeries_positiveCoefficients line 468
  27. lemma OAI.LargePrimeGaps.discrepancy_character_bound line 474
  28. lemma OAI.LargePrimeGaps.discrepancy_constant_bound line 479
  29. lemma OAI.LargePrimeGaps.regularSeries_character_eq line 489
  30. lemma OAI.LargePrimeGaps.LFunction_norm_small_power line 509
  31. lemma OAI.LargePrimeGaps.regularSeries_deriv_norm_small_power line 522