OAI/NumberTheory/CubicMoment/Estimates/StructuredCutoffConsistency.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The factor cutoff may be moved to the current output dyad. It does not impose a new condition on a product whose norm is already in that dyad.

  1. lemma OAI.CubicFirstMoment.orderedConvolution_filter_norm line 13
  2. lemma OAI.CubicFirstMoment.squarefreeConvolution_filter_norm line 34
  3. lemma OAI.CubicFirstMoment.coordinatePrimeSupport_trim line 43
  4. lemma OAI.CubicFirstMoment.primeMomentCoefficient_dyad_consistent line 56
  5. lemma OAI.CubicFirstMoment.orderedSupport_filter_norm line 62
  6. def OAI.CubicFirstMoment.structuredPrimeMomentAt line 73
  7. lemma OAI.CubicFirstMoment.structuredPrimeMomentAt_eq line 80