OAI/NumberTheory/PrimeGaps/SiegelBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargePrimeGaps.quadratic_character_im line 11
  2. lemma OAI.LargePrimeGaps.regularSeries_im_zero line 15
  3. lemma OAI.LargePrimeGaps.quadratic_LFunction_im line 37
  4. lemma OAI.LargePrimeGaps.LSeries_character_summable line 46
  5. lemma OAI.LargePrimeGaps.LSeries_character_eq line 52
  6. lemma OAI.LargePrimeGaps.LSeries_zeta_complex_eq line 58
  7. lemma OAI.LargePrimeGaps.LSeries_zetaMul_eq line 65
  8. lemma OAI.LargePrimeGaps.quadratic_LFunction_re_pos_of_one_lt line 75
  9. lemma OAI.LargePrimeGaps.quadratic_LFunction_re_pos_one line 87
  10. lemma OAI.LargePrimeGaps.quadratic_LFunction_re_pos_of_no_root line 104
  11. def OAI.LargePrimeGaps.productCharacter line 126
  12. lemma OAI.LargePrimeGaps.changeLevel_natCast line 130
  13. lemma OAI.LargePrimeGaps.productCharacter_apply line 138
  14. lemma OAI.LargePrimeGaps.productCharacter_quadratic line 149
  15. lemma OAI.LargePrimeGaps.productCharacter_ne_one_of_levels_ne line 154
  16. lemma OAI.LargePrimeGaps.productCharacter_toArithmeticFunction line 170
  17. lemma OAI.LargePrimeGaps.zeta_product_residue_lower line 187
  18. lemma OAI.LargePrimeGaps.zeta_re_neg_near_one line 233
  19. lemma OAI.LargePrimeGaps.LSeries_zeta_complex_summable line 251
  20. lemma OAI.LargePrimeGaps.biquadraticCoefficients_summable line 257
  21. lemma OAI.LargePrimeGaps.LSeries_biquadratic_eq line 266
  22. lemma OAI.LargePrimeGaps.quadratic_residue_lower_of_no_root line 282
  23. lemma OAI.LargePrimeGaps.biquadratic_norm_bound line 304
  24. lemma OAI.LargePrimeGaps.biquadratic_residue_lower_of_root line 322
  25. lemma OAI.LargePrimeGaps.quadratic_siegel_eventual line 357
  26. lemma OAI.LargePrimeGaps.finite_positive_lower line 440
  27. lemma OAI.LargePrimeGaps.LFunction_one_finite_lower line 453
  28. theorem OAI.LargePrimeGaps.quadratic_siegel line 471