PrimaryIdealMoments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Sieve moments of the actual primary-normalized ideal character. The primary representative and the ramified zero are retained explicitly.

lemma OAI.CubicFirstMoment.primaryMixedIdealChar_eq line 13

theorem OAI.CubicFirstMoment.normalized_primary_ideal_cubic_moment line 27

Source documentation

The normalized ideal character is sieved with the exact primary representative. A fixed mixed factor and any fixed bounded coefficient twist are allowed, including the ramified local factors.

theorem normalized_primary_ideal_cubic_moment {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset Eisenstein) (S : Finset EisensteinIdealExponent)
      (b : Eisenstein) (ξ : EisensteinIdealExponent → ℂ) (N Y J u : ℝ),
      primary b → (∀ ν ∈ S, ‖ξ ν‖ ≤ 1) → 1 ≤ N → 1 ≤ Y → 0 < J →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∀ ν ∈ S, J ≤ idealExponentNorm ν ∧ idealExponentNorm ν ≤ Y) →
      (∑ a ∈ P, ‖normalizedDualPolynomial S
        (fun ν => ξ ν*primaryMixedIdealChar a b ν) idealExponentNorm J u‖^2) ≤
        C*(N*Y)^ε*Y*(N+Y+(N*Y)^(2/3:ℝ)) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.primaryMixedIdealChar