OAI/NumberTheory/Jacobsthal/Harmonic/CharacterPositivity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.characterPhase line 13
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.characterPhase_norm line 15
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.characterPhase_double line 20
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.twist_vonMangoldt_term_split line 28
5. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.character_positivity_polynomial line 44
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.vonMangoldt_three_four_one_nonneg line 53
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.twisted_series_eq_actual_log_derivative line 92
8. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.character_log_derivative_positivity line 101