OAI/NumberTheory/Jacobsthal/Siegel/CompletedLAnalyticOrderNeTop.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.completedL_analyticOrderAt_ne_top line 33
  2. theorem OAI.Erdos970.WeightedTorusJets.completedL_analyticOrderNatAt_pos_iff line 41
  3. theorem OAI.Erdos970.WeightedTorusJets.finite_completedL_zeros_on_compact line 48
  4. theorem OAI.Erdos970.RealCharacterAnalysis.divisorCanonicalProduct_eq_tprod_analytic line 80
  5. theorem OAI.Erdos970.WeightedTorusJets.gammaFactor_real_parity_argument line 109
  6. theorem OAI.Erdos970.WeightedTorusJets.exists_upper_bound_zeta_logDeriv_log line 126
  7. theorem OAI.Erdos970.RealCharacterAnalysis.quadratic_prime_values line 147
  8. theorem OAI.Erdos970.RealCharacterAnalysis.deriv_lFunction_conj line 154
  9. theorem OAI.Erdos970.RealCharacterAnalysis.deriv_lFunction_real line 165
  10. theorem OAI.Erdos970.RealCharacterAnalysis.logarithmic_derivative_real line 173
  11. theorem OAI.Erdos970.RealCharacterAnalysis.quadratic_nonprincipal_has_negative_value line 180
  12. theorem OAI.Erdos970.RealCharacterAnalysis.gammaR_conj line 190
  13. theorem OAI.Erdos970.RealCharacterAnalysis.gammaFactor_inv_conj line 197
  14. theorem OAI.Erdos970.RealCharacterAnalysis.completed_lFunction_conj line 219
  15. theorem OAI.Erdos970.RealCharacterAnalysis.completed_lFunction_real line 255
  16. theorem OAI.Erdos970.RealCharacterAnalysis.deriv_completed_lFunction_conj line 263
  17. theorem OAI.Erdos970.RealCharacterAnalysis.deriv_completed_lFunction_real line 274
  18. theorem OAI.Erdos970.RealCharacterAnalysis.logDeriv_completed_lFunction_real line 282