OAI/NumberTheory/DirichletL/Hecke/Boundary.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeBoundary.re_log_comb_nonneg line 16
  2. theorem OAI.SevenEighths.HeckeBoundary.re_log_cpow_comb_nonneg line 38
  3. theorem OAI.SevenEighths.HeckeBoundary.summable_neg_log_euler line 60
  4. theorem OAI.SevenEighths.HeckeBoundary.exp_log_euler_eq_series line 65
  5. def OAI.SevenEighths.HeckeBoundary.PrimeTriple line 76
  6. theorem OAI.SevenEighths.HeckeBoundary.re_log_weighted_comb_nonneg line 81
  7. theorem OAI.SevenEighths.HeckeBoundary.norm_series_product_ge_one line 99
  8. theorem OAI.SevenEighths.HeckeBoundary.square_unitInvariant line 121
  9. theorem OAI.SevenEighths.HeckeBoundary.ofResidue_primeTriple line 126
  10. theorem OAI.SevenEighths.HeckeBoundary.norm_residue_series_product_ge_one line 149
  11. theorem OAI.SevenEighths.HeckeBoundary.horizontal_isBigO_of_zero line 160
  12. theorem OAI.SevenEighths.HeckeBoundary.horizontal_isBigO_one line 170
  13. theorem OAI.SevenEighths.HeckeBoundary.boundary_ne_zero_of_series_eq line 179
  14. def OAI.SevenEighths.HeckeBoundary.zetaConvolutionCoeff line 225
  15. theorem OAI.SevenEighths.HeckeBoundary.idealDivisors_one line 228
  16. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolutionCoeff_one line 233
  17. theorem OAI.SevenEighths.HeckeBoundary.idealDivisors_prime_pow line 238
  18. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolutionCoeff_prime_pow line 249
  19. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolutionCoeff_mul line 257
  20. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolutionCoeff_nonneg line 269
  21. theorem OAI.SevenEighths.HeckeBoundary.quadratic_normFiber_nonneg line 292
  22. theorem OAI.SevenEighths.HeckeBoundary.mulFiber_character_sum line 305
  23. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolution_hasSum line 316
  24. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolution_normFiber_one line 351
  25. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolution_LSeries_hasSum line 360
  26. theorem OAI.SevenEighths.HeckeBoundary.zetaConvolution_LSeries_eq line 369
  27. theorem OAI.SevenEighths.HeckeBoundary.quadratic_product_positive line 375
  28. theorem OAI.SevenEighths.HeckeBoundary.fullIdealZeta_eq_dirichlet_product line 392
  29. def OAI.SevenEighths.HeckeBoundary.regularizedIdealZeta line 432
  30. theorem OAI.SevenEighths.HeckeBoundary.regularizedIdealZeta_differentiable line 436
  31. theorem OAI.SevenEighths.HeckeBoundary.regularizedIdealZeta_eq line 442
  32. theorem OAI.SevenEighths.HeckeBoundary.regularizedIdealZeta_neg_two line 450
  33. theorem OAI.SevenEighths.HeckeBoundary.differentiable_dslope_of_entire line 458
  34. theorem OAI.SevenEighths.HeckeBoundary.quadratic_one_ne_zero_of_regularized_zeta line 464
  35. theorem OAI.SevenEighths.HeckeBoundary.quadratic_one_ne_zero_of_entire line 484
  36. theorem OAI.SevenEighths.HeckeBoundary.normWeight_real_nonneg line 492
  37. theorem OAI.SevenEighths.HeckeBoundary.norm_series_le_norm_fullIdealZeta line 500
  38. theorem OAI.SevenEighths.HeckeBoundary.fullIdealZeta_isBigO_near_one_horizontal line 520
  39. theorem OAI.SevenEighths.HeckeBoundary.series_isBigO_near_one_horizontal line 536
  40. theorem OAI.SevenEighths.HeckeBoundary.residue_boundary_ne_zero_of_series_eq line 548