OAI/NumberTheory/CubicMoment/Angular/AngularStructuredPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal angular sum and its finite smooth output partition, with coefficient cutoffs kept consistent at every output dyad.

  1. def OAI.CubicFirstMoment.structuredAngularPrimeMomentAt line 16
  2. lemma OAI.CubicFirstMoment.structuredAngularPrimeMomentAt_eq line 23
  3. def OAI.CubicFirstMoment.structuredAngularPrimeSum line 68
  4. lemma OAI.CubicFirstMoment.structuredAngularPrimeSum_partition line 74
  5. lemma OAI.CubicFirstMoment.structuredAngularPrimeSum_partition_dyads line 97