Content after restriction to an arithmetic progression

noncomputable def NairTenenbaum.affineRestriction (Q : Polynomial ℤ) (M a : ℤ) : Polynomial ℤ

The polynomial obtained by restricting to an arithmetic progression.

Equations

• NairTenenbaum.affineRestriction Q M a = Q.comp (Polynomial.C M * Polynomial.X + Polynomial.C a)

theorem NairTenenbaum.affineRestriction_eq_taylor_comp (Q : Polynomial ℤ) (M a : ℤ) : affineRestriction Q M a = ((Polynomial.taylor a) Q).comp (Polynomial.C M * Polynomial.X)

theorem NairTenenbaum.affineRestriction_coeff (Q : Polynomial ℤ) (M a : ℤ) (i : ℕ) : (affineRestriction Q M a).coeff i = ((Polynomial.taylor a) Q).coeff i * M ^ i

theorem NairTenenbaum.affineRestriction_coeff_zero (Q : Polynomial ℤ) (M a : ℤ) : (affineRestriction Q M a).coeff 0 = Polynomial.eval a Q

theorem NairTenenbaum.affineRestriction_coeff_one (Q : Polynomial ℤ) (M a : ℤ) : (affineRestriction Q M a).coeff 1 = Polynomial.eval a (Polynomial.derivative Q) * M

theorem NairTenenbaum.affineRestriction_content_not_dvd {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {p M a : ℤ} (hp : Prime p) {m : ℕ} (hM : ¬p ^ (m + 1) ∣ M) (hD : ¬p ^ m ∣ Q.discr) : ¬p ^ (2 * m) ∣ (affineRestriction Q M a).content

theorem NairTenenbaum.affineRestriction_primPart_high_coeff_dvd {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {p : ℕ} (hp : Nat.Prime p) {M a : ℤ} {m : ℕ} (hMp : ↑p ^ m ∣ M) (hM : ¬↑p ^ (m + 1) ∣ M) (hD : ¬↑p ^ m ∣ Q.discr) {i : ℕ} (hi : 2 ≤ i) : ↑p ∣ (affineRestriction Q M a).primPart.coeff i