AngularTwistedDualMoments.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_angular_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_angular_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 →
      (AngularUnitCompatible r η ℓ) →
      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, AngularUnitCompatible (d a) (ψ a) ℓ) →
…

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