OAI/NumberTheory/SiegelZeros/Structure/RealBridge.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.W05.eulerTerm_ofReal_eq line 13
2. theorem OAI.SiegelZeros.WeightedTorusJets.W05.real_eulerTerm_summable line 24
3. theorem OAI.SiegelZeros.WeightedTorusJets.W05.actual_character_prime_restriction line 31
4. theorem OAI.SiegelZeros.WeightedTorusJets.W05.real_eulerSum_eq_logDerivatives line 45
5. theorem OAI.SiegelZeros.WeightedTorusJets.W05.prime_mass_le_logDerivatives line 61
6. theorem OAI.SiegelZeros.WeightedTorusJets.W05.real_character_prime_mass_le_logDerivatives line 74