Entry bounds for numerators ∏ (t + γ²)

For a multiset M of integers, tpol M = ∏_{γ ∈ M} (t + γ²). Its pullback is pull K (tpol M) = ± x⁵ ∏_{γ ∈ M} (x - γ)(x + γ), so the direct bound applies to μ_X(tpol M / D_K).

noncomputable def Zeta5Irrational.tpol (M : Multiset ℤ) : Polynomial ℚ

∏_{γ ∈ M} (t + γ²).

Equations

• Zeta5Irrational.tpol M = (Multiset.map (fun (γ : ℤ) => Polynomial.X + Polynomial.C (↑γ ^ 2)) M).prod

theorem Zeta5Irrational.tpol_add (M M' : Multiset ℤ) : tpol (M + M') = tpol M * tpol M'

def Zeta5Irrational.xroots (M : Multiset ℤ) : Multiset ℤ

The x-roots of the pullback of tpol M.

Equations

• Zeta5Irrational.xroots M = Multiset.replicate 5 0 + M + Multiset.map (fun (γ : ℤ) => -γ) M

theorem Zeta5Irrational.pull_tpol (K : ℕ) (M : Multiset ℤ) : pull K (tpol M) = numOf ((-1) ^ (K + M.card)) (xroots M)

theorem Zeta5Irrational.cnt_xroots (p : ℕ) (M : Multiset ℤ) (c : ZMod p) : cnt p (xroots M) c = (if c = 0 then 5 else 0) + (Multiset.filter (fun (γ : ℤ) => ↑γ = c) M).card + (Multiset.filter (fun (γ : ℤ) => ↑γ = -c) M).card

Number of x-roots in the class c.

theorem Zeta5Irrational.μX_tpol_bound {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) (K : ℕ) (M : Multiset ℤ) (hsep : Sep p (PlK K)) (hK : K < p ^ 2) (hdeg : 5 + 2 * M.card - 2 * K + 1 < p ^ 2) (β : ℚ) (hβ : ∀ (c : ZMod p), β ≤ ↑((if c = 0 then 5 else 0) + (Multiset.filter (fun (γ : ℤ) => ↑γ = c) M).card + (Multiset.filter (fun (γ : ℤ) => ↑γ = -c) M).card) - ↑(plc p (PlK K) c).card) : GV p (μX K (tpol M)) (β - 4)

Entry bound for μ_X(tpol M / D_K).