Documentation

Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Admissible absolute values #

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 #

Main results #

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 ā†” EuclideanDomain.r x 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} [EuclideanDomain R] {abv : AbsoluteValue R ā„¤} (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} [EuclideanDomain R] {abv : AbsoluteValue R ā„¤} {Ī¹ : 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} [EuclideanDomain R] {abv : AbsoluteValue R ā„¤} (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} [EuclideanDomain R] {abv : AbsoluteValue R ā„¤} {Ī¹ : Type u_2} [Fintype Ī¹] {Īµ : ā„} (hĪµ : 0 < Īµ) {b : R} (hb : b ā‰  0) (h : abv.IsAdmissible) (A : Fin (h.card Īµ ^ Fintype.card Ī¹).succ ā†’ Ī¹ ā†’ R) :
    āˆƒ (iā‚€ : Fin (h.card Īµ ^ Fintype.card Ī¹).succ) (iā‚ : Fin (h.card Īµ ^ Fintype.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.