IdealMixedMoments.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The ordinary mixed sieve on the normalized dual ideal blocks. All coefficient bounds and the number of ideals are derived explicitly.

lemma OAI.CubicFirstMoment.ideal_support_card_le line 13
lemma OAI.CubicFirstMoment.normalizedDualPolynomial_mixed line 21

theorem OAI.CubicFirstMoment.normalized_ideal_mixed_moment line 34

Source documentation

Complete dual ideal supports, including the ramified prime, satisfy the ordinary sieve bound uniformly in their common norm twist.

theorem normalized_ideal_mixed_moment (hHuxley : HuxleyAdditiveLargeSieve)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (P : Finset (Eisenstein × Eisenstein))
      (S : Finset EisensteinIdealExponent) (Q Y J u : ℝ),
      1 ≤ Q → 1 ≤ Y → 0 < J →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∀ ν ∈ S, J ≤ idealExponentNorm ν ∧ idealExponentNorm ν ≤ Y) →
      (∑ p ∈ P, ‖normalizedDualPolynomial S
        (fun ν => mixedCubic p.1 p.2 (idealExponentGenerator ν))
        idealExponentNorm J u‖^2) ≤ C*Q^ε*(Q^2+Y)*Y := by
…

Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.idealExponentGenerator