OAI/NumberTheory/CubicMoment/Transform/MetaplecticDualFinite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The retained Voronoi sum is an actual finite frequency polynomial. Its cutoff is independent of the height parameter.

  1. lemma OAI.CubicFirstMoment.metaplectic_frequency_norm_numerator line 12
  2. lemma OAI.CubicFirstMoment.metaplecticDualNorm_coordinate_bound line 20
  3. def OAI.CubicFirstMoment.metaplecticDualBall line 42
  4. lemma OAI.CubicFirstMoment.mem_metaplecticDualBall line 46
  5. def OAI.CubicFirstMoment.metaplecticRetainedTerm line 57
  6. lemma OAI.CubicFirstMoment.metaplecticRetainedTerm_finite line 62
  7. theorem OAI.CubicFirstMoment.metaplecticDualTerm_split line 75

    Source documentation

    Exact retained/tail split of the actual absolutely convergent dual series. The retained part is the displayed finite sum.

    theorem metaplecticDualTerm_split (a : Eisenstein → MetaplecticDualArgument → ℂ)
    (r : Eisenstein) (ℓ : ℤ) (W : ℝ → ℂ) (A X J : ℝ)
    (hs : Summable (metaplecticDualTerm a r ℓ W A X)) :
    (∑' nd, metaplecticDualTerm a r ℓ W A X nd) =
      (∑ nd ∈ metaplecticDualBall J, metaplecticDualTerm a r ℓ W A X nd)+
        ∑' nd, metaplecticFarTailTerm a r ℓ W A X J nd := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.metaplecticDualTerm, OAI.CubicFirstMoment.metaplecticDualBall, OAI.CubicFirstMoment.metaplecticFarTailTerm