OAI/NumberTheory/CubicMoment/Estimates/ResidueIdealCharacters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite residue character as an actual complete ideal character, and exact restoration of Euler factors after primitive reduction.

  1. def OAI.CubicFirstMoment.residueIdealChar line 14
  2. lemma OAI.CubicFirstMoment.residueIdealChar_add line 18
  3. lemma OAI.CubicFirstMoment.residueChar_norm_le_one line 23
  4. lemma OAI.CubicFirstMoment.residueIdealChar_norm_le_one line 35
  5. lemma OAI.CubicFirstMoment.residueIdealChar_primaryMixed line 39
  6. lemma OAI.CubicFirstMoment.ideal_coprime_support line 44
  7. lemma OAI.CubicFirstMoment.induced_residueIdealChar line 60
  8. theorem OAI.CubicFirstMoment.induced_residue_smooth_euler line 70

    Source documentation

    Primitive reduction gives an exact finite Euler inclusion-exclusion for the original complete smooth sum, with every rescaling retained.

    theorem induced_residue_smooth_euler {q d : Eisenstein} (hq : q ≠ 0)
    {χ : MulChar (Residues q) ℂ} {ψ : MulChar (Residues d) ℂ}
    (h : ResidueCharacterInduces q d χ ψ) (W : ℝ → ℂ)
    (hW : HasCompactSupport W) {Z : ℝ} (hZ : 0 < Z) :
    (∑' ν, residueIdealChar q χ ν*W (idealExponentNorm ν/Z)) =
      ∑ T ∈ (idealExponentOf q).support.powerset,
        (-1:ℂ)^T.card*residueIdealChar d ψ (primeSetExponent T)*
          ∑' κ, residueIdealChar d ψ κ*
            W (idealExponentNorm κ/(Z/idealExponentNorm (primeSetExponent T))) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.ResidueCharacterInduces, OAI.CubicFirstMoment.residueIdealChar, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.primeSetExponent