OAI/NumberTheory/CubicMoment/Estimates/TailDyads.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact dyadic decomposition of both coefficient supports in the original product-envelope tail. The triangle inequality is applied only after this finite identity.

  1. lemma OAI.CubicFirstMoment.envelopeCutoffBilinearTail_dyads line 13
  2. lemma OAI.CubicFirstMoment.envelopeCutoffBilinearTail_dyads_bound line 37
  3. theorem OAI.CubicFirstMoment.stoppedNormDyad_count_power line 51