Coleman's finite spectral transform

Let R be a commutative ring, P B : R[X] with P.coeff 0 = 1, P.natDegree ≤ n and B.natDegree ≤ m. Coleman's transform of rank n is the polynomial

D_(n,m)(B, P)(T) = Res_X (reflect n P (X), 1 - T B(X)),

a resultant over R[T] with the degree bounds n and m (Polynomial.colemanDBounded). If P = ∏ (1 - αᵢ T) is a product of n linear factors, then reflect n P = ∏ (X - αᵢ) and D_(n,m)(B, P) = ∏ (1 - B(αᵢ) T) (Polynomial.colemanDBounded_prod_one_sub_C_mul_X). For P = det (1 - T A) with A an n × n matrix over any commutative ring, the transform computes det (1 - T B(A)) from P alone, without access to A or to its eigenvalues (Matrix.colemanDBounded_charpolyRev). This is the polynomial form of the spectral mapping for Fredholm determinants of compact operators.

The rank is part of the data. The reversal is taken in the specified degree n, not in the actual degree of P, so that zero eigenvalues are kept: raising the rank by one multiplies by the factor 1 - B(0) T of a new zero eigenvalue (Polynomial.colemanDBounded_succ). The rank is therefore irrelevant when B(0) = 0 (Polynomial.colemanDBounded_add_of_coeff_zero), and the minimal-rank transform Polynomial.colemanD then agrees with every bounded one (Polynomial.colemanD_eq_colemanDBounded). The bound m is irrelevant once it bounds the degree of B (Polynomial.colemanDBounded_of_natDegree_le).

Evaluating the transform at a scalar t gives the resultant over R of reflect n P and 1 - t B (Polynomial.eval_colemanDBounded). For a polynomial Q with Q(0) = 1 and invertible leading coefficient, and c the inverse of that coefficient, the polynomial B = 1 - c Q* built from the reversal Q* = Q.reverse vanishes at 0 and sends every inverse root of Q to 1. Accordingly D(B, Q) = (1 - T) ^ deg Q (Polynomial.colemanDSeries_one_sub_C_mul_reverse_self), while the value at T = 1 of the transform of any F is the resultant of the monic polynomial c Q and F (Polynomial.eval_one_colemanDBounded_one_sub_C_mul_reflect), a unit exactly when Q and F are coprime (Polynomial.isUnit_eval_one_colemanDBounded_one_sub_C_mul_reverse_iff). So if a Fredholm determinant factors as Q S, its transform along B is (1 - T) ^ deg Q times the transform of S. For a polynomial S with S(0) = 1 the latter is a unit at T = 1 exactly when Q and S are coprime: a coprime polynomial factor becomes a zero of order deg Q at one.

When B(0) = 0, the k-th coefficient of D_(n,m)(B, P) only involves the coefficients of P of index at most k m (Polynomial.coeff_colemanDBounded_congr): in the Leibniz expansion of the Sylvester matrix, a term contributing to Tᵏ moves exactly k of the first n columns down, each by at most m rows, so the columns carrying the coefficients of P move up by at most k m rows in total. Hence Coleman's transform extends to a power series input F: the series Polynomial.colemanDSeries B F has as k-th coefficient that of D_(N,m)(B, trunc (N + 1) F) for any N ≥ k m. It is multiplicative in F (Polynomial.colemanDSeries_mul), agrees with the polynomial transform on polynomials (Polynomial.colemanDSeries_coe), and each of its coefficients is a polynomial, hence continuous, function of finitely many coefficients of F (Polynomial.continuous_coeff_colemanDSeries). This is the transform computing Fredholm determinants of polynomials in compact operators.

Main results

• Polynomial.colemanDBounded_of_natDegree_le: independence of the degree bound for B.
• Polynomial.colemanDBounded_succ, Polynomial.colemanDBounded_add: padding the rank.
• Polynomial.colemanDBounded_mul: multiplicativity in P, with addition of ranks.
• Polynomial.colemanDBounded_map: compatibility with coefficient ring homomorphisms.
• Polynomial.natDegree_colemanDBounded_le, Polynomial.coeff_zero_colemanDBounded: the transform of rank n has degree at most n and constant coefficient one.
• Polynomial.colemanDBounded_prod_one_sub_C_mul_X: the transform of a product of linear factors.
• Matrix.colemanDBounded_charpolyRev: finite matrix spectral mapping, D_(n,m)(B, det (1 - T A)) = det (1 - T B(A)) for an n × n matrix A.
• Polynomial.colemanDBounded_X_left, Polynomial.colemanDBounded_zero_left, Polynomial.colemanDBounded_one_right: the values D(T, P) = P, D(0, P) = 1 and D(B, 1) = (1 - B(0) T) ^ n.
• Polynomial.eval_colemanDBounded: the value at t is Res_(n,m)(reflect n P, 1 - t B).
• Polynomial.colemanDBounded_one_sub_C_mul_reflect_self: D_(n,n)(1 - c P*, P) = (1 - T) ^ n for the reversal P* = reflect n P.
• Polynomial.eval_one_colemanDBounded_one_sub_C_mul_reflect: the value at T = 1 of D_(n,d)(1 - c Q*, F) is Res_(d,n)(c Q, F) for Q* = reflect d Q.
• Polynomial.isUnit_eval_one_colemanDBounded_one_sub_C_mul_reverse_iff: for c inverting the leading coefficient of Q, that value is a unit exactly when Q and F are coprime.
• Polynomial.coeff_prod_sylvester_colemanDBounded: the terms of the Leibniz expansion of the Sylvester matrix defining the transform when B(0) = 0.
• Polynomial.coeff_colemanDBounded_congr: locality of the coefficients in P when B(0) = 0.
• Polynomial.colemanDSeries: Coleman's transform of a power series along a polynomial B, with Polynomial.coeff_colemanDSeries_eq_coeff_colemanDBounded, Polynomial.coeff_colemanDSeries, Polynomial.colemanDSeries_coe, Polynomial.colemanDSeries_mul and Polynomial.continuous_coeff_colemanDSeries.
• Polynomial.colemanDSeries_one_sub_C_mul_reverse_self: D(1 - c Q*, Q) = (1 - T) ^ deg Q when Q(0) = 1 and c inverts the leading coefficient of Q.

References

• R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendices A3–A4.

noncomputable def Polynomial.colemanDBounded {R : Type u_1} [CommRing R] (B P : Polynomial R) (n m : ℕ) : Polynomial R

Coleman's transform of rank n: for P with P.coeff 0 = 1 and P.natDegree ≤ n, and B with B.natDegree ≤ m, the polynomial Res_X (reflect n P (X), 1 - T B(X)) in T, a resultant over R[T] with degree bounds n and m. If P = ∏ (1 - αᵢ T) over n factors, it is ∏ (1 - B(αᵢ) T). The resultant is defined for all B, P, n and m; the hypotheses are those under which it has this meaning.

noncomputable def Polynomial.colemanD {R : Type u_1} [CommRing R] (B P : Polynomial R) : Polynomial R

Coleman's transform at the minimal rank P.natDegree and degree bound B.natDegree.

theorem Polynomial.colemanDBounded_def {R : Type u_1} [CommRing R] (B P : Polynomial R) (n m : ℕ) : B.colemanDBounded P n m = (map C (reflect n P)).resultant (1 - C X * map C B) n m

theorem Polynomial.colemanD_def {R : Type u_1} [CommRing R] (B P : Polynomial R) : B.colemanD P = B.colemanDBounded P P.natDegree B.natDegree

theorem Polynomial.natDegree_one_sub_C_X_mul_map_le {R : Type u_1} [CommRing R] {B : Polynomial R} {m : ℕ} (hB : B.natDegree ≤ m) : (1 - C X * map C B).natDegree ≤ m

The kernel 1 - T B(X) of Coleman's transform has degree in X at most any bound for the degree of B.

theorem Polynomial.colemanDBounded_add_right_deg {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hB : B.natDegree ≤ m) (hP0 : P.coeff 0 = 1) (k : ℕ) : B.colemanDBounded P n (m + k) = B.colemanDBounded P n m

Raising the degree bound for B does not change Coleman's transform.

theorem Polynomial.colemanDBounded_of_natDegree_le {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hB : B.natDegree ≤ m) (hP0 : P.coeff 0 = 1) : B.colemanDBounded P n m = B.colemanDBounded P n B.natDegree

Coleman's transform does not depend on the chosen bound for the degree of B.

theorem Polynomial.colemanDBounded_succ {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hP : P.natDegree ≤ n) (hB : B.natDegree ≤ m) : B.colemanDBounded P (n + 1) m = (1 - C (B.coeff 0) * X) * B.colemanDBounded P n m

Padding the rank by one multiplies Coleman's transform by 1 - B(0) T, the factor of an additional zero eigenvalue.

theorem Polynomial.colemanDBounded_add {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hP : P.natDegree ≤ n) (hB : B.natDegree ≤ m) (k : ℕ) : B.colemanDBounded P (n + k) m = (1 - C (B.coeff 0) * X) ^ k * B.colemanDBounded P n m

Padding the rank by k multiplies Coleman's transform by (1 - B(0) T) ^ k.

theorem Polynomial.colemanDBounded_add_of_coeff_zero {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hP : P.natDegree ≤ n) (hB : B.natDegree ≤ m) (hB0 : B.coeff 0 = 0) (k : ℕ) : B.colemanDBounded P (n + k) m = B.colemanDBounded P n m

When B(0) = 0, Coleman's transform does not depend on the rank.

theorem Polynomial.colemanD_eq_colemanDBounded {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hP : P.natDegree ≤ n) (hB : B.natDegree ≤ m) (hP0 : P.coeff 0 = 1) (hB0 : B.coeff 0 = 0) : B.colemanD P = B.colemanDBounded P n m

When B(0) = 0, the minimal-rank transform equals every bounded Coleman transform.

theorem Polynomial.colemanDBounded_mul {R : Type u_1} [CommRing R] {B : Polynomial R} {m : ℕ} {P₁ P₂ : Polynomial R} {n₁ n₂ : ℕ} (hP₁ : P₁.natDegree ≤ n₁) (hP₂ : P₂.natDegree ≤ n₂) (hB : B.natDegree ≤ m) : B.colemanDBounded (P₁ * P₂) (n₁ + n₂) m = B.colemanDBounded P₁ n₁ m * B.colemanDBounded P₂ n₂ m

Coleman's transform is multiplicative in P, the ranks adding.

@[simp]

theorem Polynomial.colemanDBounded_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (B P : Polynomial R) (n m : ℕ) : map φ (B.colemanDBounded P n m) = (map φ B).colemanDBounded (map φ P) n m

Coleman's transform commutes with coefficient ring homomorphisms.

theorem Polynomial.natDegree_colemanDBounded_le {R : Type u_1} [CommRing R] (B P : Polynomial R) (n m : ℕ) : (B.colemanDBounded P n m).natDegree ≤ n

Coleman's transform of rank n is a polynomial of degree at most n.

theorem Polynomial.eval_colemanDBounded {R : Type u_1} [CommRing R] (B P : Polynomial R) (n m : ℕ) (t : R) : eval t (B.colemanDBounded P n m) = (reflect n P).resultant (1 - C t * B) n m

The value of Coleman's transform at t is the resultant over R of the reversal of P and 1 - t B, with the same degree bounds.

@[simp]

theorem Polynomial.coeff_zero_colemanDBounded {R : Type u_1} [CommRing R] {P : Polynomial R} (hP0 : P.coeff 0 = 1) (B : Polynomial R) (n m : ℕ) : (B.colemanDBounded P n m).coeff 0 = 1

Coleman's transform has constant coefficient one.

@[simp]

theorem Polynomial.colemanDBounded_X_left {R : Type u_1} [CommRing R] {P : Polynomial R} {n : ℕ} (hP : P.natDegree ≤ n) : X.colemanDBounded P n 1 = P

With B = T, Coleman's transform returns P: the eigenvalues are unchanged.

@[simp]

theorem Polynomial.colemanDBounded_zero_left {R : Type u_1} [CommRing R] {P : Polynomial R} (hP0 : P.coeff 0 = 1) (n m : ℕ) : colemanDBounded 0 P n m = 1

With B = 0, Coleman's transform is one.

@[simp]

theorem Polynomial.colemanDBounded_one_right {R : Type u_1} [CommRing R] {B : Polynomial R} {m : ℕ} (hB : B.natDegree ≤ m) (n : ℕ) : B.colemanDBounded 1 n m = (1 - C (B.coeff 0) * X) ^ n

With P = 1, all n eigenvalues are zero, and Coleman's transform is (1 - B(0) T) ^ n.

theorem Polynomial.colemanDBounded_one_sub_C_mul_X {R : Type u_1} [CommRing R] {B : Polynomial R} {m : ℕ} (hB : B.natDegree ≤ m) (α : R) : B.colemanDBounded (1 - C α * X) 1 m = 1 - C (eval α B) * X

Coleman's transform of a single factor 1 - α T is 1 - B(α) T.

theorem Polynomial.colemanDBounded_prod_one_sub_C_mul_X {R : Type u_1} [CommRing R] {B : Polynomial R} {m : ℕ} {ι : Type u_3} (s : Finset ι) (α : ι → R) (hB : B.natDegree ≤ m) : B.colemanDBounded (∏ i ∈ s, (1 - C (α i) * X)) s.card m = ∏ i ∈ s, (1 - C (eval (α i) B) * X)

If P = ∏ (1 - αᵢ T) has one factor for each unit of rank, Coleman's transform is ∏ (1 - B(αᵢ) T): it replaces each inverse root αᵢ by B(αᵢ).

theorem Polynomial.colemanDBounded_one_sub_C_mul_reflect_self {R : Type u_1} [CommRing R] {P : Polynomial R} {n : ℕ} (hP : P.natDegree ≤ n) (hP0 : P.coeff 0 = 1) (c : R) : (1 - C c * reflect n P).colemanDBounded P n n = (1 - X) ^ n

Along B = 1 - c P*, where P* = reflect n P is the reversal of P in its rank n, Coleman's transform of P is (1 - T) ^ n: if P = ∏ (1 - αᵢ T), then P* = ∏ (X - αᵢ) and B(αᵢ) = 1 for every i. No hypothesis on c is needed.

theorem Polynomial.eval_one_colemanDBounded_one_sub_C_mul_reflect {R : Type u_1} [CommRing R] (c : R) (F Q : Polynomial R) (n d : ℕ) : eval 1 ((1 - C c * reflect d Q).colemanDBounded F n d) = (C c * Q).resultant F d n

Along B = 1 - c Q*, where Q* = reflect d Q, the value at T = 1 of Coleman's transform of F is the resultant of c Q and F. If c Q = ∏ (T - rᵢ) and F = ∏ (1 - βⱼ T) have degrees d and n, then 1 - B = c Q* = ∏ (1 - rᵢ X) and both sides are ∏ᵢ ∏ⱼ (1 - rᵢ βⱼ).

theorem Polynomial.coeff_zero_one_sub_C_mul_reverse {R : Type u_1} [CommRing R] {Q : Polynomial R} {c : R} (hc : c * Q.leadingCoeff = 1) : (1 - C c * Q.reverse).coeff 0 = 0

If c inverts the leading coefficient of Q, then 1 - c Q* vanishes at 0, since the constant coefficient of the reversal Q* is the leading coefficient of Q.

theorem Polynomial.natDegree_one_sub_C_mul_reverse_le {R : Type u_1} [CommRing R] (c : R) (Q : Polynomial R) : (1 - C c * Q.reverse).natDegree ≤ Q.natDegree

The polynomial 1 - c Q* has degree at most that of Q.

theorem Polynomial.isUnit_eval_one_colemanDBounded_one_sub_C_mul_reverse_iff {R : Type u_1} [CommRing R] {n : ℕ} {Q F : Polynomial R} {c : R} (hc : c * Q.leadingCoeff = 1) (hF : F.natDegree ≤ n) : IsUnit (eval 1 ((1 - C c * Q.reverse).colemanDBounded F n Q.natDegree)) ↔ IsCoprime Q F

Let c invert the leading coefficient of Q. Along B = 1 - c Q*, the value at T = 1 of Coleman's transform of a polynomial F of degree at most n is a unit exactly when Q and F are coprime. This is the polynomial step of Coleman's Appendix A4, in which a coprime factor Q of a Fredholm determinant becomes a zero at T = 1 along 1 - lc(Q)⁻¹ Q*.

theorem Polynomial.sylvester_map_reflect_one_sub_apply {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hB0 : B.coeff 0 = 0) {i x : Fin (n + m)} (h₁ : ↑x < n → ↑x ≤ ↑i ∧ ↑i ≤ ↑x + m) (h₂ : n ≤ ↑x → ↑x ≤ ↑i + n ∧ ↑i ≤ ↑x) : (map C (reflect n P)).sylvester (1 - C X * map C B) n m i x = C (if ↑x < ↑i then -B.coeff (↑i - ↑x) else if ↑x < n then 1 else P.coeff (↑x - ↑i)) * X ^ if ↑x < ↑i then 1 else 0

An entry of the Sylvester matrix defining Coleman's transform D_(n,m)(B, P) with B(0) = 0, in row i and column x, inside the band where it can be nonzero, is a monomial in T. In the first n columns it is 1 on the diagonal and -b_(i - x) T below it, and in the last m columns it is the coefficient P_(x - i).

theorem Polynomial.coeff_prod_sylvester_colemanDBounded {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hB0 : B.coeff 0 = 0) (σ : Equiv.Perm (Fin (n + m))) (k : ℕ) : (∏ x : Fin (n + m), (map C (reflect n P)).sylvester (1 - C X * map C B) n m (σ x) x).coeff k = if (∀ (x : Fin (n + m)), (↑x < n → ↑x ≤ ↑(σ x) ∧ ↑(σ x) ≤ ↑x + m) ∧ (n ≤ ↑x → ↑x ≤ ↑(σ x) + n ∧ ↑(σ x) ≤ ↑x)) ∧ k = {x : Fin (n + m) | ↑x < ↑(σ x)}.card then ∏ x : Fin (n + m), if ↑x < ↑(σ x) then -B.coeff (↑(σ x) - ↑x) else if ↑x < n then 1 else P.coeff (↑x - ↑(σ x)) else 0

The coefficients of the terms of the Leibniz expansion of the Sylvester matrix defining Coleman's transform D_(n,m)(B, P) with B(0) = 0. The term of σ vanishes unless σ moves each of the first n columns x to a row in [x, x + m] and each of the last m columns to a row in [x - n, x]. It is then a monomial of degree the number of forward moves, whose entries are 1 or -b_(σ x - x) T in the first n columns, according as σ x = x or not, and a_(x - σ x) in the last m columns.

theorem Polynomial.coeff_colemanDBounded_congr {R : Type u_1} [CommRing R] {B P : Polynomial R} {n m : ℕ} (hB0 : B.coeff 0 = 0) {P' : Polynomial R} {k : ℕ} (h : ∀ j ≤ k * m, P.coeff j = P'.coeff j) : (B.colemanDBounded P n m).coeff k = (B.colemanDBounded P' n m).coeff k

Locality of Coleman's transform. When B(0) = 0, the k-th coefficient of D_(n,m)(B, P) depends only on the coefficients of P of index at most k m.

noncomputable def Polynomial.colemanDSeries {R : Type u_1} [CommRing R] (B : Polynomial R) (F : PowerSeries R) : PowerSeries R

Coleman's transform with polynomial functional input B and power series input F. Its k-th coefficient is the k-th coefficient of D_(N,m)(B, trunc (N + 1) F) for m = deg B and N = k m. When B(0) = 0 the same coefficient is obtained for every rank N ≥ k m (Polynomial.coeff_colemanDSeries), and for a polynomial F the series is the polynomial transform (Polynomial.colemanDSeries_coe). If B(0) ≠ 0 the finite transforms need not stabilise and this series has no spectral meaning in general.

theorem Polynomial.colemanDSeries_def {R : Type u_1} [CommRing R] (B : Polynomial R) (F : PowerSeries R) : B.colemanDSeries F = PowerSeries.mk fun (k : ℕ) => (B.colemanDBounded ((PowerSeries.trunc (k * B.natDegree + 1)) F) (k * B.natDegree) B.natDegree).coeff k

theorem Polynomial.coeff_colemanDSeries_eq_coeff_colemanDBounded {R : Type u_1} [CommRing R] (B : Polynomial R) (F : PowerSeries R) (k : ℕ) : (PowerSeries.coeff k) (B.colemanDSeries F) = (B.colemanDBounded ((PowerSeries.trunc (k * B.natDegree + 1)) F) (k * B.natDegree) B.natDegree).coeff k

For any B, the k-th coefficient of Coleman's transform of F is that of the finite transform of trunc (N + 1) F at the rank N = k deg B.

theorem Polynomial.coeff_colemanDSeries {R : Type u_1} [CommRing R] {B : Polynomial R} (hB0 : B.coeff 0 = 0) {F : PowerSeries R} {k N : ℕ} (hN : k * B.natDegree ≤ N) : (PowerSeries.coeff k) (B.colemanDSeries F) = (B.colemanDBounded ((PowerSeries.trunc (N + 1)) F) N B.natDegree).coeff k

When B(0) = 0, the k-th coefficient of Coleman's transform of F is that of the finite transform of the truncation trunc (N + 1) F at any rank N ≥ k deg B.

theorem Polynomial.coeff_colemanDSeries_of_natDegree_le {R : Type u_1} [CommRing R] {B : Polynomial R} {m : ℕ} (hB0 : B.coeff 0 = 0) {F : PowerSeries R} (hF0 : PowerSeries.constantCoeff F = 1) {k N : ℕ} (hB : B.natDegree ≤ m) (hN : k * m ≤ N) : (PowerSeries.coeff k) (B.colemanDSeries F) = (B.colemanDBounded ((PowerSeries.trunc (N + 1)) F) N m).coeff k

When B(0) = 0 and F(0) = 1, the k-th coefficient of Coleman's transform of F is that of D_(N,m)(B, trunc (N + 1) F) for every degree bound m ≥ deg B and rank N ≥ k m.

theorem Polynomial.colemanDSeries_coe_of_natDegree_le {R : Type u_1} [CommRing R] {B P : Polynomial R} {n : ℕ} (hB0 : B.coeff 0 = 0) (hP : P.natDegree ≤ n) : B.colemanDSeries ↑P = ↑(B.colemanDBounded P n B.natDegree)

When B(0) = 0, Coleman's transform of a polynomial P of degree at most n is the finite transform of rank n.

@[simp]

theorem Polynomial.colemanDSeries_coe {R : Type u_1} [CommRing R] {B : Polynomial R} (hB0 : B.coeff 0 = 0) (P : Polynomial R) : B.colemanDSeries ↑P = ↑(B.colemanD P)

When B(0) = 0, Coleman's transform of a polynomial P is the minimal-rank transform Polynomial.colemanD B P.

@[simp]

theorem Polynomial.constantCoeff_colemanDSeries {R : Type u_1} [CommRing R] {B : Polynomial R} {F : PowerSeries R} (hF0 : PowerSeries.constantCoeff F = 1) : PowerSeries.constantCoeff (B.colemanDSeries F) = 1

Coleman's transform of a normalised power series is normalised.

theorem Polynomial.colemanDSeries_mul {R : Type u_1} [CommRing R] {B : Polynomial R} (hB0 : B.coeff 0 = 0) (F G : PowerSeries R) : B.colemanDSeries (F * G) = B.colemanDSeries F * B.colemanDSeries G

Multiplicativity in F. When B(0) = 0, Coleman's transform of a product of power series is the product of their transforms.

@[simp]

theorem Polynomial.colemanDSeries_X_left {R : Type u_1} [CommRing R] (F : PowerSeries R) : X.colemanDSeries F = F

With B = T, Coleman's transform returns F.

@[simp]

theorem Polynomial.colemanDSeries_zero_left {R : Type u_1} [CommRing R] (F : PowerSeries R) : colemanDSeries 0 F = 1

With B = 0, Coleman's transform of any power series is one.

@[simp]

theorem Polynomial.colemanDSeries_one_right {R : Type u_1} [CommRing R] {B : Polynomial R} (hB0 : B.coeff 0 = 0) : B.colemanDSeries 1 = 1

When B(0) = 0, Coleman's transform of 1 is one.

theorem Polynomial.colemanDSeries_one_sub_C_mul_reverse_self {R : Type u_1} [CommRing R] {Q : Polynomial R} {c : R} (hQ0 : Q.coeff 0 = 1) (hc : c * Q.leadingCoeff = 1) : (1 - C c * Q.reverse).colemanDSeries ↑Q = (1 - PowerSeries.X) ^ Q.natDegree

Let Q(0) = 1 and let c invert the leading coefficient of Q, so that B = 1 - c Q* vanishes at 0. Coleman's transform of Q along B is (1 - T) ^ deg Q: the polynomial B sends every inverse root of Q to 1.

theorem Polynomial.continuous_coeff_colemanDSeries {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalSemiring R] (B : Polynomial R) (k : ℕ) : Continuous fun (F : PowerSeries R) => (PowerSeries.coeff k) (B.colemanDSeries F)

Each coefficient of Coleman's transform is a continuous function of F for the topology of coefficientwise convergence: it is a polynomial in the coefficients of F of index at most k deg B.

theorem Matrix.colemanDBounded_charpolyRev {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing R] (A : Matrix ι ι R) {B : Polynomial R} {m : ℕ} (hB : B.natDegree ≤ m) : B.colemanDBounded A.charpolyRev (Fintype.card ι) m = ((Polynomial.aeval A) B).charpolyRev

Finite matrix spectral mapping. For an n × n matrix A and B of degree at most m, Coleman's transform of rank n of det (1 - T A) is det (1 - T B(A)). The rank must be the dimension: a zero eigenvalue of A contributes the factor 1 - B(0) T on the right even though it is invisible in det (1 - T A).