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.