OAI/NumberTheory/Ostmann/HybridSieve/SamplingIntervals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.HybridSieve.separated_integral_sum_le_on line 11
  2. theorem OAI.Ostmann.HybridSieve.separated_sampling_bound_on line 39
  3. theorem OAI.Ostmann.HybridSieve.separated_complex_samples_le_integral line 59