OAI/NumberTheory/ZetaFive/Identities/RiemannSqueeze.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zeta5.Workers.W14.partitionStep line 13
  2. theorem OAI.Zeta5.Workers.W14.partitionStep_eq_on_cell line 16
  3. theorem OAI.Zeta5.Workers.W14.exists_partition_cell line 34
  4. theorem OAI.Zeta5.Workers.W14.partitionStep_envelopes line 40
  5. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_add_adjacent line 50
  6. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_partition line 63
  7. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_partition_bounds line 74
  8. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_partitionStep line 93
  9. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_partitionStep_tendsto line 104
  10. theorem OAI.Zeta5.Workers.W14.weightedPrimeIntervalSum_tendsto_of_darboux line 117