OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorExclusion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Divisibility filters in the coprime Mellin rows are finite combinations of the original coprimality exclusions. This identity keeps the stopped coefficient unchanged, so its proved Kummer estimate remains applicable.

  1. lemma OAI.CubicFirstMoment.prime_subset_exclusion_count line 14
  2. theorem OAI.CubicFirstMoment.prime_product_divisibility_exclusions line 30
  3. theorem OAI.CubicFirstMoment.prime_product_filtered_sum line 58
  4. lemma OAI.CubicFirstMoment.stoppedIntervalSupport_filter_coprime line 84
  5. theorem OAI.CubicFirstMoment.stopped_divisibility_row line 93
  6. theorem OAI.CubicFirstMoment.stopped_small_divisor_sw line 106