OAI/NumberTheory/ZetaFive/Identities/WeightedPNT.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zeta5.Workers.W14.primeIntervalSum line 14
  2. theorem OAI.Zeta5.Workers.W14.mem_primeInterval_iff line 17
  3. theorem OAI.Zeta5.Workers.W14.primeIntervalSum_eq_theta_sub line 23
  4. theorem OAI.Zeta5.Workers.W14.theta_scaled_tendsto line 32
  5. theorem OAI.Zeta5.Workers.W14.primeIntervalSum_scaled_tendsto line 45
  6. def OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum line 56
  7. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_const line 60
  8. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_const_tendsto line 66
  9. def OAI.Zeta5.Workers.W14.finiteStepPrimeSum line 79
  10. theorem OAI.Zeta5.Workers.W14.finiteStepPrimeSum_tendsto line 83