TwistedDualMoments.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The cubic second moment for actual primitive characters after a fixed small twist. All exceptional small-prime parts remain explicit.

theorem OAI.CubicFirstMoment.normalized_twisted_primitive_ideal_cubic_moment line 15

Source documentation

A family of primitive mixed characters satisfies the cubic second moment on a full ideal dyad. Only the explicit number of ramified parts is lost.

theorem normalized_twisted_primitive_ideal_cubic_moment {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset Eisenstein) (S : Finset EisensteinIdealExponent)
      (b : Eisenstein) (d : Eisenstein → Eisenstein)
      (ψ : (a : Eisenstein) → MulChar (Residues (d a)) ℂ)
      (r : Eisenstein) (η : MulChar (Residues r) ℂ) (N J u : ℝ),
      primary b → Squarefree b → r ≠ 0 →
      (∀ v : Eisensteinˣ, η (Ideal.Quotient.mk (modulus r) v) = 1) →
      1 ≤ N → 1 ≤ J →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N ∧ IsCoprime a b) →
      (∀ a ∈ P, IsCoprime (a*b) r) →
      (∀ a ∈ P, d a ≠ 0) →
      (∀ a ∈ P, ∀ v : Eisensteinˣ, ψ a (Ideal.Quotient.mk (modulus (d a)) v) = 1) →
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.norm