OAI/NumberTheory/CubicMoment/Estimates/PrimeIndicatorCollection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Restricting the indicator convolution to genuine primary primes, followed by the exact squarefree discrepancy.

  1. lemma OAI.CubicFirstMoment.orderedConvolution_primeIndicator line 13
  2. def OAI.CubicFirstMoment.coordinatePrimeSupport line 47
  3. lemma OAI.CubicFirstMoment.coordinatePrimeSupport_primary line 51
  4. lemma OAI.CubicFirstMoment.primeIndicatorTuple_eq_prime_convolution line 57
  5. def OAI.CubicFirstMoment.primarySquarefreePrimeTuple line 79
  6. lemma OAI.CubicFirstMoment.primeIndicator_sub_squarefree line 86
  7. def OAI.CubicFirstMoment.coordinatePrimeCutoff line 96
  8. lemma OAI.CubicFirstMoment.coordinatePrimeCutoff_spec line 99
  9. lemma OAI.CubicFirstMoment.primeIndicator_sub_squarefree_cutoff line 104