OAI/NumberTheory/Ostmann/HybridSieve/SamplingIntervals.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.HybridSieve.separated_integral_sum_le_online 11 - theorem
OAI.Ostmann.HybridSieve.separated_sampling_bound_online 39 - theorem
OAI.Ostmann.HybridSieve.separated_complex_samples_le_integralline 59