OAI/NumberTheory/GaussianMoat/PrimeMass.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianMoat.PrimeLogMass.residue_real_series line 11
  2. theorem OAI.GaussianMoat.PrimeLogMass.residue_moment_limit line 26
  3. def OAI.GaussianMoat.PrimeLogMass.betaMoment line 57
  4. lemma OAI.GaussianMoat.PrimeLogMass.betaMoment_pos line 59
  5. lemma OAI.GaussianMoat.PrimeLogMass.betaMoment_succ line 66
  6. def OAI.GaussianMoat.PrimeLogMass.windowPolynomialAux line 103
  7. lemma OAI.GaussianMoat.PrimeLogMass.windowPolynomialAux_eval line 107
  8. def OAI.GaussianMoat.PrimeLogMass.windowPolynomial line 112
  9. lemma OAI.GaussianMoat.PrimeLogMass.windowPolynomial_eval line 114
  10. lemma OAI.GaussianMoat.PrimeLogMass.windowPolynomial_nonpos line 118
  11. lemma OAI.GaussianMoat.PrimeLogMass.betaMoment_quadratic line 127
  12. lemma OAI.GaussianMoat.PrimeLogMass.windowPolynomial_integral_pos line 143
  13. lemma OAI.GaussianMoat.PrimeLogMass.polynomial_integral_coeff line 153
  14. theorem OAI.GaussianMoat.PrimeLogMass.residue_polynomial_moment_limit line 162
  15. lemma OAI.GaussianMoat.PrimeLogMass.residue_summable line 176
  16. lemma OAI.GaussianMoat.PrimeLogMass.laplace_power line 181
  17. lemma OAI.GaussianMoat.PrimeLogMass.laplace_term line 189
  18. lemma OAI.GaussianMoat.PrimeLogMass.polynomial_laplace_series line 198
  19. lemma OAI.GaussianMoat.PrimeLogMass.polynomial_laplace_summable line 218
  20. lemma OAI.GaussianMoat.PrimeLogMass.windowPolynomial_le_one line 234
  21. lemma OAI.GaussianMoat.PrimeLogMass.exp_window_lower line 252
  22. lemma OAI.GaussianMoat.PrimeLogMass.exp_window_upper line 263
  23. def OAI.GaussianMoat.PrimeLogMass.windowIndices line 276
  24. lemma OAI.GaussianMoat.PrimeLogMass.mem_windowIndices line 280
  25. lemma OAI.GaussianMoat.PrimeLogMass.laplace_window_nonpos line 285
  26. lemma OAI.GaussianMoat.PrimeLogMass.window_mass_dominates line 307
  27. theorem OAI.GaussianMoat.PrimeLogMass.eventually_residue_window_mass line 340
  28. theorem OAI.GaussianMoat.PrimeLogMass.eventually_prime_window_mass line 360
  29. theorem OAI.GaussianMoat.irreducible_of_prime_norm line 385
  30. theorem OAI.GaussianMoat.exists_split_factor line 405