AbsoluteValue.IsAdmissible.exists_partition
theorem AbsoluteValue.IsAdmissible.exists_partition :
∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type u_2} [inst_1 : Finite ι] {ε : ℝ},
0 < ε →
∀ {b : R},
b ≠ 0 →
∀ (A : ι → R) (h : abv.IsAdmissible),
∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
This theorem states that for any positive real number `ε` and any finite family `A` of elements from a Euclidean domain `R`, given a non-zero element `b` from `R` and an admissible absolute value `abv` from `R` to integers, it is possible to partition the remainders of `A` modulo `b` into `abv.card ε` sets in such a way that all elements in each partitioned set of remainders are close to each other. In other words, for any two elements `i₀` and `i₁` from the same partition, the absolute value of the difference of their remainders when divided by `b` is less than `ε` times the absolute value of `b`.
More concisely: Given a Euclidean domain R with absolute value abv, for any positive real ε, finite subset A of R, and non-zero b in R, there exists a partition of A modulo b with the property that for all i₀, i₁ in the same partition, |(a₀ mod b) - (a₁ mod b)| < ε * |b|.
|
AbsoluteValue.IsAdmissible.exists_approx
theorem AbsoluteValue.IsAdmissible.exists_approx :
∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} {ι : Type u_2} [inst_1 : Fintype ι] {ε : ℝ},
0 < ε →
∀ {b : R},
b ≠ 0 →
∀ (h : abv.IsAdmissible) (A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R),
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
The theorem `AbsoluteValue.IsAdmissible.exists_approx` states that for any Euclidean domain `R`, any absolute value `abv` from `R` to integers `ℤ`, any finite type `ι`, and any real number `ε` greater than 0, given any non-zero element `b` in `R`, if `abv` is admissible, for every function `A` mapping from the successor of the cardinality of `ε` to the power of the cardinality of `ι` to a function from `ι` to `R`, there exist two distinct indices `i₀` and `i₁` such that for every `k` in `ι`, the absolute value of the difference of the remainders when `A i₁ k` and `A i₀ k` are divided by `b` is less than `ε` times the absolute value of `b`. In simpler terms, this theorem guarantees that in any large enough collection of vectors in `R^ι`, there exists a pair whose remainders, when divided by `b`, are close to each other.
More concisely: For any Euclidean domain R, admissible absolute value abv from R to ℤ, finite type ι, and real number ε > 0, given a function A from the successor of the cardinality of ε to the power of the cardinality of ι to ι → R, there exist distinct indices i₀ and i₁ such that |A i₁ k - A i₀ k| / |b| < ε for all k in ι.
|
AbsoluteValue.IsAdmissible.exists_approx_aux
theorem AbsoluteValue.IsAdmissible.exists_approx_aux :
∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (n : ℕ) (h : abv.IsAdmissible) {ε : ℝ},
0 < ε →
∀ {b : R},
b ≠ 0 →
∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
This theorem states that for any euclidean domain `R`, absolute value `abv` from `R` to the integers, positive real number ε, non-zero element `b` of `R`, and function `A` from finite set of size `(h.card ε ^ n).succ` to `R`, where `h` is an admissible absolute value, there exist two distinct indices `i₀` and `i₁` such that for every index `k` in the finite set `Fin n`, the absolute value of the difference of the remainders of `A i₁ k` and `A i₀ k` when divided by `b`, scaled by the absolute value of `b` times ε, is less than `abv b • ε`. In simpler terms, given a large enough set of vectors in `R^n`, we can always find two vectors whose remainders, when divided by a non-zero element, are close together in every component.
More concisely: Given an Euclidean domain `R` with admissible absolute value `abv`, for any positive real number `ε` and non-zero element `b`, there exist distinct indices `i₀` and `i₁` such that the absolute values of the differences of `A(i₁) k` and `A(i₀) k`, scaled by `abv b • ε`, are less than `abv b` for all `k` in the finite set `Fin n`.
|
AbsoluteValue.IsAdmissible.exists_partition'
theorem AbsoluteValue.IsAdmissible.exists_partition' :
∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (self : abv.IsAdmissible) (n : ℕ) {ε : ℝ},
0 < ε →
∀ {b : R},
b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
For any real number `ε > 0` and a finite family `A` of elements of a Euclidean Domain `R`, this theorem states that if `b` is a non-zero element of `R` and `abv` is an admissible absolute value on `R`, we can partition the remainders of the elements of `A` modulo `b` into `abv.card ε` sets, in such a way that for any two indices `i₀` and `i₁` in the finite family `A`, if they belong to the same set in the partition, the absolute value of the difference of their remainders modulo `b` is less than ε times the absolute value of `b`.
More concisely: For any Euclidean Domain `R` with an admissible absolute value `abv`, given a finite set `A` of elements in `R`, a non-zero element `b` in `R`, and a real number `ε > 0`, there exists a partition of the remainders of `A` modulo `b` such that the absolute value of the difference of remainders for any two elements in the same partition is less than `ε * |b|`.
|