Dissection of ∏_{j ∈ S} (t + j) under t = p u - b, the truncated local functional dl on a general numerator F (discLocal r n p b A = dl r n p b (X A)), the error functional Err, and the exactness of the distribution formula on Q · D_{5n}.

def Zeta32.PrimeEdge.nearS (p b : ℕ) (S : Finset ℕ) : Finset ℕ

Near poles of S on the disc b.

Equations

• Zeta32.PrimeEdge.nearS p b S = Finset.image (fun (j : ℕ) => (j - b) / p) ({j ∈ S | j % p = b})

noncomputable def Zeta32.PrimeEdge.farS (p b : ℕ) (S : Finset ℕ) : Polynomial ℚ

Far factors of S on the disc b.

Equations

• Zeta32.PrimeEdge.farS p b S = ∏ j ∈ S with j % p ≠ b, (Polynomial.C (↑j - ↑b) + Polynomial.C ↑p * Polynomial.X)

theorem Zeta32.PrimeEdge.sub_eq_mul_div {p j b : ℕ} (h : j % p = b) : j - b = p * (j / p)

theorem Zeta32.PrimeEdge.sub_div_eq {p j b : ℕ} (hp : 0 < p) (h : j % p = b) : (j - b) / p = j / p

theorem Zeta32.PrimeEdge.cast_eq_near {p j b : ℕ} (hp : 0 < p) (h : j % p = b) : ↑j = ↑p * ↑((j - b) / p) + ↑b

theorem Zeta32.PrimeEdge.injOn_near {p b : ℕ} (hp : 0 < p) (S : Finset ℕ) : Set.InjOn (fun (j : ℕ) => (j - b) / p) ↑({j ∈ S | j % p = b})

theorem Zeta32.PrimeEdge.card_nearS {p b : ℕ} (hp : 0 < p) (S : Finset ℕ) : (nearS p b S).card = {j ∈ S | j % p = b}.card

theorem Zeta32.PrimeEdge.nearSet_eq (n p b : ℕ) : nearSet n p b = nearS p b (Finset.Icc 1 (5 * n))

theorem Zeta32.PrimeEdge.farProd_eq (n p b : ℕ) : farProd n p b = farS p b (Finset.Icc 1 (5 * n))

theorem Zeta32.PrimeEdge.comp_mprod {p : ℕ} (hp : 0 < p) (b : ℕ) (S : Finset ℕ) : (mprod S).comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b) = Polynomial.C (↑p ^ {j ∈ S | j % p = b}.card) * mprod (nearS p b S) * farS p b S

Dissection of ∏_{j∈S} (t + j) at t = p u - b.

theorem Zeta32.PrimeEdge.farS_coeff_zero_ne {p b : ℕ} (hb : b < p) (S : Finset ℕ) : (farS p b S).coeff 0 ≠ 0

theorem Zeta32.PrimeEdge.ps_mul_inv {F : Polynomial ℚ} (h : F.coeff 0 ≠ 0) : ↑F * (↑F)⁻¹ = 1

noncomputable def Zeta32.PrimeEdge.dl (r : ℚ) (n p b : ℕ) (F : Polynomial ℚ) : ℚ

The truncated local functional on a general numerator F.

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.PrimeEdge.dl_add (r : ℚ) (n p b : ℕ) (F G : Polynomial ℚ) : dl r n p b (F + G) = dl r n p b F + dl r n p b G

theorem Zeta32.PrimeEdge.dl_C_mul (r : ℚ) (n p b : ℕ) (c : ℚ) (F : Polynomial ℚ) : dl r n p b (Polynomial.C c * F) = c * dl r n p b F

noncomputable def Zeta32.PrimeEdge.Err (r : ℚ) (n p : ℕ) (F : Polynomial ℚ) : ℚ

The error of the truncated distribution formula on a numerator F.

Equations

• Zeta32.PrimeEdge.Err r n p F = Zeta32.PrimeEdge.locValue r F (Finset.Icc 1 (5 * n)) - ↑p ^ (-2) * ∑ b ∈ Finset.range p, Zeta32.PrimeEdge.dl r n p b F

theorem Zeta32.PrimeEdge.Err_add (r : ℚ) (n p : ℕ) (F G : Polynomial ℚ) : Err r n p (F + G) = Err r n p F + Err r n p G

theorem Zeta32.PrimeEdge.Err_C_mul (r : ℚ) (n p : ℕ) (c : ℚ) (F : Polynomial ℚ) : Err r n p (Polynomial.C c * F) = c * Err r n p F

theorem Zeta32.PrimeEdge.Err_sum {ι : Type u_1} (r : ℚ) (n p : ℕ) (t : Finset ι) (F : ι → Polynomial ℚ) : Err r n p (∑ i ∈ t, F i) = ∑ i ∈ t, Err r n p (F i)

theorem Zeta32.PrimeEdge.locValue_mul_mprod (s : ℚ) (M : Finset ℕ) (P : Polynomial ℚ) : locValue s (P * mprod M) M = locPoly s P

theorem Zeta32.PrimeEdge.natDegree_comp_lin_le (Q : Polynomial ℚ) (p b : ℕ) : (Q.comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b)).natDegree ≤ Q.natDegree

theorem Zeta32.PrimeEdge.card_nearSet_le {p : ℕ} (hp : 0 < p) (n b : ℕ) : (nearSet n p b).card ≤ 5 * n

theorem Zeta32.PrimeEdge.dl_poly {p : ℕ} (hp : 0 < p) (r : ℚ) (n b : ℕ) (hb : b < p) (Q : Polynomial ℚ) (hQ : Q.natDegree + 5 * n < truncOrder n) : dl r n p b (Q * mprod (Finset.Icc 1 (5 * n))) = locPoly (r * ↑p) (Q.comp (Polynomial.C ↑p * Polynomial.X - Polynomial.C ↑b))

On the disc b, dl of Q · D_{5n} is locPoly (r p) (Q (p u - b)).

theorem Zeta32.PrimeEdge.Err_poly {p : ℕ} (hp : 0 < p) (r : ℚ) (n : ℕ) (Q : Polynomial ℚ) (hQ : Q.natDegree + 5 * n < truncOrder n) : Err r n p (Q * mprod (Finset.Icc 1 (5 * n))) = 0

The distribution formula is exact on Q · D_{5n}.