OAI/NumberTheory/PrimeGaps/TaylorBounds.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargePrimeGaps.power_series_tail_bound line 39
  2. lemma OAI.LargePrimeGaps.residue_lower_bound_of_taylor line 59
  3. def OAI.LargePrimeGaps.signedTaylorCoeff line 102
  4. lemma OAI.LargePrimeGaps.signedTaylorCoeff_hasSum line 105
  5. lemma OAI.LargePrimeGaps.signedTaylorCoeff_norm_bound line 126
  6. lemma OAI.LargePrimeGaps.signedTaylorCoeff_residue line 138
  7. lemma OAI.LargePrimeGaps.signedTaylorCoeff_pole line 151
  8. lemma OAI.LargePrimeGaps.signedTaylorCoeff_sub line 168
  9. lemma OAI.LargePrimeGaps.signedTaylorCoeff_LSeries_nonneg line 177
  10. lemma OAI.LargePrimeGaps.LSeries_two_re_ge_one line 190
  11. lemma OAI.LargePrimeGaps.signedTaylorCoeff_regular_nonneg line 200
  12. lemma OAI.LargePrimeGaps.residue_polynomial_lower line 220
  13. def OAI.LargePrimeGaps.zetaRegular line 296
  14. lemma OAI.LargePrimeGaps.zetaRegular_differentiableAt line 299
  15. lemma OAI.LargePrimeGaps.zetaRegular_eq_of_one_lt_re line 303
  16. lemma OAI.LargePrimeGaps.poleRemovedZeta_eq line 309
  17. lemma OAI.LargePrimeGaps.zetaRegular_eq line 330
  18. lemma OAI.LargePrimeGaps.regularSeries_norm_simple line 340
  19. lemma OAI.LargePrimeGaps.closedBall_two_re_norm line 350
  20. lemma OAI.LargePrimeGaps.zetaRegular_norm_le_seventeen line 359
  21. lemma OAI.LargePrimeGaps.LFunction_norm_polynomial line 369
  22. def OAI.LargePrimeGaps.regularizedZetaProduct line 382
  23. lemma OAI.LargePrimeGaps.regularizedZetaProduct_differentiableOn line 385
  24. lemma OAI.LargePrimeGaps.regularizedZetaProduct_eq line 395
  25. lemma OAI.LargePrimeGaps.regularizedZetaProduct_bound line 400
  26. def OAI.LargePrimeGaps.PrimePowerEq line 451
  27. lemma OAI.LargePrimeGaps.PrimePowerEq.refl line 454
  28. lemma OAI.LargePrimeGaps.PrimePowerEq.mul line 456
  29. lemma OAI.LargePrimeGaps.primePower_zeta line 468
  30. lemma OAI.LargePrimeGaps.primePower_one line 472
  31. lemma OAI.LargePrimeGaps.primePower_character line 482
  32. lemma OAI.LargePrimeGaps.arithmetic_convolution_nonneg line 486
  33. def OAI.LargePrimeGaps.biquadraticCoefficients line 491
  34. lemma OAI.LargePrimeGaps.biquadraticCoefficients_multiplicative line 496
  35. lemma OAI.LargePrimeGaps.biquadraticCoefficients_comm line 503
  36. lemma OAI.LargePrimeGaps.biquadratic_prime_zero line 510
  37. lemma OAI.LargePrimeGaps.biquadratic_prime_one line 525
  38. lemma OAI.LargePrimeGaps.biquadratic_prime_neg_one line 544
  39. lemma OAI.LargePrimeGaps.biquadraticCoefficients_nonneg line 564