OAI/NumberTheory/SiegelZeros/EntireFunctions/CompletedLAnalyticOrderNeTop.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_analyticOrderAt_ne_top line 61
2. theorem OAI.SiegelZeros.WeightedTorusJets.completedL_analyticOrderNatAt_pos_iff line 69
3. theorem OAI.SiegelZeros.WeightedTorusJets.finite_completedL_zeros_on_compact line 76
4. theorem OAI.SiegelZeros.RealCharacterAnalysis.divisorCanonicalProduct_eq_tprod_analytic line 125
5. theorem OAI.SiegelZeros.WeightedTorusJets.gammaFactor_real_parity_argument line 179
6. theorem OAI.SiegelZeros.WeightedTorusJets.exists_upper_bound_zeta_logDeriv_log line 201
7. theorem OAI.SiegelZeros.RealCharacterAnalysis.quadratic_prime_values line 249
8. theorem OAI.SiegelZeros.RealCharacterAnalysis.deriv_lFunction_conj line 256
9. theorem OAI.SiegelZeros.RealCharacterAnalysis.deriv_lFunction_real line 267
10. theorem OAI.SiegelZeros.RealCharacterAnalysis.logarithmic_derivative_real line 275
11. theorem OAI.SiegelZeros.RealCharacterAnalysis.quadratic_nonprincipal_has_negative_value line 282
12. theorem OAI.SiegelZeros.RealCharacterAnalysis.gammaR_conj line 292
13. theorem OAI.SiegelZeros.RealCharacterAnalysis.gammaFactor_inv_conj line 299
14. theorem OAI.SiegelZeros.RealCharacterAnalysis.completed_lFunction_conj line 321
15. theorem OAI.SiegelZeros.RealCharacterAnalysis.completed_lFunction_real line 357
16. theorem OAI.SiegelZeros.RealCharacterAnalysis.deriv_completed_lFunction_conj line 365
17. theorem OAI.SiegelZeros.RealCharacterAnalysis.deriv_completed_lFunction_real line 376
18. theorem OAI.SiegelZeros.RealCharacterAnalysis.logDeriv_completed_lFunction_real line 384