OAI/NumberTheory/Jacobsthal/Siegel/ConductorCompletedL.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.conductorCompletedL line 23
  2. theorem OAI.Erdos970.WeightedTorusJets.gammaFactor_ne_zero_of_re_pos line 27
  3. theorem OAI.Erdos970.WeightedTorusJets.completedL_eq_mul_gammaFactor line 37
  4. theorem OAI.Erdos970.WeightedTorusJets.completedL_ne_zero_of_one_le_re line 44
  5. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_zero_iff line 51
  6. theorem OAI.Erdos970.WeightedTorusJets.differentiable_conductorCompletedL line 55
  7. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_one_sub line 62
  8. theorem OAI.Erdos970.WeightedTorusJets.completedL_zero_re_mem_Ioo line 78
  9. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_logDeriv line 92
  10. theorem OAI.Erdos970.WeightedTorusJets.completedL_eq_poleFree line 109
  11. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_eq_hurwitzSum line 115
  12. theorem OAI.Erdos970.WeightedTorusJets.norm_conductor_power_le line 131
  13. theorem OAI.Erdos970.WeightedTorusJets.norm_conductorCompletedL_le_hurwitzSum line 143
  14. theorem OAI.Erdos970.WeightedTorusJets.finite_uniform_exp_bound line 161
  15. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_growth_of_hurwitz line 171
  16. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_analyticOrderAt_eq line 230
  17. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_ne_zero_at_zero line 240
  18. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_analyticOrderNatAt_zero line 247
  19. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_norm_growth line 258
  20. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_log_growth line 266
  21. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_zeroIndex_vanishes line 278
  22. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_zeroIndex_re_mem_Ioo line 292
  23. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_zeroIndex_summable_inv_sq line 299
  24. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_hadamard_factorization line 312
  25. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_logDeriv_hasSum line 328
  26. theorem OAI.Erdos970.WeightedTorusJets.reflected_reciprocal_tsum line 373
  27. theorem OAI.Erdos970.WeightedTorusJets.primitive_rootNumber_ne_zero line 390
  28. theorem OAI.Erdos970.WeightedTorusJets.logDeriv_conductorCompletedL_one_sub line 400
  29. theorem OAI.Erdos970.WeightedTorusJets.analyticOrderAt_conductorCompletedL_one_sub line 412
  30. theorem OAI.Erdos970.WeightedTorusJets.completed_reciprocal_tsum_reflection line 436
  31. theorem OAI.Erdos970.WeightedTorusJets.real_logDeriv_conductorCompletedL_eq_tsum line 458
  32. theorem OAI.Erdos970.RealCharacterAnalysis.toNat_divisor_eq_analyticOrderNatAt line 498
  33. def OAI.Erdos970.RealCharacterAnalysis.divisorIndexEquivAnalytic line 506
  34. theorem OAI.Erdos970.RealCharacterAnalysis.divisorIndexEquivAnalytic_val line 522
  35. theorem OAI.Erdos970.RealCharacterAnalysis.tsum_divisorIndex_eq_analytic line 526
  36. theorem OAI.Erdos970.RealCharacterAnalysis.summable_divisorIndex_iff_analytic line 533