Subset-sum polynomial

The polynomial ∏ x ∈ s, (X - C x) attached to a multiset s and its factorization according to the vanishing subset sums, used to track integer divisibility in Niven's argument.

noncomputable def polyOfMultiset {S : Type u_1} [CommRing S] (s : Multiset S) : Polynomial S

The polynomial ∏ x ∈ s, (X - C x) associated to a multiset s.

Equations

• polyOfMultiset s = (Multiset.map (fun (a : S) => Polynomial.X - Polynomial.C a) s).prod

theorem polyOfMultiset_split_zero {S : Type u_1} [CommRing S] [DecidableEq S] (s : Multiset S) : polyOfMultiset s = Polynomial.X ^ Multiset.count 0 s * polyOfMultiset (Multiset.filter (fun (x : S) => x ≠ 0) s)

∏_{a ∈ s} (X - a) = X^{#{a ∈ s, a = 0}} ∏_{a ∈ s, a ≠ 0} (X - a).

noncomputable def varsFin (n : ℕ) : Multiset (MvPolynomial (Fin n) ℤ)

The multiset {X₀, …, Xₙ₋₁} inside ℤ[X₀, …, Xₙ₋₁].

Equations

• varsFin n = Multiset.map MvPolynomial.X Finset.univ.val

noncomputable def polyOfSubsetSums {S : Type u_1} [CommRing S] (s : Multiset S) : Polynomial S

The polynomial whose roots are { ∑_{x ∈ t} x | t ⊆ s } for a given multiset s.

Equations

• polyOfSubsetSums s = polyOfMultiset (subsetSums s)

noncomputable def polyOfNonzeroSubsetSums {S : Type u_1} [CommRing S] [DecidableEq S] (s : Multiset S) : Polynomial S

The polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s } for a given multiset s.

Equations

• polyOfNonzeroSubsetSums s = polyOfMultiset (nonzeroSubsetSums s)

theorem polyOfNonzeroSubsetSums_monic {S : Type u_1} [CommRing S] [DecidableEq S] (s : Multiset S) : (polyOfNonzeroSubsetSums s).Monic

The polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s } for a given multiset s is monic.

theorem ne_zero_of_nonzeroSubsetSums_eq_valuesFin {S : Type u_1} [AddCommMonoid S] [DecidableEq S] {s : Multiset S} {n : ℕ} {a : Fin n → S} (ha : nonzeroSubsetSums s = valuesFin a) (i : Fin n) : a i ≠ 0

If { ∑_{x ∈ t} x ≠ 0 | t ⊆ s } is indexed by a : Fin n → S, then every a i is nonzero.

noncomputable def esymmVarsFinSubsetSums (n r : ℕ) : MvPolynomial (Fin n) ℤ

The r-th elementary symmetric polynomial in { ∑_{i ∈ I} Xᵢ | I ⊆ {0, …, n-1} }.

Equations

• esymmVarsFinSubsetSums n r = (subsetSums (varsFin n)).esymm r

theorem powerset_map_eq {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) : Multiset.map (Multiset.map f) s.powerset = (Multiset.map f s).powerset

Taking powersets commutes with mapping a function over a multiset.

theorem varsFin_IsSymmetric (n : ℕ) (e : Equiv.Perm (Fin n)) : Multiset.map (⇑(MvPolynomial.rename ⇑e)) (varsFin n) = varsFin n

The multiset {X₀, …, Xₙ₋₁} is invariant under permutation of the variables.

theorem varsFinSubsetSums_IsSymmetric (n : ℕ) (e : Equiv.Perm (Fin n)) : Multiset.map (⇑(MvPolynomial.rename ⇑e)) (subsetSums (varsFin n)) = subsetSums (varsFin n)

The multiset of subset sums of X₀, …, Xₙ₋₁ is invariant under permutation of the variables.

theorem multisetEsymm_IsSymmetric {n r : ℕ} (e : Equiv.Perm (Fin n)) (s : Multiset (MvPolynomial (Fin n) ℤ)) : (MvPolynomial.rename ⇑e) (s.esymm r) = (Multiset.map (⇑(MvPolynomial.rename ⇑e)) s).esymm r

Renaming variables commutes with the elementary symmetric polynomial of a multiset.

theorem esymmVarsFinSubsetSums_isSymmetric (n r : ℕ) : (esymmVarsFinSubsetSums n r).IsSymmetric

The r-th elementary symmetric polynomial in { ∑_{i ∈ I} Xᵢ | I ⊆ {0, …, n-1} } is symmetric.

theorem aeval_varsFin {S : Type u_1} [CommRing S] (n : ℕ) (b : Fin n → S) : Multiset.map (⇑(MvPolynomial.aeval b)) (varsFin n) = valuesFin b

Evaluating {X₀, …, Xₙ₋₁} at b gives the multiset {b₀, …, bₙ₋₁}.

theorem aeval_subsetSums {S : Type u_1} [CommRing S] (n : ℕ) (b : Fin n → S) : Multiset.map (⇑(MvPolynomial.aeval b)) (subsetSums (varsFin n)) = subsetSums (valuesFin b)

Evaluating the subset sums of {X₀, …, Xₙ₋₁} at b is the subset sums of {b₀, …, bₙ₋₁}.

theorem aeval_esymmVarsFinSubsetSums {S : Type u_1} [CommRing S] (n r : ℕ) (b : Fin n → S) : (MvPolynomial.aeval b) (esymmVarsFinSubsetSums n r) = (subsetSums (valuesFin b)).esymm r

Evaluating the r-th elementary symmetric polynomial in { ∑_{i ∈ I} Xᵢ | I ⊆ {0, …, n-1} } at b gives the r-th elementary symmetric polynomial in the subset sums of {b₀, …, bₙ₋₁}.

theorem coeff_polyOfSubsetSums {S : Type u_1} [CommRing S] (n : ℕ) (b : Fin n → S) (k : ℕ) (hk : k ≤ (subsetSums (valuesFin b)).card) : (polyOfSubsetSums (valuesFin b)).coeff k = (MvPolynomial.aeval b) ((-1) ^ ((subsetSums (valuesFin b)).card - k) * esymmVarsFinSubsetSums n ((subsetSums (valuesFin b)).card - k))

The k-th coefficient of the polynomial whose roots are { ∑_{x ∈ t} x | t ⊆ b } is given by an elementary symmetric polynomial in { ∑_{i ∈ I} Xᵢ | I ⊆ {0, …, n-1} } at b.

theorem coeff_polyOfSubsetSums_as_coeff_poly {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] {n : ℕ} (B : Polynomial R) (b : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin b) {k : ℕ} (hk : k ≤ (subsetSums (valuesFin b)).card) : ∃ (Q : MvPolynomial (Fin n) ℤ), (polyOfSubsetSums (valuesFin b)).coeff k = (algebraMap R S) ((MvPolynomial.aeval fun (i : Fin n) => (-1) ^ (↑i + 1) * B.coeff (n - (↑i + 1))) Q)

If B is monic with roots b₀, …, bₙ₋₁, then the coefficients of the polynomial whose roots are { ∑_{x ∈ t} x | t ⊆ b } are polynomials in the coefficients of B.

theorem coeff_polyOfNonzeroSubsetSums_as_coeff_poly {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] [DecidableEq S] {n k : ℕ} (B : Polynomial R) (b : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin b) (hk : k + Multiset.count 0 (subsetSums (valuesFin b)) ≤ (subsetSums (valuesFin b)).card) : ∃ (Q : MvPolynomial (Fin n) ℤ), (polyOfNonzeroSubsetSums (valuesFin b)).coeff k = (algebraMap R S) ((MvPolynomial.aeval fun (i : Fin n) => (-1) ^ (↑i + 1) * B.coeff (n - (↑i + 1))) Q)

If B is monic with roots b₀, …, bₙ₋₁, then the coefficients of the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ b } are polynomials in the coefficients of B.

theorem polyOfNonzeroSubsetSums_as_poly {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] [DecidableEq S] {n : ℕ} (B : Polynomial R) (a : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin a) : ∃ (P : Polynomial R), Polynomial.map (algebraMap R S) P = polyOfNonzeroSubsetSums (valuesFin a)

From a monic polynomial B with roots a₀, …, aₙ₋₁, one obtains a polynomial over the base ring whose image has roots the nonzero subset sums of the a_i.

theorem ClearDenominatorOf (T' : Polynomial ℚ) : ∃ (T : Polynomial ℤ) (c : ℤ), c ≠ 0 ∧ Polynomial.map (algebraMap ℤ ℚ) T = c • T'

Clearing denominators for a polynomial over ℚ: every rational polynomial is a nonzero integer multiple of the image of some polynomial over ℤ.

def monicRescaleCoeff (T : Polynomial ℤ) (d : ℕ) (c : ℤ) (k : ℕ) : ℤ

The rescaled coefficient used to build the monic degree d polynomial attached to T. Precisely, they are cᵈ⁻¹⁻ᵏ Tₖ for k < d, = 1 for k = d, and = 0 for k > d

Equations

• monicRescaleCoeff T d c k = if k < d then c ^ (d - 1 - k) * T.coeff k else if k = d then 1 else 0

def monicRescaleOf (T : Polynomial ℤ) (d : ℕ) (c : ℤ) : Polynomial ℤ

The monic degree d polynomial obtained by rescaling the lower coefficients of T. Precisely, it is the polynomial Xᵈ + ∑ₖ₌₀ᵈ⁻¹ cᵈ⁻¹⁻ᵏ Tₖ Xᵏ

Equations

• monicRescaleOf T d c = (Polynomial.ofFn (d + 1)) fun (i : Fin (d + 1)) => if ↑i = d then 1 else c ^ (d - 1 - ↑i) * T.coeff ↑i

theorem coeff_monicRescaleOf (T : Polynomial ℤ) (d : ℕ) (c : ℤ) (k : ℕ) : (monicRescaleOf T d c).coeff k = monicRescaleCoeff T d c k

The coefficients of Xᵈ + ∑ₖ₌₀ᵈ⁻¹ cᵈ⁻¹⁻ᵏ Tₖ Xᵏ.

theorem natDegree_monicRescaleOf (T : Polynomial ℤ) (d : ℕ) (c : ℤ) : (monicRescaleOf T d c).natDegree = d

Xᵈ + ∑ₖ₌₀ᵈ⁻¹ cᵈ⁻¹⁻ᵏ Tₖ Xᵏ has degree d.

theorem monic_monicRescaleOf (T : Polynomial ℤ) (d : ℕ) (c : ℤ) : (monicRescaleOf T d c).Monic

Xᵈ + ∑ₖ₌₀ᵈ⁻¹ cᵈ⁻¹⁻ᵏ Tₖ Xᵏ is monic.

theorem coeff_monicRescaleOf_scaleRoots (T : Polynomial ℤ) (T' : Polynomial ℚ) (d : ℕ) (c : ℤ) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (algebraMap ℤ ℚ) T = Polynomial.C ↑c * T') (k : ℕ) : (Polynomial.map (algebraMap ℤ ℚ) (monicRescaleOf T d c)).coeff k = (T'.scaleRoots ↑c).coeff k

Coefficients of Xᵈ + ∑ₖ₌₀ᵈ⁻¹ cᵈ⁻¹⁻ᵏ Tₖ Xᵏ correspond to the coefficients of scaleRoots.

theorem monicRescaleOf_scaleRoots (T : Polynomial ℤ) (T' : Polynomial ℚ) (d : ℕ) (c : ℤ) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (algebraMap ℤ ℚ) T = Polynomial.C ↑c * T') : Polynomial.map (algebraMap ℤ ℚ) (monicRescaleOf T d c) = T'.scaleRoots ↑c

After mapping to ℚ, the monic rescaling is the scaleRoots of the monic rational polynomial T'.

theorem aroots_monicRescaleOf (T : Polynomial ℤ) (T' : Polynomial ℚ) (d : ℕ) (c : ℤ) (a : Fin d → ℂ) (hc : c ≠ 0) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') (hroots' : T'.aroots ℂ = valuesFin a) : (monicRescaleOf T d c).aroots ℂ = valuesFin fun (j : Fin d) => ↑c * a j

If T = c T' with T' monic of degree d and roots a₀, …, a_{d-1}, then Xᵈ + ∑ₖ₌₀ᵈ⁻¹ cᵈ⁻¹⁻ᵏ Tₖ Xᵏ is the monic polynomial whose roots are c a₀, …, c a_{d-1}.

theorem monic_of_T' (T' : Polynomial ℚ) (d : ℕ) (r : Fin d → ℂ) (hT' : Polynomial.map (algebraMap ℚ ℂ) T' = polyOfNonzeroSubsetSums (valuesFin r)) : T'.Monic

If T' is the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }, then T' is monic.

theorem natDegree_of_T' (T' : Polynomial ℚ) (d n : ℕ) (r : Fin d → ℂ) (a : Fin n → ℂ) (hT' : Polynomial.map (algebraMap ℚ ℂ) T' = polyOfNonzeroSubsetSums (valuesFin r)) (ha : nonzeroSubsetSums (valuesFin r) = valuesFin a) : T'.natDegree = n

If T' is the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }, then deg(T') is the number of those roots.

theorem aroots_of_T' (T' : Polynomial ℚ) (d n : ℕ) (r : Fin d → ℂ) (a : Fin n → ℂ) (hT' : Polynomial.map (algebraMap ℚ ℂ) T' = polyOfNonzeroSubsetSums (valuesFin r)) (ha : nonzeroSubsetSums (valuesFin r) = valuesFin a) : T'.aroots ℂ = valuesFin a

If T' is the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }, then its roots are exactly that multiset.

theorem aeval_zero_ne_zero_of_T' (T' : Polynomial ℚ) (d n : ℕ) (r : Fin d → ℂ) (a : Fin n → ℂ) (hT' : Polynomial.map (algebraMap ℚ ℂ) T' = polyOfNonzeroSubsetSums (valuesFin r)) (ha : nonzeroSubsetSums (valuesFin r) = valuesFin a) : (Polynomial.aeval 0) T' ≠ 0

If T' is the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }, then T'(0) ≠ 0.

theorem aroots_of_T (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (d n : ℕ) (r : Fin d → ℂ) (a : Fin n → ℂ) (hc : c ≠ 0) (hT : Polynomial.map (Int.castRingHom ℚ) T = c • T') (hT' : Polynomial.map (algebraMap ℚ ℂ) T' = polyOfNonzeroSubsetSums (valuesFin r)) (ha : nonzeroSubsetSums (valuesFin r) = valuesFin a) : T.aroots ℂ = valuesFin a

If T = c • T', and T' is the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }, then the roots of T are also { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }.

theorem RescaledOf_nonZero (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (hc : c ≠ 0) (hT' : T' ≠ 0) (hT : Polynomial.map (algebraMap ℤ ℚ) T = Polynomial.C ↑c * T') : T ≠ 0

If c ≠ 0, T' ≠ 0, and c * T' = T ∈ ℤ[X], then T ≠ 0.

theorem RescaledOf_natDegree (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (hc : c ≠ 0) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') : T.natDegree = T'.natDegree

If c ≠ 0 and c * T' = T ∈ ℤ[X], then deg(T) = deg(T').

theorem RescaledOf_nonZero_at_Zero (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (hc : c ≠ 0) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') (hT'0 : (Polynomial.aeval 0) T' ≠ 0) : (Polynomial.aeval 0) T ≠ 0

If T'(0) ≠ 0 and c * T' = T ∈ ℤ[X], then T(0) ≠ 0.

theorem aeval_zero_ne_zero_of_T (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (d n : ℕ) (r : Fin d → ℂ) (a : Fin n → ℂ) (hc : c ≠ 0) (hT : Polynomial.map (Int.castRingHom ℚ) T = c • T') (hT' : Polynomial.map (algebraMap ℚ ℂ) T' = polyOfNonzeroSubsetSums (valuesFin r)) (ha : nonzeroSubsetSums (valuesFin r) = valuesFin a) : (Polynomial.aeval 0) T ≠ 0

If T = c • T', and T' is the polynomial whose roots are { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }, then T(0) ≠ 0.