Admissible absolute values #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines a structure absolute_value.is_admissible which we use to show the class number of the ring of integers of a global field is finite.

Main definitions #

absolute_value.is_admissible 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 #

absolute_value.abs_is_admissible shows the "standard" absolute value on ℤ, mapping negative x to -x, is admissible.
polynomial.card_pow_degree_is_admissible shows card_pow_degree, mapping p : polynomial 𝔽_q to q ^ degree p, is admissible

source

structure absolute_value.is_admissible {R : Type u_1} [euclidean_domain R] (abv : absolute_value R ℤ) :

Type

to_is_euclidean : abv.is_euclidean
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 • ε

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 absolute_value.is_admissible

absolute_value.is_admissible.has_sizeof_inst
absolute_value.is_admissible.inhabited

source

theorem absolute_value.is_admissible.exists_partition {R : Type u_1} [euclidean_domain R] {abv : absolute_value R ℤ} {ι : Type u_2} [fintype ι] {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0) (A : ι → R) (h : abv.is_admissible) :

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

source

theorem absolute_value.is_admissible.exists_approx_aux {R : Type u_1} [euclidean_domain R] {abv : absolute_value R ℤ} (n : ℕ) (h : abv.is_admissible) {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0) (A : fin (h.card ε ^ n).succ → fin n → R) :

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

source

theorem absolute_value.is_admissible.exists_approx {R : Type u_1} [euclidean_domain R] {abv : absolute_value R ℤ} {ι : Type u_2} [fintype ι] {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0) (h : abv.is_admissible) (A : fin (h.card ε ^ fintype.card ι).succ → ι → R) :

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