OAI/NumberTheory/CubicMoment/Transform/MetaplecticPrefixAmplitude.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Apply the two scalar estimates to the literal prefix amplitude. The resulting weights are the geometric and primary norm weights already controlled by the finite arithmetic prefix sums.

  1. lemma OAI.CubicFirstMoment.metaplectic_min_common line 12
  2. lemma OAI.CubicFirstMoment.metaplectic_first_norm_weight line 18
  3. lemma OAI.CubicFirstMoment.metaplectic_second_norm_weight line 23
  4. lemma OAI.CubicFirstMoment.metaplecticPrefixAmplitude_nonneg line 32
  5. lemma OAI.CubicFirstMoment.metaplectic_prefix_first_amplitude line 44
  6. lemma OAI.CubicFirstMoment.metaplectic_prefix_second_amplitude line 73