OAI/NumberTheory/CubicMoment/Transform/MetaplecticPrefixSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separated finite sums over the actual supported prefixes. A finite subset of prefixes costs at most the product of its coordinate sums.

  1. lemma OAI.CubicFirstMoment.metaplectic_prefix_product_bound line 13
  2. lemma OAI.CubicFirstMoment.primary_argument_harmonic line 48
  3. lemma OAI.CubicFirstMoment.primary_argument_supported_sum line 62