Fel's Conjecture for Numerical Semigroups

structure NumericalSemigroup : Type

A numerical semigroup: an additive submonoid of ℕ with finite complement.

• carrier : Set ℕ

  The underlying set of natural numbers comprising the semigroup.

• zero_mem : 0 ∈ self.carrier
• add_mem (a b : ℕ) : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• finite_complement : self.carrierᶜ.Finite

noncomputable def NumericalSemigroup.gaps (S : NumericalSemigroup) : Finset ℕ

The gaps of S: the (finite) complement ℕ \ S as a Finset.

Equations

• S.gaps = ⋯.toFinset

noncomputable def NumericalSemigroup.gapPowerSum (S : NumericalSemigroup) (r : ℕ) : ℚ

The gap power sum G_r(S) = ∑_{g ∈ Δ} g^r (Definition 3 in the paper).

Equations

• S.gapPowerSum r = ∑ g ∈ S.gaps, ↑g ^ r

noncomputable def NumericalSemigroup.gapPolynomial (S : NumericalSemigroup) : Polynomial ℚ

The gap polynomial Φ_S(z) = ∑_{g ∈ Δ} z^g (Definition 4 in the paper).

Equations

• S.gapPolynomial = ∑ g ∈ S.gaps, Polynomial.X ^ g

noncomputable def NumericalSemigroup.hilbertSeries (S : NumericalSemigroup) : PowerSeries ℚ

The Hilbert series H_S(z) = ∑_{s ∈ S} z^s, expressed as a formal power series.

Equations

• S.hilbertSeries = PowerSeries.mk fun (n : ℕ) => if decide (n ∈ S.carrier) = true then 1 else 0

theorem NumericalSemigroup.hilbertSeries_coeff (S : NumericalSemigroup) (n : ℕ) : (PowerSeries.coeff n) S.hilbertSeries = if decide (n ∈ S.carrier) = true then 1 else 0

The coefficient of the Hilbert series at position n is 1 if n ∈ S.carrier, else 0.

theorem NumericalSemigroup.gapPolynomial_coeff (S : NumericalSemigroup) (n : ℕ) : (PowerSeries.coeff n) ↑S.gapPolynomial = if n ∈ S.gaps then 1 else 0

The coefficient of the gap polynomial (viewed as a power series) at position n is 1 if n ∈ S.gaps, else 0.

theorem NumericalSemigroup.mem_gaps_iff_not_mem_carrier (S : NumericalSemigroup) (n : ℕ) : n ∈ S.gaps ↔ n ∉ S.carrier

For any n, we have n ∈ S.gaps ↔ n ∉ S.carrier.

theorem NumericalSemigroup.semigroupGapDecomposition_aux (S : NumericalSemigroup) (n : ℕ) : (PowerSeries.coeff n) (S.hilbertSeries + ↑S.gapPolynomial) = (PowerSeries.coeff n) (PowerSeries.mk 1)

theorem NumericalSemigroup.semigroupGapDecomposition (S : NumericalSemigroup) : S.hilbertSeries + ↑S.gapPolynomial = PowerSeries.mk 1

structure NumericalSemigroupGenerators (S : NumericalSemigroup) : Type

A choice of generators for a numerical semigroup S: positive integers d₁, …, d_m with gcd = 1 whose nonneg-integer combinations recover S.carrier.

• m : ℕ

  The number of generators (embedding dimension of S).

• hm_pos : 0 < self.m
• d : Fin self.m → ℕ

  The chosen generators d₁, …, d_m.

• hd_pos (i : Fin self.m) : 0 < self.d i
• hgcd : (Finset.image self.d Finset.univ).gcd id = 1
• generates : S.carrier = {n : ℕ | ∃ (c : Fin self.m → ℕ), n = ∑ i : Fin self.m, c i * self.d i}

def NumericalSemigroupGenerators.piM {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : ℕ

The product of generators π_m = ∏ᵢ dᵢ (Definition 6 in the paper).

Equations

• G.piM = ∏ i : Fin G.m, G.d i

noncomputable def NumericalSemigroupGenerators.productPolynomial {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : Polynomial ℤ

The product polynomial P_S(z) = ∏ᵢ (1 - z^{dᵢ}) (Definition 6 in the paper).

Equations

• G.productPolynomial = ∏ i : Fin G.m, (1 - Polynomial.X ^ G.d i)

noncomputable def NumericalSemigroupGenerators.hilbertNumeratorDegBound {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : ℕ

Upper bound on the degree of the Hilbert numerator Q_S(z).

Equations

• G.hilbertNumeratorDegBound = G.productPolynomial.natDegree + S.gaps.sup id + 1

noncomputable def NumericalSemigroupGenerators.hilbertNumerator {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : Polynomial ℤ

The Hilbert numerator Q_S(z), computed coefficient-wise from P_S and the gaps.

Equations

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

theorem NumericalSemigroupGenerators.coeff_mul_hilbert_product {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (S.hilbertSeries * ↑(Polynomial.map (Int.castRingHom ℚ) G.productPolynomial)) = ∑ k ∈ Finset.range (n + 1), (PowerSeries.coeff k) S.hilbertSeries * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k))

theorem NumericalSemigroupGenerators.hilbertNumerator_coeff_lt {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n < G.hilbertNumeratorDegBound) : G.hilbertNumerator.coeff n = ∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k - ∑ g ∈ S.gaps with g ≤ n, G.productPolynomial.coeff (n - g)

theorem NumericalSemigroupGenerators.hilbertNumerator_coeff_ge {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n ≥ G.hilbertNumeratorDegBound) : G.hilbertNumerator.coeff n = 0

theorem NumericalSemigroupGenerators.coeff_hilbertNumerator_formula {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) ↑(Polynomial.map (Int.castRingHom ℚ) G.hilbertNumerator) = if n < G.hilbertNumeratorDegBound then (Int.castRingHom ℚ) (∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k - ∑ g ∈ S.gaps with g ≤ n, G.productPolynomial.coeff (n - g)) else 0

theorem NumericalSemigroupGenerators.lhs_eq_sum_over_carrier {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (if decide (k ∈ S.carrier) = true then 1 else 0) * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = ∑ k ∈ Finset.range (n + 1) with decide (k ∈ S.carrier) = true, (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k))

theorem NumericalSemigroupGenerators.partition_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = ∑ k ∈ Finset.range (n + 1) with decide (k ∈ S.carrier) = true, (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) + ∑ k ∈ Finset.range (n + 1) with (!decide (k ∈ S.carrier)) = true, (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k))

theorem NumericalSemigroupGenerators.filter_not_carrier_eq_gaps {S : NumericalSemigroup} (n : ℕ) : {k ∈ Finset.range (n + 1) | (!decide (k ∈ S.carrier)) = true} = {x ∈ S.gaps | x ≤ n}

theorem NumericalSemigroupGenerators.carrier_sum_eq_full_minus_gaps {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1) with decide (k ∈ S.carrier) = true, (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = ∑ k ∈ Finset.range (n + 1), (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) - ∑ g ∈ S.gaps with g ≤ n, (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - g))

theorem NumericalSemigroupGenerators.indicator_sum_eq_full_minus_gaps {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (if decide (k ∈ S.carrier) = true then 1 else 0) * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = ∑ k ∈ Finset.range (n + 1), (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) - ∑ g ∈ S.gaps with g ≤ n, (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - g))

theorem NumericalSemigroupGenerators.sum_coeff_reindex {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = ∑ j ∈ Finset.range (n + 1), (Int.castRingHom ℚ) (G.productPolynomial.coeff j)

theorem NumericalSemigroupGenerators.lhs_eq_hilbertNumerator_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n < G.hilbertNumeratorDegBound) : ∑ k ∈ Finset.range (n + 1), (if decide (k ∈ S.carrier) = true then 1 else 0) * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = (Int.castRingHom ℚ) (G.hilbertNumerator.coeff n)

theorem NumericalSemigroupGenerators.sum_range_reindex (f : ℕ → ℚ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), f (n - k) = ∑ j ∈ Finset.range (n + 1), f j

theorem NumericalSemigroupGenerators.large_n_both_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (_hn : n ≥ G.hilbertNumeratorDegBound) : ∑ k ∈ Finset.range (n + 1), (if decide (k ∈ S.carrier) = true then 1 else 0) * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = (Int.castRingHom ℚ) (∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k - ∑ g ∈ S.gaps with g ≤ n, G.productPolynomial.coeff (n - g))

theorem NumericalSemigroupGenerators.sum_over_semigroup_eq_diff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (if decide (k ∈ S.carrier) = true then 1 else 0) * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k)) = (Int.castRingHom ℚ) (∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k - ∑ g ∈ S.gaps with g ≤ n, G.productPolynomial.coeff (n - g))

theorem NumericalSemigroupGenerators.coeff_mul_eq_indicator_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (S.hilbertSeries * ↑(Polynomial.map (Int.castRingHom ℚ) G.productPolynomial)) = ∑ k ∈ Finset.range (n + 1), (if decide (k ∈ S.carrier) = true then 1 else 0) * (Int.castRingHom ℚ) (G.productPolynomial.coeff (n - k))

theorem NumericalSemigroupGenerators.productPolynomial_eval_one {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : Polynomial.eval 1 G.productPolynomial = 0

theorem NumericalSemigroupGenerators.sum_coeff_eq_eval_one {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : ∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), G.productPolynomial.coeff k = Polynomial.eval 1 G.productPolynomial

theorem NumericalSemigroupGenerators.coeff_Ico_eq_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (_hn : G.productPolynomial.natDegree + 1 ≤ n) (k : ℕ) (hk : k ∈ Finset.Ico (G.productPolynomial.natDegree + 1) (n + 1)) : G.productPolynomial.coeff k = 0

theorem NumericalSemigroupGenerators.sum_coeff_large_eq_sum_coeff_deg {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : G.productPolynomial.natDegree + 1 ≤ n) : ∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k = ∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), G.productPolynomial.coeff k

theorem NumericalSemigroupGenerators.first_sum_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n ≥ G.hilbertNumeratorDegBound) : ∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k = 0

theorem NumericalSemigroupGenerators.coeff_n_minus_gap_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n g : ℕ) (hn : n ≥ G.hilbertNumeratorDegBound) (hg : g ∈ S.gaps) (hgn : g ≤ n) : G.productPolynomial.coeff (n - g) = 0

theorem NumericalSemigroupGenerators.second_sum_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n ≥ G.hilbertNumeratorDegBound) : ∑ g ∈ S.gaps with g ≤ n, G.productPolynomial.coeff (n - g) = 0

theorem NumericalSemigroupGenerators.rhs_zero_of_large {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n ≥ G.hilbertNumeratorDegBound) : ∑ k ∈ Finset.range (n + 1), G.productPolynomial.coeff k - ∑ g ∈ S.gaps with g ≤ n, G.productPolynomial.coeff (n - g) = 0

theorem NumericalSemigroupGenerators.coeff_eq_zero_of_large {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : n ≥ G.hilbertNumeratorDegBound) : (PowerSeries.coeff n) (S.hilbertSeries * ↑(Polynomial.map (Int.castRingHom ℚ) G.productPolynomial)) = 0

theorem NumericalSemigroupGenerators.numeratorIdentity_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (S.hilbertSeries * ↑(Polynomial.map (Int.castRingHom ℚ) G.productPolynomial)) = (PowerSeries.coeff n) ↑(Polynomial.map (Int.castRingHom ℚ) G.hilbertNumerator)

theorem NumericalSemigroupGenerators.numeratorIdentity {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : S.hilbertSeries * ↑(Polynomial.map (Int.castRingHom ℚ) G.productPolynomial) = ↑(Polynomial.map (Int.castRingHom ℚ) G.hilbertNumerator)

noncomputable def NumericalSemigroupGenerators.numeratorCoeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (j : ℕ) : ℤ

The coefficients cⱼ in the expansion Q_S(z) = 1 - ∑_{j ≥ 1} cⱼ z^j.

Equations

• G.numeratorCoeff j = if j = 0 then 0 else -G.hilbertNumerator.coeff j

noncomputable def NumericalSemigroupGenerators.alternatingPowerSum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ℚ

The alternating power sum C_n(S) = ∑_{j ≥ 1} cⱼ · jⁿ (Definition 8).

Equations

• G.alternatingPowerSum n = ∑ j ∈ Finset.range G.hilbertNumeratorDegBound, ↑(G.numeratorCoeff j) * ↑j ^ n

noncomputable def NumericalSemigroupGenerators.KInvariant {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ℚ

The invariant K_p(S) = ((-1)^m · p!) / ((m+p)! · π_m) · C_{m+p}(S) (Definition 9 in the paper).

Equations

• G.KInvariant p = (-1) ^ G.m * ↑p.factorial / (↑(G.m + p).factorial * ↑G.piM) * G.alternatingPowerSum (G.m + p)

noncomputable def NumericalSemigroupGenerators.scaledExpFactor {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (i : Fin G.m) : PowerSeries ℚ

The single factor `(e^{dᵢ t} -

1. / (dᵢ t) = ∑_k dᵢ^k · t^k / (k+1)!of theA` generating series.

Equations

• G.scaledExpFactor i = PowerSeries.mk fun (k : ℕ) => ↑(G.d i) ^ k / ↑(k + 1).factorial

noncomputable def NumericalSemigroupGenerators.ASeries {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : PowerSeries ℚ

The generating series A(t) = ∏ᵢ (e^{dᵢ t} - 1) / (dᵢ t) (Definition 10).

Equations

• G.ASeries = ∏ i : Fin G.m, G.scaledExpFactor i

noncomputable def NumericalSemigroupGenerators.TSigma {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ℚ

The symbol T_n(σ) = n! · [t^n] A(t) (Definition 10).

Equations

• G.TSigma n = ↑n.factorial * (PowerSeries.coeff n) G.ASeries

noncomputable def NumericalSemigroupGenerators.BSeries {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : PowerSeries ℚ

The generating series B(t) = (t / (e^t - 1)) · A(t) (Definition 11).

Equations

• G.BSeries = bernoulliPowerSeries ℚ * G.ASeries

noncomputable def NumericalSemigroupGenerators.TDelta {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ℚ

The symbol T_n(δ) = (n! / 2^n) · [t^n] B(t) (Definition 11).

Equations

• G.TDelta n = ↑n.factorial / 2 ^ n * (PowerSeries.coeff n) G.BSeries

theorem FelsConjectureProof.pi_m_pos {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : 0 < G.piM

theorem FelsConjectureProof.choose_mul_sub_factorial_eq_div (n r : ℕ) (hr : r ≤ n) : ↑(n.choose r) * ↑(n - r).factorial = ↑n.factorial / ↑r.factorial

theorem FelsConjectureProof.bernoulli_term_simplify (m p piM : ℕ) (hpi : 0 < piM) (coeff : ℚ) : (-1) ^ m * ↑p.factorial / (↑(m + p).factorial * ↑piM) * ((-1) ^ m * ↑piM * ↑(m + p).factorial * coeff) = ↑p.factorial * coeff

theorem FelsConjectureProof.outer_factor_cancel {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) (sum_term : ℚ) : (-1) ^ G.m * ↑p.factorial / (↑(G.m + p).factorial * ↑G.piM) * ((-1) ^ G.m * ↑G.piM * sum_term) = ↑p.factorial / ↑(G.m + p).factorial * sum_term

theorem FelsConjectureProof.term_simplify (m p r : ℕ) (hr : r ≤ p) (A_coeff G_r : ℚ) : ↑p.factorial / ↑(m + p).factorial * (↑((m + p).choose r) * ↑(m + p - r).factorial * A_coeff * G_r) = ↑p.factorial / ↑r.factorial * A_coeff * G_r

theorem FelsConjectureProof.gap_sum_simplify {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : (-1) ^ G.m * ↑p.factorial / (↑(G.m + p).factorial * ↑G.piM) * ((-1) ^ G.m * ↑G.piM * ∑ r ∈ Finset.range (p + 1), ↑((G.m + p).choose r) * ↑(G.m + p - r).factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r) = ∑ r ∈ Finset.range (p + 1), ↑p.factorial / ↑r.factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r

noncomputable def FelsConjectureProof.QExpSeries {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : PowerSeries ℚ

Auxiliary series obtained by evaluating Q_S at t ↦ ∑ jⁿ t^n / n! per coordinate.

Equations

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

noncomputable def FelsConjectureProof.hilbertNumeratorExpSub {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : PowerSeries ℚ

Auxiliary helper: Q_S minus its constant term, evaluated coefficient-wise on the exponential expansion.

Equations

• FelsConjectureProof.hilbertNumeratorExpSub G = PowerSeries.mk fun (n : ℕ) => (∑ j ∈ Finset.range G.hilbertNumeratorDegBound, ↑(G.hilbertNumerator.coeff j) * ↑j ^ n) / ↑n.factorial

theorem FelsConjectureProof.hilbertNumerator_exp_sub_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (hilbertNumeratorExpSub G) = (∑ j ∈ Finset.range G.hilbertNumeratorDegBound, ↑(G.hilbertNumerator.coeff j) * ↑j ^ n) / ↑n.factorial

theorem FelsConjectureProof.alternatingPowerSum_eq_neg_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : 1 ≤ n) : G.alternatingPowerSum n = -∑ j ∈ Finset.range G.hilbertNumeratorDegBound, ↑(G.hilbertNumerator.coeff j) * ↑j ^ n

theorem FelsConjectureProof.alternatingPowerSum_eq_coeff_hilbert_exp {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : 1 ≤ n) : G.alternatingPowerSum n = -(↑n.factorial * (PowerSeries.coeff n) (hilbertNumeratorExpSub G))

theorem FelsConjectureProof.B_term_coeff_shift {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : (PowerSeries.coeff (G.m + p)) (PowerSeries.X ^ (G.m - 1) * G.BSeries) = (PowerSeries.coeff (p + 1)) G.BSeries

theorem FelsConjectureProof.coeff_A_mul_E {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : (PowerSeries.coeff p) (G.ASeries * PowerSeries.mk fun (n : ℕ) => ∑ g ∈ S.gaps, ↑g ^ n / ↑n.factorial) = ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ∑ g ∈ S.gaps, ↑g ^ r / ↑r.factorial

theorem FelsConjectureProof.sum_swap_gaps_range {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ∑ g ∈ S.gaps, ↑g ^ r / ↑r.factorial = ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r / ↑r.factorial

theorem FelsConjectureProof.gap_term_coeff_shift {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : (PowerSeries.coeff (G.m + p)) (PowerSeries.X ^ G.m * G.ASeries * PowerSeries.mk fun (n : ℕ) => ∑ g ∈ S.gaps, ↑g ^ n / ↑n.factorial) = ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r / ↑r.factorial

theorem FelsConjectureProof.Q_exp_coeff_at_m_plus_p {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : (PowerSeries.coeff (G.m + p)) (QExpSeries G) = (-1) ^ (G.m + 1) * ↑G.piM * ((PowerSeries.coeff (p + 1)) G.BSeries + ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r / ↑r.factorial)

theorem FelsConjectureProof.gap_coeff_to_leibniz {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ↑(G.m + p).factorial * ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r / ↑r.factorial = ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), ↑(G.m + p).factorial / ↑r.factorial * (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r

theorem FelsConjectureProof.gap_sum_swap {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), ↑(G.m + p).factorial / ↑r.factorial * (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r = ∑ r ∈ Finset.range (p + 1), ↑((G.m + p).choose r) * ↑(G.m + p - r).factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r

theorem FelsConjectureProof.gap_term_final_form {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ↑(G.m + p).factorial * ∑ g ∈ S.gaps, ∑ r ∈ Finset.range (p + 1), (PowerSeries.coeff (p - r)) G.ASeries * ↑g ^ r / ↑r.factorial = ∑ r ∈ Finset.range (p + 1), ↑((G.m + p).choose r) * ↑(G.m + p - r).factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r

noncomputable def FelsConjectureProof.expPolySub (P : Polynomial ℤ) : PowerSeries ℚ

For a polynomial P : ℤ[X], the formal power series ∑ₙ (P.coeff n : ℚ) · t^n / n! minus its constant term.

Equations

• FelsConjectureProof.expPolySub P = PowerSeries.mk fun (n : ℕ) => (∑ j ∈ Finset.range (P.natDegree + 1), ↑(P.coeff j) * ↑j ^ n) / ↑n.factorial

theorem FelsConjectureProof.exp_poly_sub_coeff (P : Polynomial ℤ) (n : ℕ) : (PowerSeries.coeff n) (expPolySub P) = (∑ j ∈ Finset.range (P.natDegree + 1), ↑(P.coeff j) * ↑j ^ n) / ↑n.factorial

theorem FelsConjectureProof.exp_poly_sub_sum_extend (P : Polynomial ℤ) (k n : ℕ) (hk : P.natDegree + 1 ≤ k) : ∑ j ∈ Finset.range (P.natDegree + 1), ↑(P.coeff j) * ↑j ^ n = ∑ j ∈ Finset.range k, ↑(P.coeff j) * ↑j ^ n

theorem FelsConjectureProof.hilbertNumerator_natDegree_le_pred_bound {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : G.hilbertNumerator.natDegree ≤ G.hilbertNumeratorDegBound - 1

theorem FelsConjectureProof.hilbertNumeratorDegBound_pos {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : 0 < G.hilbertNumeratorDegBound

theorem FelsConjectureProof.hilbertNumerator_natDegree_lt_bound {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : G.hilbertNumerator.natDegree + 1 ≤ G.hilbertNumeratorDegBound

theorem FelsConjectureProof.hilbertNumerator_exp_sub_eq_exp_poly_sub {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : hilbertNumeratorExpSub G = expPolySub G.hilbertNumerator

theorem FelsConjectureProof.Q_exp_series_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (QExpSeries G) = (-1) ^ (G.m + 1) * ↑G.piM * ((PowerSeries.coeff n) (PowerSeries.X ^ (G.m - 1) * G.BSeries) + (PowerSeries.coeff n) (PowerSeries.X ^ G.m * G.ASeries * PowerSeries.mk fun (k : ℕ) => ∑ g ∈ S.gaps, ↑g ^ k / ↑k.factorial))

theorem FelsConjectureProof.j_lt_bound_of_mem_range_natDegree {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (j : ℕ) (hj : j ∈ Finset.range (G.hilbertNumerator.natDegree + 1)) : j < G.hilbertNumeratorDegBound

theorem FelsConjectureProof.hilbert_sum_decomposition_natDegree {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), ↑(G.hilbertNumerator.coeff j) * ↑j ^ n = ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ↑j ^ n - ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ g ∈ S.gaps with g ≤ j, ↑(G.productPolynomial.coeff (j - g))) * ↑j ^ n

theorem FelsConjectureProof.partial_sum_eq_zero_when_large {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (D : ℕ) (hD : G.productPolynomial.natDegree ≤ D) : ∑ k ∈ Finset.range (D + 1), ↑(G.productPolynomial.coeff k) = 0

theorem FelsConjectureProof.leadingCoeff_one_sub_X_pow (k : ℕ) (hk : 0 < k) : (1 - Polynomial.X ^ k).leadingCoeff = -1

theorem FelsConjectureProof.productPolynomial_leadingCoeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : G.productPolynomial.leadingCoeff = (-1) ^ G.m

theorem FelsConjectureProof.natDegree_ge_of_gaps_nonempty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (h : S.gaps.Nonempty) : G.productPolynomial.natDegree ≤ G.hilbertNumerator.natDegree

theorem FelsConjectureProof.telescoping_general (D n : ℕ) (P : Polynomial ℤ) : ∑ j ∈ Finset.range (D + 1), (∑ k ∈ Finset.range (j + 1), ↑(P.coeff k)) * ((↑j + 1) ^ n - ↑j ^ n) = (∑ k ∈ Finset.range (D + 1), ↑(P.coeff k)) * (↑D + 1) ^ n - ∑ j ∈ Finset.range (D + 1), ↑(P.coeff j) * ↑j ^ n

theorem FelsConjectureProof.telescoping_sum_gaps_nonempty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hgaps : S.gaps.Nonempty) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ((↑j + 1) ^ n - ↑j ^ n) = -∑ j ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff j) * ↑j ^ n

theorem FelsConjectureProof.hilbertNumerator_coeff_eq_partial_sum_gaps_empty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hgaps : ¬S.gaps.Nonempty) (j : ℕ) (hj : j < G.hilbertNumeratorDegBound) : G.hilbertNumerator.coeff j = ∑ k ∈ Finset.range (j + 1), G.productPolynomial.coeff k

theorem FelsConjectureProof.partial_sum_zero_after_natDegree_gaps_empty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hgaps : ¬S.gaps.Nonempty) (j : ℕ) (hj1 : G.hilbertNumerator.natDegree < j) (hj2 : j < G.hilbertNumeratorDegBound) : ∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k) = 0

theorem FelsConjectureProof.coeff_eq_partial_sum_diff (P : Polynomial ℤ) (n : ℕ) : ↑(P.coeff n) = ∑ k ∈ Finset.range (n + 1), ↑(P.coeff k) - ∑ k ∈ Finset.range n, ↑(P.coeff k)

theorem FelsConjectureProof.coeff_at_D_plus_one_gaps_empty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hgaps : ¬S.gaps.Nonempty) (hbound : G.hilbertNumerator.natDegree + 1 < G.hilbertNumeratorDegBound) : ↑(G.productPolynomial.coeff (G.hilbertNumerator.natDegree + 1)) = -∑ k ∈ Finset.range (G.hilbertNumerator.natDegree + 1), ↑(G.productPolynomial.coeff k)

theorem FelsConjectureProof.coeff_zero_after_D_plus_one_gaps_empty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hgaps : ¬S.gaps.Nonempty) (_hbound : G.hilbertNumerator.natDegree + 1 < G.hilbertNumeratorDegBound) (j : ℕ) (hj_lo : G.hilbertNumerator.natDegree + 2 ≤ j) (hj_hi : j ≤ G.productPolynomial.natDegree) : ↑(G.productPolynomial.coeff j) = 0

theorem FelsConjectureProof.sum_tail_eq_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hgaps : ¬S.gaps.Nonempty) (hbound : G.hilbertNumerator.natDegree + 1 < G.hilbertNumeratorDegBound) : ∑ j ∈ Finset.Ico (G.hilbertNumerator.natDegree + 2) (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff j) * ↑j ^ n = 0

theorem FelsConjectureProof.poly_sum_tail_eq_neg_partial_gaps_empty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hgaps : ¬S.gaps.Nonempty) (hbound : G.hilbertNumerator.natDegree + 1 < G.hilbertNumeratorDegBound) : ∑ j ∈ Finset.Ico (G.hilbertNumerator.natDegree + 1) (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff j) * ↑j ^ n = (-∑ k ∈ Finset.range (G.hilbertNumerator.natDegree + 1), ↑(G.productPolynomial.coeff k)) * (↑G.hilbertNumerator.natDegree + 1) ^ n

theorem FelsConjectureProof.telescoping_sum_gaps_empty {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hgaps : ¬S.gaps.Nonempty) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ((↑j + 1) ^ n - ↑j ^ n) = -∑ j ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff j) * ↑j ^ n

theorem FelsConjectureProof.telescoping_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ((↑j + 1) ^ n - ↑j ^ n) = -∑ j ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff j) * ↑j ^ n

noncomputable def FelsConjectureProof.partialSumGenFunc {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : PowerSeries ℚ

Generating function for the partial sums of P_S.coeff along Finset.range.

Equations

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

theorem FelsConjectureProof.partialSumGenFunc_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (partialSumGenFunc G) = (∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ↑j ^ n) / ↑n.factorial

theorem FelsConjectureProof.exp_poly_sub_one : expPolySub 1 = 1

theorem FelsConjectureProof.coeff_mul_expand (P Q : Polynomial ℤ) (n : ℕ) : (PowerSeries.coeff n) (expPolySub P * expPolySub Q) = ∑ k ∈ Finset.range (n + 1), (∑ a ∈ Finset.range (P.natDegree + 1), ↑(P.coeff a) * ↑a ^ k) / ↑k.factorial * ((∑ b ∈ Finset.range (Q.natDegree + 1), ↑(Q.coeff b) * ↑b ^ (n - k)) / ↑(n - k).factorial)

theorem FelsConjectureProof.lhs_to_triple_sum (P Q : Polynomial ℤ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (∑ a ∈ Finset.range (P.natDegree + 1), ↑(P.coeff a) * ↑a ^ k) / ↑k.factorial * ((∑ b ∈ Finset.range (Q.natDegree + 1), ↑(Q.coeff b) * ↑b ^ (n - k)) / ↑(n - k).factorial) = ∑ k ∈ Finset.range (n + 1), ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑a ^ k * ↑b ^ (n - k) / (↑k.factorial * ↑(n - k).factorial)

theorem FelsConjectureProof.term_factorial_to_choose (Pa Qb : ℚ) (a b k n : ℕ) (hk : k ≤ n) : Pa * Qb * ↑a ^ k * ↑b ^ (n - k) / (↑k.factorial * ↑(n - k).factorial) = Pa * Qb * ↑a ^ k * ↑b ^ (n - k) * (↑(n.choose k) / ↑n.factorial)

theorem FelsConjectureProof.natDegree_one_sub_X_pow_le (k : ℕ) : (1 - Polynomial.X ^ k).natDegree ≤ k

theorem FelsConjectureProof.sum_coeff_one_sub_X_pow (k : ℕ) (_hk : 0 < k) : ∑ j ∈ Finset.range (k + 1), ↑((1 - Polynomial.X ^ k).coeff j) = 0

theorem FelsConjectureProof.exp_poly_sub_one_sub_X_pow_coeff_zero (k : ℕ) (hk : 0 < k) : (PowerSeries.coeff 0) (expPolySub (1 - Polynomial.X ^ k)) = 0

theorem FelsConjectureProof.natDegree_one_sub_X_pow_eq (k : ℕ) (hk : 0 < k) : (1 - Polynomial.X ^ k).natDegree = k

theorem FelsConjectureProof.one_sub_X_pow_term_eq_zero (k n j : ℕ) (_hk : 0 < k) (hn : 1 ≤ n) (_hj_mem : j ∈ Finset.range (k + 1)) (hj_ne : j ≠ k) : ↑((1 - Polynomial.X ^ k).coeff j) * ↑j ^ n = 0

theorem FelsConjectureProof.one_sub_X_pow_term_at_k (k n : ℕ) (hk : 0 < k) : ↑((1 - Polynomial.X ^ k).coeff k) * ↑k ^ n = -↑k ^ n

theorem FelsConjectureProof.one_sub_X_pow_sum_eq (k n : ℕ) (hk : 0 < k) (hn : 1 ≤ n) : ∑ j ∈ Finset.range ((1 - Polynomial.X ^ k).natDegree + 1), ↑((1 - Polynomial.X ^ k).coeff j) * ↑j ^ n = -↑k ^ n

theorem FelsConjectureProof.exp_poly_sub_one_sub_X_pow_coeff_pos (k n : ℕ) (hk : 0 < k) (hn : 1 ≤ n) : (PowerSeries.coeff n) (expPolySub (1 - Polynomial.X ^ k)) = -↑k ^ n / ↑n.factorial

theorem FelsConjectureProof.rhs_coeff_zero {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (i : Fin G.m) : (PowerSeries.coeff 0) (-↑(G.d i) • (PowerSeries.X * G.scaledExpFactor i)) = 0

theorem FelsConjectureProof.rhs_coeff_pos {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (i : Fin G.m) (n : ℕ) (hn : 1 ≤ n) : (PowerSeries.coeff n) (-↑(G.d i) • (PowerSeries.X * G.scaledExpFactor i)) = -↑(G.d i) ^ n / ↑n.factorial

theorem FelsConjectureProof.single_factor_exp_transform {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (i : Fin G.m) : expPolySub (1 - Polynomial.X ^ G.d i) = -↑(G.d i) • (PowerSeries.X * G.scaledExpFactor i)

theorem FelsConjectureProof.prod_smul_eq_smul_prod (m : ℕ) (c : Fin m → ℚ) (f : Fin m → PowerSeries ℚ) : ∏ i : Fin m, c i • f i = (∏ i : Fin m, c i) • ∏ i : Fin m, f i

theorem FelsConjectureProof.prod_X_mul_eq_X_pow_mul (m : ℕ) (f : Fin m → PowerSeries ℚ) : ∏ i : Fin m, PowerSeries.X * f i = PowerSeries.X ^ m * ∏ i : Fin m, f i

theorem FelsConjectureProof.prod_neg_eq_neg_one_pow_mul (m : ℕ) (c : Fin m → ℚ) : ∏ i : Fin m, -c i = (-1) ^ m * ∏ i : Fin m, c i

theorem FelsConjectureProof.prod_single_factor_eq_final_form {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : ∏ i : Fin G.m, -↑(G.d i) • (PowerSeries.X * G.scaledExpFactor i) = ((-1) ^ G.m * ↑G.piM) • (PowerSeries.X ^ G.m * G.ASeries)

theorem FelsConjectureProof.triple_sum_factorial_to_choose (P Q : Polynomial ℤ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑a ^ k * ↑b ^ (n - k) / (↑k.factorial * ↑(n - k).factorial) = ∑ k ∈ Finset.range (n + 1), ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑a ^ k * ↑b ^ (n - k) * (↑(n.choose k) / ↑n.factorial)

theorem FelsConjectureProof.factor_out_factorial (P Q : Polynomial ℤ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑a ^ k * ↑b ^ (n - k) * (↑(n.choose k) / ↑n.factorial) = 1 / ↑n.factorial * ∑ k ∈ Finset.range (n + 1), ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k)

theorem FelsConjectureProof.sum_rearrange (P Q : Polynomial ℤ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k) = ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ∑ k ∈ Finset.range (n + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k)

theorem FelsConjectureProof.factor_coeffs_from_inner_sum (P Q : Polynomial ℤ) (n : ℕ) : ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ∑ k ∈ Finset.range (n + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k) = ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k)

theorem FelsConjectureProof.binomial_sum_eq_power (a b n : ℕ) : ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k) = (↑a + ↑b) ^ n

theorem FelsConjectureProof.apply_binomial_to_inner_sum (P Q : Polynomial ℤ) (n : ℕ) : ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ↑a ^ k * ↑b ^ (n - k) = ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * (↑a + ↑b) ^ n

theorem FelsConjectureProof.exp_poly_sub_mul_coeff_eq (P Q : Polynomial ℤ) (n : ℕ) : (PowerSeries.coeff n) (expPolySub P * expPolySub Q) = (∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * (↑a + ↑b) ^ n) / ↑n.factorial

theorem FelsConjectureProof.convolution_sum_eq (P Q : Polynomial ℤ) (n : ℕ) : ∑ j ∈ Finset.range ((P * Q).natDegree + 1), ↑((P * Q).coeff j) * ↑j ^ n = ∑ j ∈ Finset.range (P.natDegree + Q.natDegree + 1), ∑ ab ∈ Finset.antidiagonal j, ↑(P.coeff ab.1) * ↑(Q.coeff ab.2) * (↑ab.1 + ↑ab.2) ^ n

theorem FelsConjectureProof.rectangle_subset_triangle (P Q : Polynomial ℤ) : Finset.range (P.natDegree + 1) ×ˢ Finset.range (Q.natDegree + 1) ⊆ (Finset.range (P.natDegree + Q.natDegree + 1)).biUnion Finset.antidiagonal

theorem FelsConjectureProof.term_vanishes_outside_rectangle (P Q : Polynomial ℤ) (n : ℕ) (ab : ℕ × ℕ) (_h_in_tri : ab ∈ (Finset.range (P.natDegree + Q.natDegree + 1)).biUnion Finset.antidiagonal) (h_not_rect : ab ∉ Finset.range (P.natDegree + 1) ×ˢ Finset.range (Q.natDegree + 1)) : ↑(P.coeff ab.1) * ↑(Q.coeff ab.2) * (↑ab.1 + ↑ab.2) ^ n = 0

theorem FelsConjectureProof.pairwiseDisjoint_antidiagonal (s : Finset ℕ) : (↑s).PairwiseDisjoint Finset.antidiagonal

theorem FelsConjectureProof.nested_sum_eq_biUnion_sum (P Q : Polynomial ℤ) (n : ℕ) : ∑ j ∈ Finset.range (P.natDegree + Q.natDegree + 1), ∑ ab ∈ Finset.antidiagonal j, ↑(P.coeff ab.1) * ↑(Q.coeff ab.2) * (↑ab.1 + ↑ab.2) ^ n = ∑ ab ∈ (Finset.range (P.natDegree + Q.natDegree + 1)).biUnion Finset.antidiagonal, ↑(P.coeff ab.1) * ↑(Q.coeff ab.2) * (↑ab.1 + ↑ab.2) ^ n

theorem FelsConjectureProof.product_sum_eq_nested (P Q : Polynomial ℤ) (n : ℕ) : ∑ ab ∈ Finset.range (P.natDegree + 1) ×ˢ Finset.range (Q.natDegree + 1), ↑(P.coeff ab.1) * ↑(Q.coeff ab.2) * (↑ab.1 + ↑ab.2) ^ n = ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * (↑a + ↑b) ^ n

theorem FelsConjectureProof.triangular_to_rectangular_sum (P Q : Polynomial ℤ) (n : ℕ) : ∑ j ∈ Finset.range (P.natDegree + Q.natDegree + 1), ∑ ab ∈ Finset.antidiagonal j, ↑(P.coeff ab.1) * ↑(Q.coeff ab.2) * (↑ab.1 + ↑ab.2) ^ n = ∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * (↑a + ↑b) ^ n

theorem FelsConjectureProof.exp_poly_sub_prod_coeff_eq (P Q : Polynomial ℤ) (n : ℕ) : (PowerSeries.coeff n) (expPolySub (P * Q)) = (∑ a ∈ Finset.range (P.natDegree + 1), ∑ b ∈ Finset.range (Q.natDegree + 1), ↑(P.coeff a) * ↑(Q.coeff b) * (↑a + ↑b) ^ n) / ↑n.factorial

theorem FelsConjectureProof.exp_poly_sub_mul (P Q : Polynomial ℤ) : expPolySub (P * Q) = expPolySub P * expPolySub Q

theorem FelsConjectureProof.exp_poly_sub_prod' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : expPolySub G.productPolynomial = ∏ i : Fin G.m, expPolySub (1 - Polynomial.X ^ G.d i)

theorem FelsConjectureProof.productPolynomial_exp_transform {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : expPolySub G.productPolynomial = ((-1) ^ G.m * ↑G.piM) • (PowerSeries.X ^ G.m * G.ASeries)

theorem FelsConjectureProof.coeff_one_sub_exp (n : ℕ) : (PowerSeries.coeff n) (1 - PowerSeries.exp ℚ) = if n = 0 then 0 else -1 / ↑n.factorial

theorem FelsConjectureProof.binomial_sum_minus_j_pow (j n : ℕ) : (∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else ↑(n.choose k) * ↑j ^ (n - k)) = (↑j + 1) ^ n - ↑j ^ n

theorem FelsConjectureProof.coeff_mul_as_range_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) ((1 - PowerSeries.exp ℚ) * partialSumGenFunc G) = ∑ k ∈ Finset.range (n + 1), (PowerSeries.coeff k) (1 - PowerSeries.exp ℚ) * (PowerSeries.coeff (n - k)) (partialSumGenFunc G)

theorem FelsConjectureProof.coeff_sum_substitute {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (PowerSeries.coeff k) (1 - PowerSeries.exp ℚ) * (PowerSeries.coeff (n - k)) (partialSumGenFunc G) = ∑ k ∈ Finset.range (n + 1), (if k = 0 then 0 else -1 / ↑k.factorial) * ((∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)) / ↑(n - k).factorial)

theorem FelsConjectureProof.drop_k_eq_zero_term {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (if k = 0 then 0 else -1 / ↑k.factorial) * ((∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)) / ↑(n - k).factorial) = ∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else -1 / ↑k.factorial * ((∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)) / ↑(n - k).factorial)

theorem FelsConjectureProof.summand_eq_for_pos {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n k : ℕ) (_hk_pos : k ≠ 0) (hk_le : k ≤ n) : -1 / ↑k.factorial * ((∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)) / ↑(n - k).factorial) = -↑(n.choose k) / ↑n.factorial * ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)

theorem FelsConjectureProof.apply_factorial_identity {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else -1 / ↑k.factorial * ((∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)) / ↑(n - k).factorial)) = ∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else -↑(n.choose k) / ↑n.factorial * ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)

theorem FelsConjectureProof.factor_neg_choose_div_factorial (D n : ℕ) (coeff : ℕ → ℚ) : (∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else -↑(n.choose k) / ↑n.factorial * ∑ j ∈ Finset.range (D + 1), coeff j * ↑j ^ (n - k)) = -1 / ↑n.factorial * ∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else ↑(n.choose k) * ∑ j ∈ Finset.range (D + 1), coeff j * ↑j ^ (n - k)

theorem FelsConjectureProof.swap_and_apply_binomial (D n : ℕ) (coeff : ℕ → ℚ) : (∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else ↑(n.choose k) * ∑ j ∈ Finset.range (D + 1), coeff j * ↑j ^ (n - k)) = ∑ j ∈ Finset.range (D + 1), coeff j * ((↑j + 1) ^ n - ↑j ^ n)

theorem FelsConjectureProof.factor_and_apply_binomial {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (∑ k ∈ Finset.range (n + 1), if k = 0 then 0 else -↑(n.choose k) / ↑n.factorial * ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ↑j ^ (n - k)) = -1 / ↑n.factorial * ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ m ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff m)) * ((↑j + 1) ^ n - ↑j ^ n)

theorem FelsConjectureProof.coeff_lhs_expand {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) ((1 - PowerSeries.exp ℚ) * partialSumGenFunc G) = -1 / ↑n.factorial * ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ((↑j + 1) ^ n - ↑j ^ n)

theorem FelsConjectureProof.coeff_lhs_eq_rhs {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) ((1 - PowerSeries.exp ℚ) * partialSumGenFunc G) = (PowerSeries.coeff n) (expPolySub G.productPolynomial)

theorem FelsConjectureProof.partialSumGenFunc_mul_one_sub_exp {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : (1 - PowerSeries.exp ℚ) * partialSumGenFunc G = expPolySub G.productPolynomial

theorem FelsConjectureProof.partialSumGenFunc_identity {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : PowerSeries.X * partialSumGenFunc G = ((-1) ^ (G.m + 1) * ↑G.piM) • (PowerSeries.X ^ G.m * G.BSeries)

theorem FelsConjectureProof.cond_equiv (m n : ℕ) : m ≤ n + 1 ↔ m - 1 ≤ n

theorem FelsConjectureProof.index_eq (m n : ℕ) (hm : 0 < m) (h : m ≤ n + 1) : n + 1 - m = n - (m - 1)

theorem FelsConjectureProof.coeff_X_pow_shift {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff (n + 1)) (PowerSeries.X ^ G.m * G.BSeries) = (PowerSeries.coeff n) (PowerSeries.X ^ (G.m - 1) * G.BSeries)

theorem FelsConjectureProof.partialSumGenFunc_coeff_eq_bernoulli_term {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (PowerSeries.coeff n) (partialSumGenFunc G) = (-1) ^ (G.m + 1) * ↑G.piM * (PowerSeries.coeff n) (PowerSeries.X ^ (G.m - 1) * G.BSeries)

theorem FelsConjectureProof.sum_part_equals_bernoulli_term_natDegree {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ k ∈ Finset.range (j + 1), ↑(G.productPolynomial.coeff k)) * ↑j ^ n) / ↑n.factorial = (-1) ^ (G.m + 1) * ↑G.piM * (PowerSeries.coeff n) (PowerSeries.X ^ (G.m - 1) * G.BSeries)

theorem FelsConjectureProof.gap_le_sup {S : NumericalSemigroup} (g : ℕ) (hg : g ∈ S.gaps) : g ≤ S.gaps.sup id

theorem FelsConjectureProof.neg_neg_one_pow_eq (m : ℕ) : -(-1) ^ m = (-1) ^ (m + 1)

theorem FelsConjectureProof.gap_sum_at_jstar {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hnonempty : S.gaps.Nonempty) : ∑ g ∈ S.gaps with g ≤ G.productPolynomial.natDegree + S.gaps.sup id, G.productPolynomial.coeff (G.productPolynomial.natDegree + S.gaps.sup id - g) = (-1) ^ G.m

theorem FelsConjectureProof.hilbertNumerator_coeff_at_jstar {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hnonempty : S.gaps.Nonempty) : G.hilbertNumerator.coeff (G.productPolynomial.natDegree + S.gaps.sup id) = (-1) ^ (G.m + 1)

theorem FelsConjectureProof.neg_one_pow_ne_zero' (m : ℕ) : (-1) ^ (m + 1) ≠ 0

theorem FelsConjectureProof.hilbertNumerator_natDegree_ge_jstar {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (hnonempty : S.gaps.Nonempty) : G.productPolynomial.natDegree + S.gaps.sup id ≤ G.hilbertNumerator.natDegree

theorem FelsConjectureProof.hilbertNumerator_natDegree_ge_prod_plus_gap {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g : ℕ) (hg : g ∈ S.gaps) : G.productPolynomial.natDegree + g ≤ G.hilbertNumerator.natDegree

theorem FelsConjectureProof.forward_map_mem {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g j : ℕ) (hj : j ∈ {x ∈ Finset.range (G.hilbertNumerator.natDegree + 1) | g ≤ x}) : j - g ∈ Finset.range (G.hilbertNumerator.natDegree + 1 - g)

theorem FelsConjectureProof.inverse_map_mem {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g k : ℕ) (hk : k ∈ Finset.range (G.hilbertNumerator.natDegree + 1 - g)) : k + g ∈ {x ∈ Finset.range (G.hilbertNumerator.natDegree + 1) | g ≤ x}

theorem FelsConjectureProof.forward_inverse_id' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g j : ℕ) (hj : j ∈ {x ∈ Finset.range (G.hilbertNumerator.natDegree + 1) | g ≤ x}) : j - g + g = j

theorem FelsConjectureProof.inverse_forward_id' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g k : ℕ) (_hk : k ∈ Finset.range (G.hilbertNumerator.natDegree + 1 - g)) : k + g - g = k

theorem FelsConjectureProof.summand_eq' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n g j : ℕ) (hj : j ∈ {x ∈ Finset.range (G.hilbertNumerator.natDegree + 1) | g ≤ x}) : ↑(G.productPolynomial.coeff (j - g)) * ↑j ^ n = ↑(G.productPolynomial.coeff (j - g)) * (↑(j - g) + ↑g) ^ n

theorem FelsConjectureProof.inner_sum_reindex {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n g : ℕ) (_hg : g ∈ S.gaps) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1) with g ≤ j, ↑(G.productPolynomial.coeff (j - g)) * ↑j ^ n = ∑ k ∈ Finset.range (G.hilbertNumerator.natDegree + 1 - g), ↑(G.productPolynomial.coeff k) * (↑k + ↑g) ^ n

theorem FelsConjectureProof.range_subset_from_degree_bound' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g : ℕ) (hg : g ∈ S.gaps) : Finset.range (G.productPolynomial.natDegree + 1) ⊆ Finset.range (G.hilbertNumerator.natDegree + 1 - g)

theorem FelsConjectureProof.summand_zero_beyond_degree' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (g n k : ℕ) (_hk : k ∈ Finset.range (G.hilbertNumerator.natDegree + 1 - g)) (hk_not : k ∉ Finset.range (G.productPolynomial.natDegree + 1)) : ↑(G.productPolynomial.coeff k) * (↑k + ↑g) ^ n = 0

theorem FelsConjectureProof.inner_sum_extend_range' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n g : ℕ) (hg : g ∈ S.gaps) : ∑ k ∈ Finset.range (G.hilbertNumerator.natDegree + 1 - g), ↑(G.productPolynomial.coeff k) * (↑k + ↑g) ^ n = ∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff k) * (↑k + ↑g) ^ n

theorem FelsConjectureProof.distribute_j_pow_into_sum {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n j : ℕ) : (∑ g ∈ S.gaps with g ≤ j, ↑(G.productPolynomial.coeff (j - g))) * ↑j ^ n = ∑ g ∈ S.gaps with g ≤ j, ↑(G.productPolynomial.coeff (j - g)) * ↑j ^ n

theorem FelsConjectureProof.sum_exchange_condition' {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (j g : ℕ) : j ∈ Finset.range (G.hilbertNumerator.natDegree + 1) ∧ g ∈ {x ∈ S.gaps | x ≤ j} ↔ j ∈ {x ∈ Finset.range (G.hilbertNumerator.natDegree + 1) | g ≤ x} ∧ g ∈ S.gaps

theorem FelsConjectureProof.distribute_and_swap_sums {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ g ∈ S.gaps with g ≤ j, ↑(G.productPolynomial.coeff (j - g))) * ↑j ^ n = ∑ g ∈ S.gaps, ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1) with g ≤ j, ↑(G.productPolynomial.coeff (j - g)) * ↑j ^ n

theorem FelsConjectureProof.gap_sum_exchange {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ g ∈ S.gaps with g ≤ j, ↑(G.productPolynomial.coeff (j - g))) * ↑j ^ n = ∑ g ∈ S.gaps, ∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff k) * (↑k + ↑g) ^ n

theorem FelsConjectureProof.binomial_sum_eq_add_pow (a b : ℚ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * a ^ k * b ^ (n - k) = (a + b) ^ n

theorem FelsConjectureProof.triple_sum_exchange (gaps : Finset ℕ) (degP : ℕ) (coeff : ℕ → ℚ) (n : ℕ) : ∑ g ∈ gaps, ∑ k ∈ Finset.range (degP + 1), ∑ r ∈ Finset.range (n + 1), coeff k * ↑(n.choose r) * ↑k ^ r * ↑g ^ (n - r) = ∑ r ∈ Finset.range (n + 1), ∑ g ∈ gaps, ∑ k ∈ Finset.range (degP + 1), coeff k * ↑(n.choose r) * ↑k ^ r * ↑g ^ (n - r)

theorem FelsConjectureProof.factor_binomial_coeff_from_double_sum (gaps : Finset ℕ) (degP : ℕ) (coeff : ℕ → ℚ) (n r : ℕ) : ∑ g ∈ gaps, ∑ k ∈ Finset.range (degP + 1), coeff k * ↑(n.choose r) * ↑k ^ r * ↑g ^ (n - r) = (↑(n.choose r) * ∑ k ∈ Finset.range (degP + 1), coeff k * ↑k ^ r) * ∑ g ∈ gaps, ↑g ^ (n - r)

theorem FelsConjectureProof.sum_choose_mul_div_factorial_eq_sum_div_factorials (n : ℕ) (A B : ℕ → ℚ) : ∑ r ∈ Finset.range (n + 1), ↑(n.choose r) * A r * B r / ↑n.factorial = ∑ r ∈ Finset.range (n + 1), A r / ↑r.factorial * (B r / ↑(n - r).factorial)

theorem FelsConjectureProof.gap_sum_binomial_expand {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (∑ g ∈ S.gaps, ∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff k) * (↑k + ↑g) ^ n) / ↑n.factorial = ∑ r ∈ Finset.range (n + 1), (∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff k) * ↑k ^ r) / ↑r.factorial * ((∑ g ∈ S.gaps, ↑g ^ (n - r)) / ↑(n - r).factorial)

theorem FelsConjectureProof.P_sum_to_exp_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (r : ℕ) : (∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff k) * ↑k ^ r) / ↑r.factorial = (-1) ^ G.m * ↑G.piM * (PowerSeries.coeff r) (PowerSeries.X ^ G.m * G.ASeries)

theorem FelsConjectureProof.gap_sum_to_coeff {S : NumericalSemigroup} (k : ℕ) : (∑ g ∈ S.gaps, ↑g ^ k) / ↑k.factorial = (PowerSeries.coeff k) (PowerSeries.mk fun (j : ℕ) => ∑ g ∈ S.gaps, ↑g ^ j / ↑j.factorial)

theorem FelsConjectureProof.coeff_mul_range' {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) (n : ℕ) : (PowerSeries.coeff n) (φ * ψ) = ∑ r ∈ Finset.range (n + 1), (PowerSeries.coeff r) φ * (PowerSeries.coeff (n - r)) ψ

theorem FelsConjectureProof.sum_factor_scalar' {α : Type u_1} (s : Finset α) (c : ℚ) (a b : α → ℚ) : ∑ r ∈ s, c * a r * b r = c * ∑ r ∈ s, a r * b r

theorem FelsConjectureProof.binomial_sum_to_convolution {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : ∑ r ∈ Finset.range (n + 1), (∑ k ∈ Finset.range (G.productPolynomial.natDegree + 1), ↑(G.productPolynomial.coeff k) * ↑k ^ r) / ↑r.factorial * ((∑ g ∈ S.gaps, ↑g ^ (n - r)) / ↑(n - r).factorial) = (-1) ^ G.m * ↑G.piM * (PowerSeries.coeff n) (PowerSeries.X ^ G.m * G.ASeries * PowerSeries.mk fun (k : ℕ) => ∑ g ∈ S.gaps, ↑g ^ k / ↑k.factorial)

theorem FelsConjectureProof.gap_part_equals_gap_term_natDegree {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) : (∑ j ∈ Finset.range (G.hilbertNumerator.natDegree + 1), (∑ g ∈ S.gaps with g ≤ j, ↑(G.productPolynomial.coeff (j - g))) * ↑j ^ n) / ↑n.factorial = (-1) ^ (G.m + 1) * ↑G.piM * -(PowerSeries.coeff n) (PowerSeries.X ^ G.m * G.ASeries * PowerSeries.mk fun (k : ℕ) => ∑ g ∈ S.gaps, ↑g ^ k / ↑k.factorial)

theorem FelsConjectureProof.exp_poly_sub_hilbertNumerator_eq {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : expPolySub G.hilbertNumerator = QExpSeries G

theorem FelsConjectureProof.hilbertNumerator_exp_eq_Q_exp {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) : hilbertNumeratorExpSub G = QExpSeries G

theorem FelsConjectureProof.alternatingPowerSum_eq_neg_factorial_coeff {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (n : ℕ) (hn : 1 ≤ n) : G.alternatingPowerSum n = -(↑n.factorial * (PowerSeries.coeff n) (QExpSeries G))

theorem FelsConjectureProof.C_m_plus_p_formula {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : G.alternatingPowerSum (G.m + p) = (-1) ^ G.m * ↑G.piM * ↑(G.m + p).factorial * (PowerSeries.coeff (p + 1)) G.BSeries + (-1) ^ G.m * ↑G.piM * ∑ r ∈ Finset.range (p + 1), ↑((G.m + p).choose r) * ↑(G.m + p - r).factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r

theorem FelsConjectureProof.K_invariant_expanded {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : G.KInvariant p = ↑p.factorial * (PowerSeries.coeff (p + 1)) G.BSeries + ∑ r ∈ Finset.range (p + 1), ↑p.factorial / ↑r.factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r

theorem FelsConjectureProof.bernoulli_coeff_to_T_delta {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ↑p.factorial * (PowerSeries.coeff (p + 1)) G.BSeries = 2 ^ (p + 1) / (↑p + 1) * G.TDelta (p + 1)

theorem FelsConjectureProof.factorial_div_eq_choose_mul {p r : ℕ} (hr : r ≤ p) : ↑p.factorial / ↑r.factorial = ↑(p.choose r) * ↑(p - r).factorial

theorem FelsConjectureProof.A_coeff_to_T_sigma {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p r : ℕ) (hr : r ≤ p) : ↑p.factorial / ↑r.factorial * (PowerSeries.coeff (p - r)) G.ASeries = ↑(p.choose r) * G.TSigma (p - r)

theorem FelsConjectureProof.sum_A_coeff_eq_sum_T_sigma {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : ∑ r ∈ Finset.range (p + 1), ↑p.factorial / ↑r.factorial * (PowerSeries.coeff (p - r)) G.ASeries * S.gapPowerSum r = ∑ r ∈ Finset.range (p + 1), ↑(p.choose r) * G.TSigma (p - r) * S.gapPowerSum r

theorem FelsConjectureProof.fels_conjecture_main {S : NumericalSemigroup} (G : NumericalSemigroupGenerators S) (p : ℕ) : G.KInvariant p = ∑ r ∈ Finset.range (p + 1), ↑(p.choose r) * G.TSigma (p - r) * S.gapPowerSum r + 2 ^ (p + 1) / (↑p + 1) * G.TDelta (p + 1)

theorem fels_conjecture (S : NumericalSemigroup) (G : NumericalSemigroupGenerators S) (p : ℕ) : G.KInvariant p = ∑ r ∈ Finset.range (p + 1), ↑(p.choose r) * G.TSigma (p - r) * S.gapPowerSum r + 2 ^ (p + 1) / (↑p + 1) * G.TDelta (p + 1)