Generic factors with independent integral coefficient parameters. Specializing the logarithmic pair at (x^a,1) proves that the generic pair is nonzero.

noncomputable def CCDN.eulerPolynomialFromCoefficients {R : Type u_1} [CommRing R] (d : ℕ) (c : EulerLowIndex d → R) : Polynomial (Polynomial R)

The bivariate polynomial of total degree at most d with monomial coefficients c.

Equations

• CCDN.eulerPolynomialFromCoefficients d c = ∑ i : CCDN.EulerLowIndex d, c i • CCDN.eulerCoefficientMonomial R d i

theorem CCDN.eulerPolynomialFromCoefficients_degree {R : Type u_1} [CommRing R] (d : ℕ) (c : EulerLowIndex d → R) : bivariateTotalDegree (eulerPolynomialFromCoefficients d c) ≤ d

The polynomial eulerPolynomialFromCoefficients d c has total degree at most d.

@[reducible, inline]

abbrev CCDN.EulerFactorParameters (a b : ℕ) : Type

Index set of the coefficient parameters of a pair of generic factors of total degrees at most a and b.

Equations

• CCDN.EulerFactorParameters a b = (CCDN.EulerLowIndex a ⊕ CCDN.EulerLowIndex b)

noncomputable def CCDN.genericEulerFactorLeft (a b : ℕ) : Polynomial (Polynomial (MvPolynomial (EulerFactorParameters a b) ℤ))

The generic bivariate polynomial of total degree at most a, whose coefficients are independent integer variables.

Equations

• CCDN.genericEulerFactorLeft a b = CCDN.eulerPolynomialFromCoefficients a fun (i : CCDN.EulerLowIndex a) => MvPolynomial.X (Sum.inl i)

noncomputable def CCDN.genericEulerFactorRight (a b : ℕ) : Polynomial (Polynomial (MvPolynomial (EulerFactorParameters a b) ℤ))

The generic bivariate polynomial of total degree at most b, whose coefficients are independent integer variables, disjoint from those of genericEulerFactorLeft a b.

Equations

• CCDN.genericEulerFactorRight a b = CCDN.eulerPolynomialFromCoefficients b fun (i : CCDN.EulerLowIndex b) => MvPolynomial.X (Sum.inr i)

noncomputable def CCDN.genericEulerFactorSpecialization {R : Type u_1} [CommRing R] (a b : ℕ) (g h : Polynomial (Polynomial R)) : MvPolynomial (EulerFactorParameters a b) ℤ →+* R

The ring homomorphism specializing the generic factors to g and h, sending each coefficient variable to the corresponding coefficient of g or h.

Equations

• CCDN.genericEulerFactorSpecialization a b g h = MvPolynomial.eval₂Hom (Int.castRingHom R) (Sum.elim (CCDN.eulerCoefficientData a g) (CCDN.eulerCoefficientData b h))

theorem CCDN.genericEulerFactorLeft_specialize {R : Type u_1} [CommRing R] (a b : ℕ) (g h : Polynomial (Polynomial R)) (hg : bivariateTotalDegree g ≤ a) : (bivariateMap (genericEulerFactorSpecialization a b g h)) (genericEulerFactorLeft a b) = g

If g has total degree at most a, then genericEulerFactorLeft a b specializes to g.

theorem CCDN.genericEulerFactorRight_specialize {R : Type u_1} [CommRing R] (a b : ℕ) (g h : Polynomial (Polynomial R)) (hh : bivariateTotalDegree h ≤ b) : (bivariateMap (genericEulerFactorSpecialization a b g h)) (genericEulerFactorRight a b) = h

If h has total degree at most b, then genericEulerFactorRight a b specializes to h.

theorem CCDN.eulerFactorPair_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (a b : ℕ) (g h : Polynomial (Polynomial R)) : ((bivariateMap φ) (eulerFactorPair a b g h).1, (bivariateMap φ) (eulerFactorPair a b g h).2) = eulerFactorPair a b ((bivariateMap φ) g) ((bivariateMap φ) h)

The logarithmic factor pair commutes with applying a coefficient ring homomorphism to both factors.

theorem CCDN.genericEulerFactorPair_ne_zero (a b : ℕ) (ha : 0 < a) (hb : 0 < b) : eulerFactorPair a b (genericEulerFactorLeft a b) (genericEulerFactorRight a b) ≠ 0

The generic logarithmic pair is nonzero over its integral coefficient ring, proved by a rational specialization.