Admissible absolute values on polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

polynomial.card_pow_degree_is_admissible shows card_pow_degree, mapping p : polynomial 𝔽_q to q ^ degree p, is admissible

source

theorem polynomial.exists_eq_polynomial {Fq : Type u_1} [fintype Fq] [semiring Fq] {d m : ℕ} (hm : fintype.card Fq ^ d ≤ m) (b : polynomial Fq) (hb : b.nat_degree ≤ d) (A : fin m.succ → polynomial Fq) (hA : ∀ (i : fin m.succ), (A i).degree < b.degree) :

∃ (i₀ 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.

source

theorem polynomial.exists_approx_polynomial_aux {Fq : Type u_1} [fintype Fq] [ring Fq] {d m : ℕ} (hm : fintype.card Fq ^ d ≤ m) (b : polynomial Fq) (A : fin m.succ → polynomial Fq) (hA : ∀ (i : fin m.succ), (A i).degree < b.degree) :

∃ (i₀ i₁ : fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.nat_degree - 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.

source

theorem polynomial.exists_approx_polynomial {Fq : Type u_1} [fintype Fq] [field Fq] {b : polynomial Fq} (hb : b ≠ 0) {ε : ℝ} (hε : 0 < ε) (A : fin (fintype.card Fq ^ ⌈-real.log ε / real.log ↑(fintype.card Fq)⌉₊).succ → polynomial Fq) :

∃ (i₀ i₁ : fin (fintype.card Fq ^ ⌈-real.log ε / real.log ↑(fintype.card Fq)⌉₊).succ), i₀ ≠ i₁ ∧ ↑(⇑polynomial.card_pow_degree (A i₁ % b - A i₀ % b)) < ⇑polynomial.card_pow_degree 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.

source

theorem polynomial.card_pow_degree_anti_archimedean {Fq : Type u_1} [fintype Fq] [field Fq] {x y z : polynomial Fq} {a : ℤ} (hxy : ⇑polynomial.card_pow_degree (x - y) < a) (hyz : ⇑polynomial.card_pow_degree (y - z) < a) :

⇑polynomial.card_pow_degree (x - z) < a

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

source

theorem polynomial.exists_partition_polynomial_aux {Fq : Type u_1} [fintype Fq] [field Fq] (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : polynomial Fq} (hb : b ≠ 0) (A : fin n → polynomial Fq) :

∃ (t : fin n → fin (fintype.card Fq ^ ⌈-real.log ε / real.log ↑(fintype.card Fq)⌉₊)), ∀ (i₀ i₁ : fin n), t i₀ = t i₁ ↔ ↑(⇑polynomial.card_pow_degree (A i₁ % b - A i₀ % b)) < ⇑polynomial.card_pow_degree 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 ε".

source

theorem polynomial.exists_partition_polynomial {Fq : Type u_1} [fintype Fq] [field Fq] (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : polynomial Fq} (hb : b ≠ 0) (A : fin n → polynomial Fq) :

∃ (t : fin n → fin (fintype.card Fq ^ ⌈-real.log ε / real.log ↑(fintype.card Fq)⌉₊)), ∀ (i₀ i₁ : fin n), t i₀ = t i₁ → ↑(⇑polynomial.card_pow_degree (A i₁ % b - A i₀ % b)) < ⇑polynomial.card_pow_degree 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.

source

noncomputable def polynomial.card_pow_degree_is_admissible {Fq : Type u_1} [fintype Fq] [field Fq] :

polynomial.card_pow_degree.is_admissible

λ p, fintype.card Fq ^ degree p is an admissible absolute value. We set q ^ degree 0 = 0.

Equations

polynomial.card_pow_degree_is_admissible = {to_is_euclidean := _, card := λ (ε : ℝ), fintype.card Fq ^ ⌈-real.log ε / real.log ↑(fintype.card Fq)⌉₊, exists_partition' := _}