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 #

  • card :
  • 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.

    exists_partition' : ∀ (n : ) {ε : }, 0 < ε∀ {b : R}, b 0∀ (A : Fin nR), t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁↑(abv (A i₁ % b - A i₀ % b)) < abv b ε

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.

Instances For
    theorem AbsoluteValue.IsAdmissible.exists_partition {R : Type u_2} [inst : EuclideanDomain R] {abv : AbsoluteValue R } {ι : Type u_1} [inst : Fintype ι] {ε : } (hε : 0 < ε) {b : R} (hb : b 0) (A : ιR) (h : AbsoluteValue.IsAdmissible abv) :
    t, ∀ (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} [inst : EuclideanDomain R] {abv : AbsoluteValue R } (n : ) (h : AbsoluteValue.IsAdmissible abv) {ε : } (_hε : 0 < ε) {b : R} (_hb : b 0) (A : Fin (Nat.succ (AbsoluteValue.IsAdmissible.card h ε ^ n))Fin nR) :
    i₀ i₁, 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_2} [inst : EuclideanDomain R] {abv : AbsoluteValue R } {ι : Type u_1} [inst : Fintype ι] {ε : } (hε : 0 < ε) {b : R} (hb : b 0) (h : AbsoluteValue.IsAdmissible abv) (A : Fin (Nat.succ (AbsoluteValue.IsAdmissible.card h ε ^ Fintype.card ι))ιR) :
    i₀ i₁, 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.