OAI/NumberTheory/CubicMoment/Transform/MetaplecticGrowthProvider.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The internal strip-growth property can be supplied either by the original published auxiliary estimates or directly by the Voronoi formula. The latter route removes those auxiliary hypotheses from the main results.

  1. def OAI.CubicFirstMoment.MetaplecticPolynomialGrowth line 14
  2. lemma OAI.CubicFirstMoment.metaplectic_polynomial_growth_of_published line 18
  3. lemma OAI.CubicFirstMoment.metaplectic_continuation_unique line 24
  4. theorem OAI.CubicFirstMoment.metaplectic_polynomial_growth_of_voronoi line 48