OAI/NumberTheory/CubicMoment/Estimates/IdealDualDyads.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact dyadic decomposition of the retained full-ideal polynomial. The square-root normalization changes only coefficients, not characters.

  1. def OAI.CubicFirstMoment.idealDyadIndex line 14
  2. def OAI.CubicFirstMoment.idealDyad line 17
  3. def OAI.CubicFirstMoment.idealDyadIndices line 20
  4. lemma OAI.CubicFirstMoment.idealDyad_norm line 22
  5. lemma OAI.CubicFirstMoment.finite_idealDirichlet_dyad_partition line 29
  6. theorem OAI.CubicFirstMoment.finite_idealDirichlet_normalized_dyads line 39

    Source documentation

    The complete retained polynomial is the sum of normalized dyads; all coefficient weights are independent of the Hecke conductor.

    theorem finite_idealDirichlet_normalized_dyads (S : Finset EisensteinIdealExponent)
    (χ : EisensteinIdealExponent → ℂ) (u : ℝ) :
    finiteNormDirichlet S χ idealExponentNorm ((1/2:ℂ)-(u:ℂ)*Complex.I) =
      ∑ j ∈ idealDyadIndices S, (((2:ℝ)^j)^(-(1/2:ℝ)):ℝ)*
        ∑ ν ∈ idealDyad S j,
          (χ ν*((((2:ℝ)^j)/idealExponentNorm ν)^(1/2:ℝ):ℝ))*
            mellinPhase u (idealExponentNorm ν) := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.finiteNormDirichlet, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.idealDyadIndices, OAI.CubicFirstMoment.idealDyad, OAI.CubicFirstMoment.mellinPhase

  7. lemma OAI.CubicFirstMoment.idealDyad_normalized_coefficient_le line 52
  8. lemma OAI.CubicFirstMoment.idealDyadIndices_card_le line 58