OAI/NumberTheory/CubicMoment/Estimates/TripleScaleLogRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A product envelope fixes the sum of the three smooth norm indices up to an absolute interval. Its location may grow with X; its length is independent of X.

  1. lemma OAI.CubicFirstMoment.tripleNormScale_log_product line 12
  2. def OAI.CubicFirstMoment.tripleIndexEnvelopeWidth line 24
  3. def OAI.CubicFirstMoment.tripleIndexEnvelopeStart line 26
  4. lemma OAI.CubicFirstMoment.tripleNormScale_index_sum_range line 29