OAI/NumberTheory/CubicMoment/Estimates/MixedCharacterSieve.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The conductor-by-conductor Gauss transfer for actual squarefree mixed characters.

  1. lemma OAI.CubicFirstMoment.primary_coprime_three line 13
  2. lemma OAI.CubicFirstMoment.norm_mixedGaussFactor line 18
  3. theorem OAI.CubicFirstMoment.mixedCharacter_unit_energy line 30

    Source documentation

    Each actual primitive mixed cubic character is bounded by the unit-residue additive energy at the same conductor. No analytic hypothesis is used.

    theorem mixedCharacter_unit_energy (N : Finset Eisenstein) (v : Eisenstein → ℂ)
    {a b : Eisenstein} (ha : primary a) (hb : primary b)
    (hsa : Squarefree a) (hsb : Squarefree b) (hab : IsCoprime a b) :
    ‖∑ n ∈ N, v n*star (mixedCubic a b n)‖^2 ≤ huxleyModulusMass (a*b) N v := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.huxleyModulusMass