# Admissible absolute values on polynomials #

This file defines an admissible absolute value Polynomial.cardPowDegreeIsAdmissible which we use to show the class number of the ring of integers of a function field is finite.

## Main results #

• Polynomial.cardPowDegreeIsAdmissible shows cardPowDegree, mapping p : Polynomial š½_q to q ^ degree p, is admissible
theorem Polynomial.exists_eq_polynomial {Fq : Type u_1} [Fintype Fq] [Semiring Fq] {d : ā} {m : ā} (hm : ^ d ā¤ m) (b : ) (hb : b.natDegree ā¤ d) (A : Fin m.succ ā ) (hA : ā (i : Fin m.succ), (A i).degree < b.degree) :
ā (iā : Fin m.succ) (iā : Fin m.succ), iā ā  iā ā§ A iā = A iā

If A is a family of enough low-degree polynomials over a finite semiring, there is a pair of equal elements in A.

theorem Polynomial.exists_approx_polynomial_aux {Fq : Type u_1} [Fintype Fq] [Ring Fq] {d : ā} {m : ā} (hm : ^ d ā¤ m) (b : ) (A : Fin m.succ ā ) (hA : ā (i : Fin m.succ), (A i).degree < b.degree) :
ā (iā : Fin m.succ) (iā : Fin m.succ), iā ā  iā ā§ (A iā - A iā).degree < ā(b.natDegree - d)

If A is a family of enough low-degree polynomials over a finite ring, there is a pair of elements in A (with different indices but not necessarily distinct), such that their difference has small degree.

theorem Polynomial.exists_approx_polynomial {Fq : Type u_1} [Fintype Fq] [Field Fq] {b : } (hb : b ā  0) {Īµ : ā} (hĪµ : 0 < Īµ) (A : Fin ( ^ ā-Īµ.log / (ā()).logāā).succ ā ) :
ā (iā : Fin ( ^ ā-Īµ.log / (ā()).logāā).succ) (iā : Fin ( ^ ā-Īµ.log / (ā()).logāā).succ), iā ā  iā ā§ ā(Polynomial.cardPowDegree (A iā % b - A iā % b)) < Polynomial.cardPowDegree b ā¢ Īµ

If A is a family of enough low-degree polynomials over a finite field, there is a pair of elements in A (with different indices but not necessarily distinct), such that the difference of their remainders is close together.

theorem Polynomial.cardPowDegree_anti_archimedean {Fq : Type u_1} [Fintype Fq] [Field Fq] {x : } {y : } {z : } {a : ā¤} (hxy : Polynomial.cardPowDegree (x - y) < a) (hyz : Polynomial.cardPowDegree (y - z) < a) :
Polynomial.cardPowDegree (x - z) < a

If x is close to y and y is close to z, then x and z are at least as close.

theorem Polynomial.exists_partition_polynomial_aux {Fq : Type u_1} [Fintype Fq] [Field Fq] (n : ā) {Īµ : ā} (hĪµ : 0 < Īµ) {b : } (hb : b ā  0) (A : Fin n ā ) :
ā (t : Fin n ā Fin ( ^ ā-Īµ.log / (ā()).logāā)), ā (iā iā : Fin n), t iā = t iā ā ā(Polynomial.cardPowDegree (A iā % b - A iā % b)) < Polynomial.cardPowDegree b ā¢ Īµ

A slightly stronger version of exists_partition on which we perform induction on n: for all Īµ > 0, we can partition the remainders of any family of polynomials A into equivalence classes, where the equivalence(!) relation is "closer than Īµ".

theorem Polynomial.exists_partition_polynomial {Fq : Type u_1} [Fintype Fq] [Field Fq] (n : ā) {Īµ : ā} (hĪµ : 0 < Īµ) {b : } (hb : b ā  0) (A : Fin n ā ) :
ā (t : Fin n ā Fin ( ^ ā-Īµ.log / (ā()).logāā)), ā (iā iā : Fin n), t iā = t iā ā ā(Polynomial.cardPowDegree (A iā % b - A iā % b)) < Polynomial.cardPowDegree b ā¢ Īµ

For all Īµ > 0, we can partition the remainders of any family of polynomials A into classes, where all remainders in a class are close together.

noncomputable def Polynomial.cardPowDegreeIsAdmissible {Fq : Type u_1} [Fintype Fq] [Field Fq] :
fun p => Fintype.card Fq ^ degree p is an admissible absolute value. We set q ^ degree 0 = 0.