OAI/NumberTheory/CubicMoment/Decomposition/StoppedIntervalRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact conversion of the sharp stopped side to the full analytic interval at exclusion e=1. Coefficients vanish off their actual product support, so the interval extension adds no term.

  1. lemma OAI.CubicFirstMoment.stoppedNormDyad_mem_iff line 15
  2. lemma OAI.CubicFirstMoment.primaryPairSupport_self_of_mem line 37
  3. lemma OAI.CubicFirstMoment.stoppedRowCoefficient_eq_zero_of_not_mem line 43
  4. theorem OAI.CubicFirstMoment.stoppedBeta_interval_sum_to_row line 60