OAI/NumberTheory/Jacobsthal/Siegel/NormLogDerivLFunctionNegLogDerivZeta.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.norm_logDeriv_LFunction_le_neg_logDeriv_zeta line 15
2. theorem OAI.Erdos970.WeightedTorusJets.exists_upper_bound_completedL_logDeriv line 51
3. theorem OAI.Erdos970.WeightedTorusJets.reciprocal_re_lower_of_near_one line 77
4. theorem OAI.Erdos970.WeightedTorusJets.near_one_indices_eq_of_tsum_bound line 102
5. theorem OAI.Erdos970.WeightedTorusJets.exists_near_one_divisor_indices_unique line 130
6. theorem OAI.Erdos970.WeightedTorusJets.analyticOrderAt_eq_one_of_divisor_indices_unique line 171
7. theorem OAI.Erdos970.WeightedTorusJets.exists_classical_near_one_zero_unique_real_simple line 204