OAI/NumberTheory/CubicMoment/Angular/AngularUpperTailAggregation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Aggregate the literal upper-height stopped terms over their original labels, side dyads and distinguished-prime scales.

  1. def OAI.CubicFirstMoment.angular_upperStoppedEnvelopeTail line 17
  2. lemma OAI.CubicFirstMoment.angular_upperTailStoppedRow_height_dyads line 24
  3. theorem OAI.CubicFirstMoment.angular_upperStoppedEnvelopeTail_aggregate line 45