# Documentation

This file defines a structure AbsoluteValue.IsAdmissible which we use to show the class number of the ring of integers of a global field is finite.

## Main definitions #

• AbsoluteValue.IsAdmissible abv states the absolute value abv : R ā ā¤ respects the Euclidean domain structure on R, and that a large enough set of elements of R^n contains a pair of elements whose remainders are pointwise close together.

## Main results #

• AbsoluteValue.absIsAdmissible shows the "standard" absolute value on ā¤, mapping negative x to -x, is admissible.
• Polynomial.cardPowDegreeIsAdmissible shows cardPowDegree, mapping p : Polynomial š½_q to q ^ degree p, is admissible
structure AbsoluteValue.IsAdmissible {R : Type u_1} [] (abv : ) extends :

An absolute value R ā ā¤ is admissible if it respects the Euclidean domain structure and a large enough set of elements in R^n will contain a pair of elements whose remainders are pointwise close together.

• map_lt_map_iff' : ā {x y : R}, abv x < abv y ā
• card : ā ā ā
• exists_partition' : ā (n : ā) {Īµ : ā}, 0 < Īµ ā ā {b : R}, b ā  0 ā ā (A : Fin n ā R), ā (t : Fin n ā Fin (self.card Īµ)), ā (iā iā : Fin n), t iā = t iā ā ā(abv (A iā % b - A iā % b)) < abv b ā¢ Īµ

For all Īµ > 0 and finite families A, we can partition the remainders of A mod b into abv.card Īµ sets, such that all elements in each part of remainders are close together.

Instances For
theorem AbsoluteValue.IsAdmissible.exists_partition' {R : Type u_1} [] {abv : } (self : abv.IsAdmissible) (n : ā) {Īµ : ā} :
0 < Īµ ā ā {b : R}, b ā  0 ā ā (A : Fin n ā R), ā (t : Fin n ā Fin (self.card Īµ)), ā (iā iā : Fin n), t iā = t iā ā ā(abv (A iā % b - A iā % b)) < abv b ā¢ Īµ

For all Īµ > 0 and finite families A, we can partition the remainders of A mod b into abv.card Īµ sets, such that all elements in each part of remainders are close together.

theorem AbsoluteValue.IsAdmissible.exists_partition {R : Type u_1} [] {abv : } {Ī¹ : Type u_2} [Finite Ī¹] {Īµ : ā} (hĪµ : 0 < Īµ) {b : R} (hb : b ā  0) (A : Ī¹ ā R) (h : abv.IsAdmissible) :
ā (t : Ī¹ ā Fin (h.card Īµ)), ā (iā iā : Ī¹), t iā = t iā ā ā(abv (A iā % b - A iā % b)) < abv b ā¢ Īµ

For all Īµ > 0 and finite families A, we can partition the remainders of A mod b into abv.card Īµ sets, such that all elements in each part of remainders are close together.

theorem AbsoluteValue.IsAdmissible.exists_approx_aux {R : Type u_1} [] {abv : } (n : ā) (h : abv.IsAdmissible) {Īµ : ā} (_hĪµ : 0 < Īµ) {b : R} (_hb : b ā  0) (A : Fin (h.card Īµ ^ n).succ ā Fin n ā R) :
ā (iā : Fin (h.card Īµ ^ n).succ) (iā : Fin (h.card Īµ ^ n).succ), iā ā  iā ā§ ā (k : Fin n), ā(abv (A iā k % b - A iā k % b)) < abv b ā¢ Īµ

Any large enough family of vectors in R^n has a pair of elements whose remainders are close together, pointwise.

theorem AbsoluteValue.IsAdmissible.exists_approx {R : Type u_1} [] {abv : } {Ī¹ : Type u_2} [Fintype Ī¹] {Īµ : ā} (hĪµ : 0 < Īµ) {b : R} (hb : b ā  0) (h : abv.IsAdmissible) (A : Fin (h.card Īµ ^ ).succ ā Ī¹ ā R) :
ā (iā : Fin (h.card Īµ ^ ).succ) (iā : Fin (h.card Īµ ^ ).succ), iā ā  iā ā§ ā (k : Ī¹), ā(abv (A iā k % b - A iā k % b)) < abv b ā¢ Īµ

Any large enough family of vectors in R^Ī¹ has a pair of elements whose remainders are close together, pointwise.