OAI/NumberTheory/CubicMoment/Estimates/WideLogDenominator.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A quadratic coordinate range accommodates the fixed dilations in an output norm partition. The denominator identities need no upper range.

  1. def OAI.CubicFirstMoment.wideLogWeightParameters line 13
  2. lemma OAI.CubicFirstMoment.wideLogWeightParameters_compact line 15
  3. def OAI.CubicFirstMoment.uniformWideLogDenominatorWeights line 18
  4. def OAI.CubicFirstMoment.uniformCoordinateWideLogDenominatorWeights line 32
  5. lemma OAI.CubicFirstMoment.wideLogWeightParameters_mem line 40
  6. lemma OAI.CubicFirstMoment.logDenominatorWeight_scale_lower line 57
  7. lemma OAI.CubicFirstMoment.normalizedVonMangoldt_weight_lower line 75
  8. lemma OAI.CubicFirstMoment.primaryNormalizedVonMangoldtTuple_eq_lower line 95
  9. lemma OAI.CubicFirstMoment.normalizedCoordinate_norm_le_lower line 124