OAI/NumberTheory/ZetaFive/Arithmetic/LargePrimeWeighted.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Zeta5.Workers.W14.affineGrid line 12
  2. def OAI.Zeta5.Workers.W14.affineLower line 15
  3. def OAI.Zeta5.Workers.W14.affineUpper line 18
  4. theorem OAI.Zeta5.Workers.W14.grid_zero line 21
  5. theorem OAI.Zeta5.Workers.W14.grid_end line 24
  6. theorem OAI.Zeta5.Workers.W14.grid_width line 30
  7. theorem OAI.Zeta5.Workers.W14.grid_strict line 35
  8. theorem OAI.Zeta5.Workers.W14.affine_cell_envelopes line 43
  9. theorem OAI.Zeta5.Workers.W14.affine_envelope_gap line 85
  10. theorem OAI.Zeta5.Workers.W14.affine_envelope_balance line 106
  11. theorem OAI.Zeta5.Workers.W14.affine_piece_darboux line 126
  12. theorem OAI.Zeta5.Workers.W14.weighted_affine_piece_tendsto line 168
  13. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_01 line 178
  14. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_02 line 190
  15. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_03 line 202
  16. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_04 line 214
  17. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_05 line 226
  18. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_06 line 238
  19. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_07 line 250
  20. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_piece_08 line 262
  21. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_tendsto line 274
  22. theorem OAI.Zeta5.Workers.W14.largePrime_weighted_normalized_tendsto line 304