OAI/NumberTheory/CubicMoment/Transform/MetaplecticCoefficientMajorant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic bounds for the actual dual coefficients. Clearing the ramified denominator identifies every common level prime among the two supported factors; the free factor is coprime to the level.

  1. lemma OAI.CubicFirstMoment.metaplectic_numerator_of_frequency line 15
  2. lemma OAI.CubicFirstMoment.metaplecticCommonNorm_le_supported line 29
  3. lemma OAI.CubicFirstMoment.metaplectic_actual_coefficient_bound line 61

    Source documentation

    The published coefficient support gives this bound with no angular restriction. It will be summed using the actual lattice norm series.

    lemma metaplectic_actual_coefficient_bound
    {a : Eisenstein → MetaplecticDualArgument → ℂ} {C : ℝ} (hC : 0 ≤ C)
    {r : Eisenstein} (hr : primary r) (n : MetaplecticDualArgument)
    {j : ℤ} (hj : -1 ≤ j) (ζ : Eisensteinˣ) {h h' w : Eisenstein}
    (hh : primary h) (hh' : primary h') (hwr : IsCoprime w r)
    (he : metaplecticFrequency n = traceLambda^j*(ζ.val:ℂ)*(h:ℂ)*(w:ℂ)*(h':ℂ)^3)
    (ha : ‖a r n‖ ≤ C*3^((max j 0:ℤ)/3:ℝ)*Real.sqrt (norm h')) :
    ‖a r n*metaplecticLocalCoefficient r n‖ ≤
      C*3^((max j 0:ℤ)/3:ℝ)*Real.sqrt (norm h')*(norm h*norm h') := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticFrequency, OAI.CubicFirstMoment.traceLambda, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticLocalCoefficient

  4. lemma OAI.CubicFirstMoment.metaplectic_norm_pow line 77
  5. lemma OAI.CubicFirstMoment.metaplectic_lambda_norm line 82
  6. lemma OAI.CubicFirstMoment.metaplectic_frequency_norm line 89
  7. lemma OAI.CubicFirstMoment.metaplectic_squarefree_supported_divisor line 105
  8. lemma OAI.CubicFirstMoment.metaplectic_supported_divisor_mem line 113
  9. lemma OAI.CubicFirstMoment.metaplectic_units_finite line 120