PrimitiveDualMoments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Cubic second moments for the actual primitive ideal characters. The primes above three are separated exactly before applying the cubic sieve.

lemma OAI.CubicFirstMoment.primitiveDualPolynomial_ramified_partition line 13

theorem OAI.CubicFirstMoment.normalized_primitive_ideal_cubic_moment line 37

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_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)) ℂ) (N J u : ℝ),
      primary b → Squarefree b → 1 ≤ N → 1 ≤ J →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N ∧ IsCoprime a b) →
      (∀ a ∈ P, d a ≠ 0) →
      (∀ a ∈ P, ∀ v : Eisensteinˣ, ψ a (Ideal.Quotient.mk (modulus (d a)) v) = 1) →
      (∀ a ∈ P, ∀ x : Eisenstein, primary x → IsCoprime (a*b) x →
        ψ a (Ideal.Quotient.mk (modulus (d a)) x) = mixedCubic a b x) →
      (∀ ν ∈ S, J ≤ idealExponentNorm ν ∧ idealExponentNorm ν ≤ 2*J) →
      (∑ a ∈ P, ‖normalizedDualPolynomial S (residueIdealChar (d a) (ψ a))
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.modulus, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.residueIdealChar