OAI/NumberTheory/SiegelZeros/EntireFunctions/DeletedProduct.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.gamma_le_exp_mul_log line 17
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.global_exponential_envelope line 49
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.even_kernel_global_envelope line 75
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.cos_kernel_global_envelope line 84
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.odd_kernel_global_envelope line 91
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.sin_kernel_global_envelope line 97
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_eq_regularized line 103
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.mellin_integrand_envelope line 121
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.mellin_tail_gamma_bound line 136
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.mellin_tail_order_one_bound line 177
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.mellin_upper_indicator line 211
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.strong_lower_mellin line 219
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.strong_mellin_split line 255
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.weak_regularized_mellin_split line 275
  15. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.tailGrowth line 311
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.weak_regularized_growth line 315
  17. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.strong_mellin_growth line 328
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_even_growth line 341
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_odd_growth line 367
  20. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.radiusLog line 397
  21. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.radiusLog_ge_one line 399
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.tailGrowth_le_radiusLog line 405
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.coeff_tailGrowth_le line 421
  24. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.pair_tailGrowth_le line 433
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_even_radius_growth line 452
  26. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_odd_radius_growth line 464
  27. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_norm_le_common_bound line 487
  28. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.completed_radius_growth line 522
  29. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.radiusLog_le_standard line 585
  30. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.normalized_radius_growth line 612
  31. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.normalizedCompletion_order_one_growth line 640
  32. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.differentiable_indexedGenusOneProduct line 659
  33. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_zero_inverse_square_summable line 681
  34. def OAI.SiegelZeros.SiegelZerosAwei.W03.zeroSubproduct line 688
  35. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.zeroSubfamily_inverse_square_summable line 692
  36. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.zeroSubfamily_cofinite_far line 697
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.differentiable_zeroSubproduct line 703
  38. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.zeroSubproduct_ne_zero line 711
  39. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_genusOneProduct_multipliable line 720
  40. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.multipliable_zeroSubproduct line 730
  41. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.deleted_root_subproduct_ne_zero line 742