OAI/NumberTheory/Ostmann/HybridSieve/SamplingLog.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.HybridSieve.sampling_harmonic_factor_le line 9
2. lemma OAI.Ostmann.HybridSieve.sampling_log_derivative_factor_le line 17
3. theorem OAI.Ostmann.HybridSieve.exists_character_polynomial_sampling_log_constant line 23
4. theorem OAI.Ostmann.HybridSieve.exists_unweighted_character_polynomial_sampling_log_constant line 64