Positivity of generating-function coefficients (Theorem 1)

This file formalizes Theorem 1 of the Chebyshev-quotient / Demazure-multiplicity paper: the coefficients of the generating function attached to a partition are eventually positive, built from a Chebyshev-type polynomial recurrence and a Dyck-path model.

Core Definitions

noncomputable def Biswal.Theorem1.polyP (R : Type u_1) [CommRing R] : ℕ → Polynomial R

The Chebyshev-type polynomial sequence P n over a commutative ring, defined by P 0 = P 1 = 1 and P (n + 2) = P (n + 1) - X * P n.

Equations

• Biswal.Theorem1.polyP R 0 = 1
• Biswal.Theorem1.polyP R 1 = 1
• Biswal.Theorem1.polyP R n.succ.succ = Biswal.Theorem1.polyP R (n + 1) - Polynomial.X * Biswal.Theorem1.polyP R n

theorem Biswal.Theorem1.polyP_zero (R : Type u_1) [CommRing R] : polyP R 0 = 1

theorem Biswal.Theorem1.polyP_one (R : Type u_1) [CommRing R] : polyP R 1 = 1

theorem Biswal.Theorem1.polyP_succ_succ (R : Type u_1) [CommRing R] (n : ℕ) : polyP R (n + 2) = polyP R (n + 1) - Polynomial.X * polyP R n

noncomputable def Biswal.Theorem1.partitionPoly (R : Type u_1) [CommRing R] {s : ℕ} (ξ : s.Partition) : Polynomial R

The partition polynomial of ξ: the product of polyP R over the parts of ξ.

Equations

• Biswal.Theorem1.partitionPoly R ξ = (Multiset.map (Biswal.Theorem1.polyP R) ξ.parts).prod

def Biswal.Theorem1.countMaxParts (m : ℕ) {s : ℕ} (ξ : s.Partition) : ℕ

The number of parts of ξ equal to m.

Equations

• Biswal.Theorem1.countMaxParts m ξ = Multiset.count m ξ.parts

noncomputable def Biswal.Theorem1.genFun (K : Type u_1) [Field K] (m n : ℕ) {s : ℕ} (ξ : s.Partition) : PowerSeries K

The generating function attached to ξ with parameters m and n, as a power series.

Equations

• Biswal.Theorem1.genFun K m n ξ = ↑(Biswal.Theorem1.polyP K (m - n % m - 1) * Biswal.Theorem1.partitionPoly K ξ) * (↑(Biswal.Theorem1.polyP K m) ^ (n / m + 1))⁻¹

noncomputable def Biswal.Theorem1.genFunCoeff (K : Type u_1) [Field K] (m n r : ℕ) {s : ℕ} (ξ : s.Partition) : K

The r-th coefficient of the generating function genFun K m n ξ.

Equations

• Biswal.Theorem1.genFunCoeff K m n r ξ = (PowerSeries.coeff r) (Biswal.Theorem1.genFun K m n ξ)

Basic Properties of polyP

theorem Biswal.Theorem1.polyP_constantCoeff (R : Type u_1) [CommRing R] (n : ℕ) : (polyP R n).coeff 0 = 1

theorem Biswal.Theorem1.polyP_coe_constantCoeff_ne_zero (K : Type u_1) [Field K] (m : ℕ) : PowerSeries.constantCoeff ↑(polyP K m) ≠ 0

theorem Biswal.Theorem1.polyP_coe_pow_constantCoeff_ne_zero (K : Type u_1) [Field K] (m k : ℕ) : PowerSeries.constantCoeff (↑(polyP K m) ^ k) ≠ 0

theorem Biswal.Theorem1.partitionPoly_eq_one_of_parts_le_one (K : Type u_1) [Field K] {s : ℕ} (ξ : s.Partition) (h : ∀ i ∈ ξ.parts, i ≤ 1) : partitionPoly K ξ = 1

theorem Biswal.Theorem1.partitionPoly_split (K : Type u_1) [CommRing K] (m : ℕ) {s : ℕ} (ξ : s.Partition) : ∃ (Q : Polynomial K), partitionPoly K ξ = polyP K m ^ countMaxParts m ξ * Q

theorem Biswal.Theorem1.genFun_is_poly_coe (K : Type u_1) [Field K] (m n : ℕ) {s : ℕ} (ξ : s.Partition) (_hm : 2 ≤ m) (_h_parts : ∀ i ∈ ξ.parts, i ≤ m) (h_t : n / m + 1 ≤ countMaxParts m ξ) : ∃ (P : Polynomial K), genFun K m n ξ = ↑P

theorem Biswal.Theorem1.poly_coe_eventually_zero (K : Type u_1) [Field K] (P : Polynomial K) (r : ℕ) : P.natDegree < r → (PowerSeries.coeff r) ↑P = 0

noncomputable def Biswal.Theorem1.nonMaxPartsPoly (K : Type u_1) [CommRing K] (m : ℕ) {s : ℕ} (ξ : s.Partition) : Polynomial K

The product of polyP K over the parts of ξ that are not equal to m.

Equations

• Biswal.Theorem1.nonMaxPartsPoly K m ξ = (Multiset.map (Biswal.Theorem1.polyP K) (Multiset.filter (fun (x : ℕ) => x ≠ m) ξ.parts)).prod

theorem Biswal.Theorem1.polyP_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) : Polynomial.map f (polyP R n) = polyP S n

theorem Biswal.Theorem1.genFun_as_rational_fraction_with_pos_numerator (m n : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (h_t : countMaxParts m ξ ≤ n / m) : ∃ (A : Polynomial ℚ) (k : ℕ), 0 < k ∧ genFun ℚ m n ξ = ↑A * (↑(polyP ℚ m) ^ k)⁻¹ ∧ ∀ (ρ : ℝ), 0 < ρ → Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) (polyP ℚ m)) = 0 → (∀ j < m, 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) (polyP ℚ j))) → 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) A)

theorem Biswal.Theorem1.coeff_rational_fraction_eq_proper_part (A D : Polynomial ℚ) (_hD : PowerSeries.constantCoeff ↑D ≠ 0) : ∃ (S : Polynomial ℚ) (R : Polynomial ℚ) (N : ℕ), ↑A * (↑D)⁻¹ = ↑S + ↑R * (↑D)⁻¹ ∧ ∀ (r : ℕ), N < r → (PowerSeries.coeff r) (↑A * (↑D)⁻¹) = (PowerSeries.coeff r) (↑R * (↑D)⁻¹)

Trigonometric and Chebyshev Lemmas

Root Analysis

theorem Biswal.Theorem1.polyP_roots_positive (m : ℕ) (hm : 2 ≤ m) : ∃ (ρ : ℝ), 0 < ρ ∧ Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) (polyP ℚ m)) = 0 ∧ ∀ j < m, 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) (polyP ℚ j))

theorem Biswal.Theorem1.remainder_positive_at_roots (A D S R : Polynomial ℚ) (hdiv : ↑A * (↑D)⁻¹ = ↑S + ↑R * (↑D)⁻¹) (hD_ne : PowerSeries.constantCoeff ↑D ≠ 0) (ρ : ℝ) (hρ : Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) D) = 0) (hA : 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) A)) : 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) R)

theorem Biswal.Theorem1.pos_coeff_transfer_R_to_Q (f : PowerSeries ℚ) (N : ℕ) (h : ∀ (r : ℕ), N < r → 0 < (PowerSeries.coeff r) ((PowerSeries.map (algebraMap ℚ ℝ)) f)) (r : ℕ) : N < r → 0 < (PowerSeries.coeff r) f

theorem Biswal.Theorem1.map_algebraMap_inv_comm (f : PowerSeries ℚ) (hf : PowerSeries.constantCoeff f ≠ 0) : (PowerSeries.map (algebraMap ℚ ℝ)) f⁻¹ = ((PowerSeries.map (algebraMap ℚ ℝ)) f)⁻¹

theorem Biswal.Theorem1.polyP_ne_zero (m : ℕ) : polyP ℝ m ≠ 0

theorem Biswal.Theorem1.polyP_natDegree_le (n : ℕ) : (polyP ℝ n).natDegree ≤ n / 2

theorem Biswal.Theorem1.polyP_chebyshev_rescale (n : ℕ) (z : ℝ) (hz : z ≠ 0) : (2 * z) ^ n * Polynomial.eval (1 / (4 * z ^ 2)) (polyP ℝ n) = Polynomial.eval z (Polynomial.Chebyshev.U ℝ ↑n)

theorem Biswal.Theorem1.angle_lt_pi_div_two (m k : ℕ) (_hm : 2 ≤ m) (hk_bound : 2 * k < m + 1) : ↑k * Real.pi / (↑m + 1) < Real.pi / 2

theorem Biswal.Theorem1.cos_angle_pos (m : ℕ) (hm : 2 ≤ m) (j : Fin (m / 2)) : 0 < Real.cos ((↑↑j + 1) * Real.pi / (↑m + 1))

theorem Biswal.Theorem1.angle_pos (m : ℕ) (_hm : 2 ≤ m) (j : Fin (m / 2)) : 0 < (↑↑j + 1) * Real.pi / (↑m + 1)

theorem Biswal.Theorem1.angle_lt_pi (m : ℕ) (hm : 2 ≤ m) (j : Fin (m / 2)) : (↑↑j + 1) * Real.pi / (↑m + 1) < Real.pi

theorem Biswal.Theorem1.candidate_is_root (m : ℕ) (hm : 2 ≤ m) (j : Fin (m / 2)) : (polyP ℝ m).IsRoot (1 / (4 * Real.cos ((↑↑j + 1) * Real.pi / (↑m + 1)) ^ 2))

theorem Biswal.Theorem1.angle_strict_mono (m k_ρ k_x : ℕ) (_hm : 2 ≤ m) (hk_lt : k_ρ < k_x) : ↑k_ρ * Real.pi / (↑m + 1) < ↑k_x * Real.pi / (↑m + 1)

theorem Biswal.Theorem1.candidate_strictMono (m : ℕ) (hm : 2 ≤ m) : StrictMono fun (j : Fin (m / 2)) => 1 / (4 * Real.cos ((↑↑j + 1) * Real.pi / (↑m + 1)) ^ 2)

Coprimality and Splitting

theorem Biswal.Theorem1.bezout_core (ρ : ℝ) (hρ_pos : 0 < ρ) (s : ℝ) (hs_pos : 0 < s) (Q : Polynomial ℝ) : Polynomial.C (1 / s) * ((Polynomial.X - Polynomial.C ρ) * Q + Polynomial.C s) + Polynomial.C (ρ / s) * Q * (-Polynomial.C (1 / ρ) * (Polynomial.X - Polynomial.C ρ)) = 1

theorem Biswal.Theorem1.isCoprime_of_eval_pos (ρ : ℝ) (hρ_pos : 0 < ρ) (S : Polynomial ℝ) (hS_pos : 0 < Polynomial.eval ρ S) : IsCoprime S (Polynomial.X - Polynomial.C ρ)

theorem Biswal.Theorem1.prod_linear_factors_dvd {p : Polynomial ℝ} {d : ℕ} (_hp : p ≠ 0) (r : Fin d → ℝ) (hr_pos : ∀ (j : Fin d), 0 < r j) (hr_mono : StrictMono r) (hr_root : ∀ (j : Fin d), p.IsRoot (r j)) (h_dvd : ∀ (j : Fin d), Polynomial.X - Polynomial.C (r j) ∣ p) : ∏ j : Fin d, (Polynomial.X - Polynomial.C (r j)) ∣ p

theorem Biswal.Theorem1.splits_of_distinct_pos_roots_and_deg_le {p : Polynomial ℝ} {d : ℕ} (hp : p ≠ 0) (hdeg : p.natDegree ≤ d) (r : Fin d → ℝ) (hr_pos : ∀ (j : Fin d), 0 < r j) (hr_mono : StrictMono r) (hr_root : ∀ (j : Fin d), p.IsRoot (r j)) : p.Splits

theorem Biswal.Theorem1.polyP_root_to_chebyshev_root (m : ℕ) (r : ℝ) (hr_pos : 0 < r) (hr_root : Polynomial.eval r (polyP ℝ m) = 0) : have z := 1 / (2 * √r); 0 < z ∧ Polynomial.eval z (Polynomial.Chebyshev.U ℝ ↑m) = 0

theorem Biswal.Theorem1.cos_pos_angle_bound (m : ℕ) (hm : 2 ≤ m) (j : ℕ) (hj : j < m) (hcos_pos : 0 < Real.cos ((↑j + 1) * Real.pi / (↑m + 1))) : 2 * (j + 1) < m + 1

theorem Biswal.Theorem1.chebyshev_root_parametrize (m : ℕ) (hm : 2 ≤ m) (z : ℝ) (hz_pos : 0 < z) (hz_root : Polynomial.eval z (Polynomial.Chebyshev.U ℝ ↑m) = 0) : ∃ (k : ℕ), 1 ≤ k ∧ 2 * k < m + 1 ∧ z = Real.cos (↑k * Real.pi / (↑m + 1))

theorem Biswal.Theorem1.polyP_root_parametrize (m : ℕ) (hm : 2 ≤ m) (r : ℝ) (hr_pos : 0 < r) (hr_root : Polynomial.eval r (polyP ℝ m) = 0) : ∃ (k : ℕ), 1 ≤ k ∧ 2 * k < m + 1 ∧ 1 / (2 * √r) = Real.cos (↑k * Real.pi / (↑m + 1))

theorem Biswal.Theorem1.candidate_lt_m (m k : ℕ) (_hm : 2 ≤ m) (hk : 2 ≤ k) (hk_bound : 2 * k < m + 1) : (m + 1) / k < m

theorem Biswal.Theorem1.nat_ineq_div_mul (m k : ℕ) (hk : 2 ≤ k) : m + 1 < ((m + 1) / k + 1) * k

theorem Biswal.Theorem1.angle_gt_pi (m k : ℕ) (hm : 2 ≤ m) (hk : 2 ≤ k) (_hk_bound : 2 * k < m + 1) : Real.pi < (↑((m + 1) / k) + 1) * (↑k * Real.pi / (↑m + 1))

theorem Biswal.Theorem1.angle_lt_two_pi (m k : ℕ) (hm : 2 ≤ m) (hk : 2 ≤ k) (hk_bound : 2 * k < m + 1) : (↑((m + 1) / k) + 1) * (↑k * Real.pi / (↑m + 1)) < 2 * Real.pi

theorem Biswal.Theorem1.sin_nonpos_of_pi_lt_lt_two_pi (θ : ℝ) (h1 : Real.pi < θ) (h2 : θ < 2 * Real.pi) : Real.sin θ ≤ 0

theorem Biswal.Theorem1.polyP_eval_nonpos_at_bad_index (m k j₀ : ℕ) (hm : 2 ≤ m) (hk : 2 ≤ k) (hk_bound : 2 * k < m + 1) (_hj₀ : j₀ < m) (r : ℝ) (hr_pos : 0 < r) (hr_param : 1 / (2 * √r) = Real.cos (↑k * Real.pi / (↑m + 1))) (h_sin : Real.sin ((↑j₀ + 1) * (↑k * Real.pi / (↑m + 1))) ≤ 0) : Polynomial.eval r (polyP ℝ j₀) ≤ 0

theorem Biswal.Theorem1.polyP_roots_pos (m : ℕ) (_hm : 2 ≤ m) (x : ℝ) (hx : Polynomial.eval x (polyP ℝ m) = 0) : 0 < x

theorem Biswal.Theorem1.root_index_eq_one (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) (k : ℕ) (hk_pos : 1 ≤ k) (hk_bound : 2 * k < m + 1) (hρ_param : 1 / (2 * √ρ) = Real.cos (↑k * Real.pi / (↑m + 1))) : k = 1

theorem Biswal.Theorem1.sqrt_from_param (ρ c : ℝ) (_hρ : 0 < ρ) (hc : 0 < c) (h : 1 / (2 * √ρ) = c) : √ρ = 1 / (2 * c)

theorem Biswal.Theorem1.cos_pos_from_param (ρ c : ℝ) (hρ : 0 < ρ) (h : 1 / (2 * √ρ) = c) : 0 < c

theorem Biswal.Theorem1.root_comparison (m : ℕ) (hm : 2 ≤ m) (ρ x : ℝ) (hρ_pos : 0 < ρ) (hx_pos : 0 < x) (k_ρ k_x : ℕ) (hk_ρ_pos : 1 ≤ k_ρ) (_hk_ρ_bound : 2 * k_ρ < m + 1) (_hk_x_pos : 1 ≤ k_x) (hk_x_bound : 2 * k_x < m + 1) (hρ_param : 1 / (2 * √ρ) = Real.cos (↑k_ρ * Real.pi / (↑m + 1))) (hx_param : 1 / (2 * √x) = Real.cos (↑k_x * Real.pi / (↑m + 1))) (hk_lt : k_ρ < k_x) : ρ < x

theorem Biswal.Theorem1.root_is_smallest (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_root : Polynomial.eval ρ (polyP ℝ m) = 0) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) (x : ℝ) (hx_root : Polynomial.eval x (polyP ℝ m) = 0) (hx_ne : x ≠ ρ) : ρ < x

theorem Biswal.Theorem1.L_eval_at_rho (ρ : ℝ) (hρ : 0 < ρ) : Polynomial.eval ρ (1 - Polynomial.C (1 / ρ) * Polynomial.X) = 0

theorem Biswal.Theorem1.eval_deriv_eq_neg_inv_rho_mul_eval_S (m : ℕ) (ρ : ℝ) (hρ_pos : 0 < ρ) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) : Polynomial.eval ρ (Polynomial.derivative (polyP ℝ m)) = -(1 / ρ) * Polynomial.eval ρ S

Derivative Convolution Identity

theorem Biswal.Theorem1.polyP_neg_deriv_base_two (R : Type u_1) [CommRing R] : -Polynomial.derivative (polyP R 2) = ∑ j ∈ Finset.range 1, polyP R j * polyP R (0 - j)

theorem Biswal.Theorem1.polyP_neg_deriv_base_three (R : Type u_1) [CommRing R] : -Polynomial.derivative (polyP R 3) = ∑ j ∈ Finset.range 2, polyP R j * polyP R (1 - j)

theorem Biswal.Theorem1.polyP_deriv_recurrence (R : Type u_1) [CommRing R] (n : ℕ) : Polynomial.derivative (polyP R (n + 2)) = Polynomial.derivative (polyP R (n + 1)) - polyP R n - Polynomial.X * Polynomial.derivative (polyP R n)

theorem Biswal.Theorem1.inner_sum_recurrence (R : Type u_1) [CommRing R] (n : ℕ) : ∑ j ∈ Finset.range (n + 1), polyP R j * polyP R (n + 2 - j) = ∑ j ∈ Finset.range (n + 1), polyP R j * polyP R (n + 1 - j) - Polynomial.X * ∑ j ∈ Finset.range (n + 1), polyP R j * polyP R (n - j)

theorem Biswal.Theorem1.convolution_sum_step (R : Type u_1) [CommRing R] (n : ℕ) : ∑ j ∈ Finset.range (n + 3), polyP R j * polyP R (n + 2 - j) = ∑ j ∈ Finset.range (n + 2), polyP R j * polyP R (n + 1 - j) + polyP R (n + 2) - Polynomial.X * ∑ j ∈ Finset.range (n + 1), polyP R j * polyP R (n - j)

theorem Biswal.Theorem1.polyP_neg_deriv_eq_convolution (R : Type u_1) [CommRing R] (n : ℕ) (hn : 2 ≤ n) : -Polynomial.derivative (polyP R n) = ∑ j ∈ Finset.range (n - 1), polyP R j * polyP R (n - 2 - j)

theorem Biswal.Theorem1.eval_deriv_polyP_neg (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (_hρ_pos : 0 < ρ) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) : Polynomial.eval ρ (Polynomial.derivative (polyP ℝ m)) < 0

theorem Biswal.Theorem1.rho_not_root_of_S (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (hρ_pos : 0 < ρ) (_hρ_root : Polynomial.eval ρ (polyP ℝ m) = 0) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) : Polynomial.eval ρ S ≠ 0

theorem Biswal.Theorem1.S_constantCoeff_from_fact (m : ℕ) (ρ : ℝ) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) : S.coeff 0 = 1

theorem Biswal.Theorem1.S_splits (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) : S.Splits

theorem Biswal.Theorem1.eval_pos_from_splits_and_roots_gt (S : Polynomial ℝ) (ρ : ℝ) (hρ_pos : 0 < ρ) (_hS_ne : S ≠ 0) (_hS_splits : S.Splits) (hS_eval_zero : Polynomial.eval 0 S = 1) (hS_roots_gt : ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ < x) : 0 < Polynomial.eval ρ S

theorem Biswal.Theorem1.roots_of_S_gt_rho_v2 (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_root : Polynomial.eval ρ (polyP ℝ m) = 0) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) (x : ℝ) (hx : Polynomial.eval x S = 0) : ρ < x

theorem Biswal.Theorem1.S_eval_pos (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_root : Polynomial.eval ρ (polyP ℝ m) = 0) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) : 0 < Polynomial.eval ρ S

theorem Biswal.Theorem1.L_constantCoeff (ρ : ℝ) : (1 - Polynomial.C (1 / ρ) * Polynomial.X).coeff 0 = 1

theorem Biswal.Theorem1.L_eq_neg_C_mul (ρ : ℝ) (hρ : 0 < ρ) : 1 - Polynomial.C (1 / ρ) * Polynomial.X = -Polynomial.C (1 / ρ) * (Polynomial.X - Polynomial.C ρ)

Factorization and Power Series Decomposition

theorem Biswal.Theorem1.polyP_factor_at_root (m : ℕ) (hm : 2 ≤ m) (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_root : Polynomial.eval ρ (polyP ℝ m) = 0) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) : ∃ (S : Polynomial ℝ), polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S ∧ 0 < Polynomial.eval ρ S ∧ IsCoprime (1 - Polynomial.C (1 / ρ) * Polynomial.X) S ∧ Polynomial.eval 0 S = 1 ∧ (∀ (x : ℝ), Polynomial.eval x S = 0 → ρ < x) ∧ S.Splits

theorem Biswal.Theorem1.coe_pow_constantCoeff_ne_zero (p : Polynomial ℝ) (k : ℕ) (hp : p.coeff 0 = 1) : PowerSeries.constantCoeff (↑p ^ k) ≠ 0

theorem Biswal.Theorem1.bezout_lift_to_ps (L S a b : Polynomial ℝ) (k : ℕ) (hbez : a * L ^ k + b * S ^ k = 1) : ↑a * ↑L ^ k + ↑b * ↑S ^ k = 1

theorem Biswal.Theorem1.ps_decomp_core (R_rem Lk Sk : PowerSeries ℝ) (hLk : PowerSeries.constantCoeff Lk ≠ 0) (hSk : PowerSeries.constantCoeff Sk ≠ 0) (a_ps b_ps : PowerSeries ℝ) (hbez : a_ps * Lk + b_ps * Sk = 1) : R_rem * (Lk * Sk)⁻¹ = R_rem * b_ps * Lk⁻¹ + R_rem * a_ps * Sk⁻¹

theorem Biswal.Theorem1.ps_decomp (R_rem : Polynomial ℝ) (k : ℕ) (_hk : 0 < k) (L S : Polynomial ℝ) (hL_const : L.coeff 0 = 1) (hS_const : S.coeff 0 = 1) (a b : Polynomial ℝ) (hbez : a * L ^ k + b * S ^ k = 1) (P : Polynomial ℝ) (hP : P = L * S) : ↑R_rem * (↑P ^ k)⁻¹ = ↑(R_rem * b) * (↑L ^ k)⁻¹ + ↑(R_rem * a) * (↑S ^ k)⁻¹

theorem Biswal.Theorem1.bezout_eval_at_root (L S a b : Polynomial ℝ) (k : ℕ) (hk : 0 < k) (ρ : ℝ) (hL_zero : Polynomial.eval ρ L = 0) (hbez : a * L ^ k + b * S ^ k = 1) : Polynomial.eval ρ b * Polynomial.eval ρ S ^ k = 1

theorem Biswal.Theorem1.bezout_fraction_split (m : ℕ) (_hm : 2 ≤ m) (R_rem : Polynomial ℝ) (k : ℕ) (hk : 0 < k) (ρ : ℝ) (hρ_pos : 0 < ρ) (hR_pos : 0 < Polynomial.eval ρ R_rem) (S : Polynomial ℝ) (hfact : polyP ℝ m = (1 - Polynomial.C (1 / ρ) * Polynomial.X) * S) (hS_pos : 0 < Polynomial.eval ρ S) (hCop : IsCoprime (1 - Polynomial.C (1 / ρ) * Polynomial.X) S) : ∃ (N_poly : Polynomial ℝ) (M_poly : Polynomial ℝ), have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ↑R_rem * (↑(polyP ℝ m) ^ k)⁻¹ = ↑N_poly * (↑L ^ k)⁻¹ + ↑M_poly * (↑S ^ k)⁻¹ ∧ 0 < Polynomial.eval ρ N_poly

theorem Biswal.Theorem1.L_coe_eq_rescale_one_sub_X (ρ : ℝ) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ↑L = (PowerSeries.rescale (1 / ρ)) (1 - PowerSeries.X)

theorem Biswal.Theorem1.one_sub_X_pow_constantCoeff_ne_zero (k : ℕ) : PowerSeries.constantCoeff ((1 - PowerSeries.X) ^ k) ≠ 0

theorem Biswal.Theorem1.inv_one_sub_pow_eq_invOneSubPow (k : ℕ) : ((1 - PowerSeries.X) ^ k)⁻¹ = ↑(PowerSeries.invOneSubPow ℝ k)

theorem Biswal.Theorem1.rescale_inv (a : ℝ) (f : PowerSeries ℝ) (hf : PowerSeries.constantCoeff f ≠ 0) : (PowerSeries.rescale a) f⁻¹ = ((PowerSeries.rescale a) f)⁻¹

theorem Biswal.Theorem1.inv_L_pow_coeff (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (r : ℕ) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; (PowerSeries.coeff r) (↑L ^ k)⁻¹ = ↑((k - 1 + r).choose (k - 1)) * (1 / ρ) ^ r

theorem Biswal.Theorem1.sum_le_pow_mul_sum (q : Polynomial ℝ) (hd : 1 ≤ q.natDegree) (x : ℝ) (hx : 1 ≤ x) : ∑ i ∈ Finset.range q.natDegree, |q.coeff i| * x ^ i ≤ x ^ (q.natDegree - 1) * ∑ i ∈ Finset.range q.natDegree, |q.coeff i|

theorem Biswal.Theorem1.abs_sum_le_pow_mul_sum_abs (q : Polynomial ℝ) (hd : 1 ≤ q.natDegree) (x : ℝ) (hx : 1 ≤ x) : |∑ i ∈ Finset.range q.natDegree, q.coeff i * x ^ i| ≤ x ^ (q.natDegree - 1) * ∑ i ∈ Finset.range q.natDegree, |q.coeff i|

theorem Biswal.Theorem1.poly_eval_lower_bound (q : Polynomial ℝ) (hd : 1 ≤ q.natDegree) (x : ℝ) (hx : 1 ≤ x) : x ^ (q.natDegree - 1) * (q.leadingCoeff * x - ∑ i ∈ Finset.range q.natDegree, |q.coeff i|) ≤ Polynomial.eval x q

theorem Biswal.Theorem1.poly_eventually_pos_nat (q : Polynomial ℝ) (hq : 0 < q.leadingCoeff) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → 0 < Polynomial.eval (↑r) q

Hilbert Polynomial and Eventual Positivity

noncomputable def Biswal.Theorem1.nScaled (ρ : ℝ) (N_poly : Polynomial ℝ) : Polynomial ℝ

The polynomial N_poly rescaled by ρ, i.e. N_poly.comp (C ρ * X).

Equations

• Biswal.Theorem1.nScaled ρ N_poly = N_poly.comp (Polynomial.C ρ * Polynomial.X)

theorem Biswal.Theorem1.N_scaled_coe_eq_rescale (ρ : ℝ) (N_poly : Polynomial ℝ) : ↑(nScaled ρ N_poly) = (PowerSeries.rescale ρ) ↑N_poly

theorem Biswal.Theorem1.N_scaled_eval_one (ρ : ℝ) (N_poly : Polynomial ℝ) : Polynomial.eval 1 (nScaled ρ N_poly) = Polynomial.eval ρ N_poly

theorem Biswal.Theorem1.rescale_rho_L_eq_one_sub_X (ρ : ℝ) (hρ : 0 < ρ) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; (PowerSeries.rescale ρ) ↑L = 1 - PowerSeries.X

theorem Biswal.Theorem1.degree_smul_preHilbertPoly (p : Polynomial ℝ) (d i : ℕ) (hi : i ∈ p.support) : (p.coeff i • Polynomial.preHilbertPoly ℝ d i).degree = ↑d

theorem Biswal.Theorem1.hilbertPoly_succ_leadingCoeff_sum (p : Polynomial ℝ) (d : ℕ) (h_nonzero : ∑ i ∈ p.support, p.coeff i ≠ 0) : (∑ i ∈ p.support, p.coeff i • Polynomial.preHilbertPoly ℝ d i).leadingCoeff = ∑ i ∈ p.support, p.coeff i * (↑d.factorial)⁻¹

theorem Biswal.Theorem1.hilbertPoly_succ_leadingCoeff (p : Polynomial ℝ) (d : ℕ) (hp : Polynomial.eval 1 p ≠ 0) : (p.hilbertPoly (d + 1)).leadingCoeff = Polynomial.eval 1 p * (↑d.factorial)⁻¹

theorem Biswal.Theorem1.hilbertPoly_pos_leadingCoeff (ρ : ℝ) (_hρ : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) : 0 < ((nScaled ρ N_poly).hilbertPoly k).leadingCoeff

theorem Biswal.Theorem1.scaled_coeff_is_eventually_poly (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ∃ (q : Polynomial ℝ) (N₀ : ℕ), 0 < q.leadingCoeff ∧ ∀ (r : ℕ), N₀ < r → ρ ^ r * (PowerSeries.coeff r) (↑N_poly * (↑L ^ k)⁻¹) = Polynomial.eval (↑r) q

theorem Biswal.Theorem1.L_part_eventually_pos (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ∃ (N : ℕ), ∀ (r : ℕ), N < r → 0 < (PowerSeries.coeff r) (↑N_poly * (↑L ^ k)⁻¹)

Coefficient Bounds and Asymptotic Analysis

theorem Biswal.Theorem1.S_eq_one_of_deg_zero_const_one (S : Polynomial ℝ) (hS_const_coeff : Polynomial.eval 0 S = 1) (hS_deg : S.natDegree = 0) : S = 1

theorem Biswal.Theorem1.S_part_eventually_zero_of_const (M_poly S : Polynomial ℝ) (k : ℕ) (_hk : 0 < k) (hS_const_coeff : Polynomial.eval 0 S = 1) (hS_deg : S.natDegree = 0) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → (PowerSeries.coeff r) (↑M_poly * (↑S ^ k)⁻¹) = 0

theorem Biswal.Theorem1.inv_one_pow_coeff_bound (k : ℕ) (_hk : 0 < k) (ρ₁ : ℝ) (hρ₁_pos : 0 < ρ₁) : ∃ (C : ℝ) (D : ℕ), 0 < C ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) (↑1 ^ k)⁻¹| ≤ C * (↑r + 1) ^ D * (1 / ρ₁) ^ r

theorem Biswal.Theorem1.coeff_bound_strengthened (f : PowerSeries ℝ) (C : ℝ) (D : ℕ) (q : ℝ) (hC : 0 < C) (hq : 0 < q) (hbound : ∀ (r : ℕ), |(PowerSeries.coeff r) f| ≤ C * (↑r + 1) ^ D * q ^ r) (r i j : ℕ) (hij : i + j = r) : |(PowerSeries.coeff j) f| ≤ C * (↑r + 1) ^ D * q ^ r * q⁻¹ ^ i

theorem Biswal.Theorem1.antidiag_term_bound (P : Polynomial ℝ) (f : PowerSeries ℝ) (C : ℝ) (D : ℕ) (q : ℝ) (hC : 0 < C) (hq : 0 < q) (hbound : ∀ (r : ℕ), |(PowerSeries.coeff r) f| ≤ C * (↑r + 1) ^ D * q ^ r) (r i j : ℕ) (hij : i + j = r) : |P.coeff i| * |(PowerSeries.coeff j) f| ≤ |P.coeff i| * (C * (↑r + 1) ^ D * q ^ r * q⁻¹ ^ i)

theorem Biswal.Theorem1.antidiag_sum_eq_range_sum (P : Polynomial ℝ) (C : ℝ) (D : ℕ) (q : ℝ) (r : ℕ) : ∑ p ∈ Finset.antidiagonal r, |P.coeff p.1| * (C * (↑r + 1) ^ D * q ^ r * q⁻¹ ^ p.1) = C * (↑r + 1) ^ D * q ^ r * ∑ i ∈ Finset.range (r + 1), |P.coeff i| * q⁻¹ ^ i

theorem Biswal.Theorem1.sum_eq_of_natDegree_lt (P : Polynomial ℝ) (q : ℝ) (r : ℕ) (h : P.natDegree + 1 < r + 1) : ∑ i ∈ Finset.range (r + 1), |P.coeff i| * q⁻¹ ^ i = ∑ i ∈ Finset.range (P.natDegree + 1), |P.coeff i| * q⁻¹ ^ i

theorem Biswal.Theorem1.antidiag_sum_bound (P : Polynomial ℝ) (f : PowerSeries ℝ) (C : ℝ) (D : ℕ) (q : ℝ) (hC : 0 < C) (hq : 0 < q) (hbound : ∀ (r : ℕ), |(PowerSeries.coeff r) f| ≤ C * (↑r + 1) ^ D * q ^ r) (r : ℕ) : ∑ p ∈ Finset.antidiagonal r, |P.coeff p.1| * |(PowerSeries.coeff p.2) f| ≤ (C * ∑ i ∈ Finset.range (P.natDegree + 1), |P.coeff i| * q⁻¹ ^ i) * (↑r + 1) ^ D * q ^ r

theorem Biswal.Theorem1.poly_mul_coeff_bound (P : Polynomial ℝ) (f : PowerSeries ℝ) (C : ℝ) (D : ℕ) (q : ℝ) (hC : 0 < C) (hq : 0 < q) (hbound : ∀ (r : ℕ), |(PowerSeries.coeff r) f| ≤ C * (↑r + 1) ^ D * q ^ r) (r : ℕ) : |(PowerSeries.coeff r) (↑P * f)| ≤ (C * ∑ i ∈ Finset.range (P.natDegree + 1), |P.coeff i| * q⁻¹ ^ i) * (↑r + 1) ^ D * q ^ r

theorem Biswal.Theorem1.poly_mul_preserves_bound (P : Polynomial ℝ) (f : PowerSeries ℝ) (C : ℝ) (D : ℕ) (q : ℝ) (hC : 0 < C) (hq : 0 < q) (hbound : ∀ (r : ℕ), |(PowerSeries.coeff r) f| ≤ C * (↑r + 1) ^ D * q ^ r) : ∃ (C' : ℝ) (D' : ℕ), 0 < C' ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) (↑P * f)| ≤ C' * (↑r + 1) ^ D' * q ^ r

theorem Biswal.Theorem1.choose_le_pow_succ_core (n r : ℕ) : ↑((n + r).choose n) ≤ (↑r + 1) ^ n

theorem Biswal.Theorem1.cauchy_summand_bound (C₁ C₂ : ℝ) (D₁ D₂ : ℕ) (q : ℝ) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hq : 0 ≤ q) (r r₁ r₂ : ℕ) (hr : r₁ + r₂ = r) (b₁ b₂ : ℝ) (hb₁ : |b₁| ≤ C₁ * (↑r₁ + 1) ^ D₁ * q ^ r₁) (hb₂ : |b₂| ≤ C₂ * (↑r₂ + 1) ^ D₂ * q ^ r₂) : |b₁ * b₂| ≤ C₁ * C₂ * (↑r + 1) ^ (D₁ + D₂) * q ^ r

theorem Biswal.Theorem1.cauchy_product_bound (f₁ f₂ : PowerSeries ℝ) (C₁ C₂ : ℝ) (D₁ D₂ : ℕ) (q : ℝ) (hC₁ : 0 < C₁) (hC₂ : 0 < C₂) (hq : 0 < q) (hf₁ : ∀ (r : ℕ), |(PowerSeries.coeff r) f₁| ≤ C₁ * (↑r + 1) ^ D₁ * q ^ r) (hf₂ : ∀ (r : ℕ), |(PowerSeries.coeff r) f₂| ≤ C₂ * (↑r + 1) ^ D₂ * q ^ r) (r : ℕ) : |(PowerSeries.coeff r) (f₁ * f₂)| ≤ C₁ * C₂ * (↑r + 1) ^ (D₁ + D₂ + 1) * q ^ r

theorem Biswal.Theorem1.ps_mul_coeff_bound (f₁ f₂ : PowerSeries ℝ) (C₁ C₂ : ℝ) (D₁ D₂ : ℕ) (q : ℝ) (hC₁ : 0 < C₁) (hC₂ : 0 < C₂) (hq : 0 < q) (hf₁ : ∀ (r : ℕ), |(PowerSeries.coeff r) f₁| ≤ C₁ * (↑r + 1) ^ D₁ * q ^ r) (hf₂ : ∀ (r : ℕ), |(PowerSeries.coeff r) f₂| ≤ C₂ * (↑r + 1) ^ D₂ * q ^ r) : ∃ (C' : ℝ) (D' : ℕ), 0 < C' ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) (f₁ * f₂)| ≤ C' * (↑r + 1) ^ D' * q ^ r

theorem Biswal.Theorem1.single_factor_inv_pow_bound (α ρ₁ : ℝ) (k : ℕ) (hα_pos : 0 < α) (hρ₁_pos : 0 < ρ₁) (hk : 0 < k) (hα_ge : ρ₁ ≤ α) : have L := 1 - Polynomial.C (1 / α) * Polynomial.X; ∀ (r : ℕ), |(PowerSeries.coeff r) (↑L ^ k)⁻¹| ≤ (↑r + 1) ^ (k - 1) * (1 / ρ₁) ^ r

theorem Biswal.Theorem1.base_case_bound (k : ℕ) (ρ₁ : ℝ) (_hk : 0 < k) (hρ₁_pos : 0 < ρ₁) : ∃ (C : ℝ) (D : ℕ), 0 < C ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) (Multiset.map (fun (α : ℝ) => (↑(1 - Polynomial.C (1 / α) * Polynomial.X) ^ k)⁻¹) 0).prod| ≤ C * (↑r + 1) ^ D * (1 / ρ₁) ^ r

theorem Biswal.Theorem1.multiset_prod_inv_bound (roots : Multiset ℝ) (k : ℕ) (ρ₁ : ℝ) (hk : 0 < k) (hρ₁_pos : 0 < ρ₁) (hroots_pos : ∀ α ∈ roots, 0 < α) (hroots_ge : ∀ α ∈ roots, ρ₁ ≤ α) : have F := (Multiset.map (fun (α : ℝ) => (↑(1 - Polynomial.C (1 / α) * Polynomial.X) ^ k)⁻¹) roots).prod; ∃ (C : ℝ) (D : ℕ), 0 < C ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) F| ≤ C * (↑r + 1) ^ D * (1 / ρ₁) ^ r

theorem Biswal.Theorem1.X_sub_C_eq_neg_C_mul_L (α : ℝ) (hα : 0 < α) : Polynomial.X - Polynomial.C α = -Polynomial.C α * (1 - Polynomial.C (1 / α) * Polynomial.X)

theorem Biswal.Theorem1.prod_X_sub_C_eq_scalar_mul_prod_L (roots : Multiset ℝ) (hroots : ∀ α ∈ roots, 0 < α) : (Multiset.map (fun (α : ℝ) => Polynomial.X - Polynomial.C α) roots).prod = (Multiset.map (fun (α : ℝ) => -Polynomial.C α) roots).prod * (Multiset.map (fun (α : ℝ) => 1 - Polynomial.C (1 / α) * Polynomial.X) roots).prod

theorem Biswal.Theorem1.prod_neg_C_eq_C_prod_neg (roots : Multiset ℝ) : (Multiset.map (fun (α : ℝ) => -Polynomial.C α) roots).prod = Polynomial.C (Multiset.map Neg.neg roots).prod

theorem Biswal.Theorem1.leadingCoeff_mul_prod_neg_roots_eq_one (S : Polynomial ℝ) (_hS_ne : S ≠ 0) (hS_splits : S.Splits) (hS_const : Polynomial.eval 0 S = 1) : S.leadingCoeff * (Multiset.map Neg.neg S.roots).prod = 1

theorem Biswal.Theorem1.splits_poly_eq_prod_L (S : Polynomial ℝ) (hS_ne : S ≠ 0) (hS_splits : S.Splits) (hS_const : Polynomial.eval 0 S = 1) (hroots_pos : ∀ x ∈ S.roots, 0 < x) : S = (Multiset.map (fun (α : ℝ) => 1 - Polynomial.C (1 / α) * Polynomial.X) S.roots).prod

theorem Biswal.Theorem1.coe_pow_eq_prod_coe_pow (S : Polynomial ℝ) (hS_eq : S = (Multiset.map (fun (α : ℝ) => 1 - Polynomial.C (1 / α) * Polynomial.X) S.roots).prod) (k : ℕ) : ↑S ^ k = (Multiset.map (fun (α : ℝ) => ↑(1 - Polynomial.C (1 / α) * Polynomial.X) ^ k) S.roots).prod

theorem Biswal.Theorem1.inv_prod_eq_prod_inv_of_roots (roots : Multiset ℝ) (k : ℕ) : (Multiset.map (fun (α : ℝ) => ↑(1 - Polynomial.C (1 / α) * Polynomial.X) ^ k) roots).prod⁻¹ = (Multiset.map (fun (α : ℝ) => (↑(1 - Polynomial.C (1 / α) * Polynomial.X) ^ k)⁻¹) roots).prod

theorem Biswal.Theorem1.splits_inv_pow_eq_multiset_prod (S : Polynomial ℝ) (k : ℕ) (_hk : 0 < k) (hS_ne : S ≠ 0) (hS_splits : S.Splits) (hS_const : Polynomial.eval 0 S = 1) (hroots_pos : ∀ x ∈ S.roots, 0 < x) : 0 < S.natDegree → ∃ (P : Polynomial ℝ), (↑S ^ k)⁻¹ = ↑P * (Multiset.map (fun (α : ℝ) => (↑(1 - Polynomial.C (1 / α) * Polynomial.X) ^ k)⁻¹) S.roots).prod

theorem Biswal.Theorem1.inv_splits_pow_coeff_bound (S : Polynomial ℝ) (k : ℕ) (hk : 0 < k) (hS_ne : S ≠ 0) (hS_splits : S.Splits) (hS_const : Polynomial.eval 0 S = 1) (ρ₁ : ℝ) (hρ₁_pos : 0 < ρ₁) (hρ₁_le : ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ₁ ≤ x) : ∃ (C : ℝ) (D : ℕ), 0 < C ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) (↑S ^ k)⁻¹| ≤ C * (↑r + 1) ^ D * (1 / ρ₁) ^ r

theorem Biswal.Theorem1.eval_eq_zero_of_mem_roots_toFinset (S : Polynomial ℝ) (hS_ne : S ≠ 0) {x : ℝ} (hx : x ∈ S.roots.toFinset) : Polynomial.eval x S = 0

theorem Biswal.Theorem1.exists_min_root_gt (S : Polynomial ℝ) (ρ : ℝ) (hρ_pos : 0 < ρ) (hS_ne : S ≠ 0) (hS_splits : S.Splits) (hS_nconst : 0 < S.natDegree) (hS_roots_larger : ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ < x) : ∃ (ρ₁ : ℝ), ρ < ρ₁ ∧ 0 < ρ₁ ∧ ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ₁ ≤ x

theorem Biswal.Theorem1.S_part_coeff_bound (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (M_poly S : Polynomial ℝ) (hS_pos : 0 < Polynomial.eval ρ S) (hS_const : Polynomial.eval 0 S = 1) (hS_roots_larger : ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ < x) (hS_splits : S.Splits) (hS_nconst : 0 < S.natDegree) : ∃ (C : ℝ) (D : ℕ) (ρ₂ : ℝ), 0 < C ∧ ρ < ρ₂ ∧ ∀ (r : ℕ), |(PowerSeries.coeff r) (↑M_poly * (↑S ^ k)⁻¹)| ≤ C * (↑r + 1) ^ D * (1 / ρ₂) ^ r

theorem Biswal.Theorem1.poly_eq_of_eventually_eq (q₁ q₂ : Polynomial ℝ) (N : ℕ) (h : ∀ (r : ℕ), N < r → Polynomial.eval (↑r) q₁ = Polynomial.eval (↑r) q₂) : q₁ = q₂

theorem Biswal.Theorem1.scaled_coeff_poly_degree_ge (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) (q : Polynomial ℝ) (N₀ : ℕ) (_hq_lc : 0 < q.leadingCoeff) (hq_eq : ∀ (r : ℕ), N₀ < r → ρ ^ r * (PowerSeries.coeff r) (↑N_poly * (↑(1 - Polynomial.C (1 / ρ) * Polynomial.X) ^ k)⁻¹) = Polynomial.eval (↑r) q) : k - 1 ≤ q.natDegree

theorem Biswal.Theorem1.divide_by_rho_pow (ρ : ℝ) (hρ : 0 < ρ) (c : ℝ) (d r : ℕ) (x : ℝ) (h : c * ↑r ^ d ≤ ρ ^ r * x) : c * ↑r ^ d * (1 / ρ) ^ r ≤ x

theorem Biswal.Theorem1.poly_lower_bound_at_point (q : Polynomial ℝ) (hq : 0 < q.leadingCoeff) (hdeg : 1 ≤ q.natDegree) (d : ℕ) (hd : d ≤ q.natDegree) (x : ℝ) (hx : 1 ≤ x) (hxS : (2 * ∑ i ∈ Finset.range q.natDegree, |q.coeff i|) / q.leadingCoeff < x) : q.leadingCoeff / 2 * x ^ d ≤ Polynomial.eval x q

theorem Biswal.Theorem1.poly_eventually_lower_bound_of_deg_ge_one (q : Polynomial ℝ) (hq : 0 < q.leadingCoeff) (hdeg : 1 ≤ q.natDegree) (d : ℕ) (hd : d ≤ q.natDegree) : ∃ (c : ℝ) (N : ℕ), 0 < c ∧ ∀ (r : ℕ), N < r → c * ↑r ^ d ≤ Polynomial.eval (↑r) q

theorem Biswal.Theorem1.poly_eventually_lower_bound (q : Polynomial ℝ) (hq : 0 < q.leadingCoeff) (d : ℕ) (hd : d ≤ q.natDegree) : ∃ (c : ℝ) (N : ℕ), 0 < c ∧ ∀ (r : ℕ), N < r → c * ↑r ^ d ≤ Polynomial.eval (↑r) q

theorem Biswal.Theorem1.L_part_coeff_lower_bound (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ∃ (c : ℝ) (N : ℕ), 0 < c ∧ ∀ (r : ℕ), N < r → c * ↑r ^ (k - 1) * (1 / ρ) ^ r ≤ (PowerSeries.coeff r) (↑N_poly * (↑L ^ k)⁻¹)

theorem Biswal.Theorem1.bound_transfer (C c : ℝ) (D E r : ℕ) (ρ ρ₂ : ℝ) (hρ_pos : 0 < ρ) (hρ₂_pos : 0 < ρ₂) (h : C * (↑r + 1) ^ D * (ρ / ρ₂) ^ r < c * ↑r ^ E) : C * (↑r + 1) ^ D * (1 / ρ₂) ^ r < c * ↑r ^ E * (1 / ρ) ^ r

theorem Biswal.Theorem1.tendsto_add_one_pow_mul_geometric (D : ℕ) (q : ℝ) (hq_pos : 0 ≤ q) (hq_lt : q < 1) : Filter.Tendsto (fun (r : ℕ) => (↑r + 1) ^ D * q ^ r) Filter.atTop (nhds 0)

theorem Biswal.Theorem1.poly_geometric_eventually_lt (C c : ℝ) (_hC : 0 < C) (hc : 0 < c) (D E : ℕ) (q : ℝ) (hq_pos : 0 < q) (hq_lt : q < 1) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → C * (↑r + 1) ^ D * q ^ r < c * ↑r ^ E

theorem Biswal.Theorem1.S_part_eventually_dominated (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly M_poly S : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) (hS_pos : 0 < Polynomial.eval ρ S) (hS_const : Polynomial.eval 0 S = 1) (hS_roots_larger : ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ < x) (hS_splits : S.Splits) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ∃ (N : ℕ), ∀ (r : ℕ), N < r → |(PowerSeries.coeff r) (↑M_poly * (↑S ^ k)⁻¹)| < (PowerSeries.coeff r) (↑N_poly * (↑L ^ k)⁻¹)

theorem Biswal.Theorem1.sum_parts_eventually_pos (ρ : ℝ) (hρ_pos : 0 < ρ) (k : ℕ) (hk : 0 < k) (N_poly M_poly S : Polynomial ℝ) (hN_pos : 0 < Polynomial.eval ρ N_poly) (hS_pos : 0 < Polynomial.eval ρ S) (hS_const : Polynomial.eval 0 S = 1) (hS_roots_larger : ∀ (x : ℝ), Polynomial.eval x S = 0 → ρ < x) (hS_splits : S.Splits) : have L := 1 - Polynomial.C (1 / ρ) * Polynomial.X; ∃ (N : ℕ), ∀ (r : ℕ), N < r → 0 < (PowerSeries.coeff r) (↑N_poly * (↑L ^ k)⁻¹ + ↑M_poly * (↑S ^ k)⁻¹)

theorem Biswal.Theorem1.proper_fraction_coeff_pos_over_R (m : ℕ) (hm : 2 ≤ m) (R_rem : Polynomial ℝ) (k : ℕ) (hk : 0 < k) (ρ : ℝ) (hρ_pos : 0 < ρ) (hρ_root : Polynomial.eval ρ (polyP ℝ m) = 0) (hρ_lower : ∀ j < m, 0 < Polynomial.eval ρ (polyP ℝ j)) (hR_pos : 0 < Polynomial.eval ρ R_rem) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → 0 < (PowerSeries.coeff r) (↑R_rem * (↑(polyP ℝ m) ^ k)⁻¹)

theorem Biswal.Theorem1.map_genFun_comm (R_poly : Polynomial ℚ) (m k : ℕ) : (PowerSeries.map (algebraMap ℚ ℝ)) (↑R_poly * (↑(polyP ℚ m) ^ k)⁻¹) = ↑(Polynomial.map (algebraMap ℚ ℝ) R_poly) * (↑(polyP ℝ m) ^ k)⁻¹

theorem Biswal.Theorem1.proper_fraction_coeff_eventually_pos (m : ℕ) (hm : 2 ≤ m) (R_poly : Polynomial ℚ) (k : ℕ) (hk : 0 < k) (hR_pos_at_root : ∀ (ρ : ℝ), 0 < ρ → Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) (polyP ℚ m)) = 0 → (∀ j < m, 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) (polyP ℚ j))) → 0 < Polynomial.eval ρ (Polynomial.map (algebraMap ℚ ℝ) R_poly)) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → 0 < (PowerSeries.coeff r) (↑R_poly * (↑(polyP ℚ m) ^ k)⁻¹)

Main Theorems

theorem Biswal.Theorem1.genFun_eq_one_of_m_eq_one (K : Type u_1) [Field K] (n : ℕ) {s : ℕ} (ξ : s.Partition) (h_parts : ∀ i ∈ ξ.parts, i ≤ 1) : genFun K 1 n ξ = 1

theorem Biswal.Theorem1.genFun_is_polynomial (K : Type u_1) [Field K] (m n : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (h_t : n / m + 1 ≤ countMaxParts m ξ) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → genFunCoeff K m n r ξ = 0

theorem Biswal.Theorem1.genFun_coeff_eventually_pos (m n : ℕ) {s : ℕ} (ξ : s.Partition) (hm : 2 ≤ m) (h_parts : ∀ i ∈ ξ.parts, i ≤ m) (h_t : countMaxParts m ξ ≤ n / m) : ∃ (N : ℕ), ∀ (r : ℕ), N < r → 0 < genFunCoeff ℚ m n r ξ