OAI/NumberTheory/SiegelZeros/Characters/ConductorCompletedL.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL line 22
  2. theorem OAI.SiegelZeros.WeightedTorusJets.gammaFactor_ne_zero_of_re_pos line 26
  3. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_eq_mul_gammaFactor line 36
  4. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_ne_zero_of_one_le_re line 43
  5. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_zero_iff line 50
  6. theorem OAI.SiegelZeros.WeightedTorusJets.differentiable_conductorCompletedL line 54
  7. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_one_sub line 61
  8. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_zero_re_mem_Ioo line 77
  9. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_logDeriv line 91
  10. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_eq_poleFree line 108
  11. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_eq_hurwitzSum line 114
  12. theorem OAI.SiegelZeros.WeightedTorusJets.norm_conductor_power_le line 130
  13. theorem OAI.SiegelZeros.WeightedTorusJets.norm_conductorCompletedL_le_hurwitzSum line 142
  14. theorem OAI.SiegelZeros.WeightedTorusJets.finite_uniform_exp_bound line 160
  15. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_growth_of_hurwitz line 170
  16. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_analyticOrderAt_eq line 229
  17. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_ne_zero_at_zero line 239
  18. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_analyticOrderNatAt_zero line 246
  19. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_norm_growth line 257
  20. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_log_growth line 265
  21. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_zeroIndex_vanishes line 275
  22. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_zeroIndex_re_mem_Ioo line 289
  23. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_zeroIndex_summable_inv_sq line 296
  24. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_hadamard_factorization line 309
  25. theorem OAI.SiegelZeros.WeightedTorusJets.conductorCompletedL_logDeriv_hasSum line 325
  26. theorem OAI.SiegelZeros.WeightedTorusJets.reflected_reciprocal_tsum line 368
  27. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_rootNumber_ne_zero line 383
  28. theorem OAI.SiegelZeros.WeightedTorusJets.logDeriv_conductorCompletedL_one_sub line 393
  29. theorem OAI.SiegelZeros.WeightedTorusJets.analyticOrderAt_conductorCompletedL_one_sub line 405
  30. theorem OAI.SiegelZeros.WeightedTorusJets.completed_reciprocal_tsum_reflection line 429
  31. theorem OAI.SiegelZeros.WeightedTorusJets.real_logDeriv_conductorCompletedL_eq_tsum line 449
  32. theorem OAI.SiegelZeros.RealCharacterAnalysis.toNat_divisor_eq_analyticOrderNatAt line 487
  33. def OAI.SiegelZeros.RealCharacterAnalysis.divisorIndexEquivAnalytic line 495
  34. theorem OAI.SiegelZeros.RealCharacterAnalysis.divisorIndexEquivAnalytic_val line 511
  35. theorem OAI.SiegelZeros.RealCharacterAnalysis.tsum_divisorIndex_eq_analytic line 515
  36. theorem OAI.SiegelZeros.RealCharacterAnalysis.summable_divisorIndex_iff_analytic line 522