OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Epsilon.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.SourcePrimeBands.epsilon line 13
  2. def OAI.OrdinaryCorrelations.SourcePrimeBands.eta line 14
  3. def OAI.OrdinaryCorrelations.SourcePrimeBands.corePrimes line 16
  4. def OAI.OrdinaryCorrelations.SourcePrimeBands.centerPrimes line 20
  5. def OAI.OrdinaryCorrelations.SourcePrimeBands.coreMass line 24
  6. def OAI.OrdinaryCorrelations.SourcePrimeBands.centerMass line 25
  7. def OAI.OrdinaryCorrelations.SourcePrimeBands.primeHarmonic line 27
  8. def OAI.OrdinaryCorrelations.SourcePrimeBands.Support.reciprocalHom line 34
  9. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.Support.reciprocal_prime_norm line 39
  10. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.Support.harmonic_le_finite_euler line 45
  11. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.prime_set_eq line 74
  12. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.prime_set_zero_eq line 84
  13. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.logPrimeReciprocal_abel line 91
  14. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.logPrimeReciprocal_le line 131
  15. def OAI.OrdinaryCorrelations.SourcePrimeBands.rpowHom line 176
  16. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.zeta_rpow_le line 181
  17. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.prime_rpow_sum_log_bound line 204
  18. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.rpow_reciprocal_error line 238
  19. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.primeHarmonic_upper line 253
  20. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.log_inv_one_sub_le line 296
  21. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.prime_reciprocal_square_le line 307
  22. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.primeHarmonic_lower line 320
  23. theorem OAI.OrdinaryCorrelations.SourcePrimeBands.primeHarmonic_loglog_bounded line 350
  24. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.primeHarmonic_exp_rpow_ratio line 365
  25. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.primeHarmonic_exp_sub line 385
  26. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.coreMass_eq line 421
  27. lemma OAI.OrdinaryCorrelations.SourcePrimeBands.centerMass_eq line 431
  28. theorem OAI.OrdinaryCorrelations.SourcePrimeBands.source_prime_bands line 438