OAI/NumberTheory/SiegelZeros/EntireFunctions/AvoidZeroRadii.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.analyticOrderAt_normalizedCompletion line 31
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.analyticOrderAt_normalizedCompletion_ne_top line 41
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.natCast_order_normalizedCompletion line 51
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.order_normalizedCompletion_pos line 57
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.rootNumber_ne_zero line 79
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedCompletion_zero_mem_strip line 86
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.LFunction_zero_of_normalizedCompletion_zero line 102
  8. def OAI.SiegelZeros.SiegelZerosAwei.W51.ZeroIndex line 118
  9. def OAI.SiegelZeros.SiegelZerosAwei.W51.zeroValue line 122
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroValue_is_zero line 124
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.exists_zeroIndex_iff line 127
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.exists_zeroIndex_of_real_zero line 135
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroValue_mem_strip line 141
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroValue_contribution_nonneg line 146
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.normalizedCompletion_zeros_closed_discrete line 164
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.finite_normalizedCompletion_zeros_in_compact line 180
  17. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.finite_completedLFunction_zeros_in_compact line 186
  18. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.finite_zeroSubtype_preimage_compact line 192
  19. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.finite_zeroIndex_fiber line 199
  20. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.finite_zeroIndex_preimage_compact line 210
  21. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.finite_zeroIndex_norm_le line 216
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.countable_zeroIndex line 221
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroValue_tendsto_cofinite_cocompact line 230
  24. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroValue_cofinite_far line 234
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.nonzeroZeros_cofinite_far line 239
  26. def OAI.SiegelZeros.WeightedTorusJets.W63.HadamardFormulaAt line 264
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W63.HadamardFormulaAt.to_expansion line 275
  28. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.entire_order_ne_top line 298
  29. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.divisor_eq_nat_order line 306
  30. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.jensen_identity_at_zero line 314
  31. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.circleAverage_log_norm_le line 330
  32. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.finite_zero_count_mul_log_two_le line 342
  33. def OAI.SiegelZeros.SiegelZerosAwei.W03.zeroRootFinset line 406
  34. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.mem_zeroRootFinset line 411
  35. def OAI.SiegelZeros.SiegelZerosAwei.W03.zeroIndexFinset line 417
  36. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.mem_zeroIndexFinset line 421
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.zeroIndex_ncard_eq_sum_orders line 429
  38. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_zero_count_jensen line 441
  39. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_zero_count_le_of_growth line 470
  40. def OAI.SiegelZeros.SiegelZerosAwei.W51.canonicalProduct line 503
  41. def OAI.SiegelZeros.SiegelZerosAwei.W51.deletedRootProduct line 506
  42. def OAI.SiegelZeros.SiegelZerosAwei.W51.zeroRootFiberEquiv line 510
  43. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroRootFiber_tprod line 522
  44. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.analyticOrderAt_genusOneFactor line 531
  45. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.analyticOrderAt_genusOneFactor_pow line 543
  46. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.canonicalProduct_split_root line 550
  47. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.analyticOrderAt_canonicalProduct_at_root line 571
  48. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.dyadic_count_bound_of_jensen line 602
  49. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_zero_inverse_square_summable_of_growth line 651
  50. theorem OAI.SiegelZeros.WeightedTorusJets.W04.exists_radius_avoiding_finite line 676
  51. theorem OAI.SiegelZeros.WeightedTorusJets.W04.exists_radius_avoiding_finite_set line 729
  52. theorem OAI.SiegelZeros.WeightedTorusJets.W04.actual_zero_radius_count_separation line 740
  53. theorem OAI.SiegelZeros.WeightedTorusJets.W04.eventually_count_denominator_le_cube line 753
  54. theorem OAI.SiegelZeros.WeightedTorusJets.W04.eventually_radius_avoiding_of_dyadic_count line 788
  55. theorem OAI.SiegelZeros.WeightedTorusJets.W04.actual_eventually_radius_separation_of_growth line 824