Polynomial.exists_partition_polynomial
theorem Polynomial.exists_partition_polynomial :
∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] (n : ℕ) {ε : ℝ},
0 < ε →
∀ {b : Polynomial Fq},
b ≠ 0 →
∀ (A : Fin n → Polynomial Fq),
∃ t,
∀ (i₀ i₁ : Fin n),
t i₀ = t i₁ → ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
This theorem states that, given any positive real number `ε`, and for any non-zero polynomial `b` in a finite field `Fq`, we can partition the remainders of any family of polynomials `A` (indexed by elements of `Fin n`) into classes, such that all remainders in a class are "close together". Here "close together" means that if two indices `i₀` and `i₁` belong to the same class (i.e., `t i₀ = t i₁`), then the absolute value (as defined by the function `cardPowDegree`) of the difference of the remainders of `A i₁` and `A i₀` when divided by `b`, is less than `ε` times the `cardPowDegree` of `b`. This partitioning `t` depends on the polynomials `A` and the number `ε`.
More concisely: Given any positive real number `ε` and a finite field `Fq`, there exists a partition `t` of the remainders of any family `A` of polynomials over `Fq` such that for all indices `i₀` and `i₁` in the same class, the absolute value of the difference quotient of `A i₁` and `A i₀` modulo `b` is less than `ε` times the degree of `b`.
|
Polynomial.exists_approx_polynomial
theorem Polynomial.exists_approx_polynomial :
∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] {b : Polynomial Fq},
b ≠ 0 →
∀ {ε : ℝ},
0 < ε →
∀ (A : Fin (Fintype.card Fq ^ ⌈-ε.log / (↑(Fintype.card Fq)).log⌉₊).succ → Polynomial Fq),
∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
This theorem states that given a finite field `Fq` and a non-zero polynomial `b` over `Fq`, for any positive real number `ε`, if we have a family of polynomials `A` that has more elements than the size of the field raised to the ceiling of the negative logarithm of `ε` divided by the logarithm of the size of the field, there exist two polynomials in `A` (not necessarily distinct but with different indices) such that the absolute value of the difference of their remainders when divided by `b`, raised to the power of the size of the field (`Fq`), is less than `ε` times the absolute value of `b` raised to the power of the size of the field. In other words, the theorem asserts that in a large enough family of low-degree polynomials over a finite field, it's possible to find two polynomials whose remainders, when divided by a given non-zero polynomial, are close together.
More concisely: Given a finite field `Fq`, a non-zero polynomial `b`, and a positive real number `ε`, if `A` is a family of polynomials over `Fq` with more elements than the size of `Fq` raised to the ceiling of `- log(ε) / log(|Fq|)`, then there exist two polynomials in `A` whose remainders, when divided by `b`, differ by less than `ε * |b|^|Fq|` when reduced modulo `|Fq|`.
|
Polynomial.cardPowDegree_anti_archimedean
theorem Polynomial.cardPowDegree_anti_archimedean :
∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] {x y z : Polynomial Fq} {a : ℤ},
Polynomial.cardPowDegree (x - y) < a →
Polynomial.cardPowDegree (y - z) < a → Polynomial.cardPowDegree (x - z) < a
The theorem `Polynomial.cardPowDegree_anti_archimedean` states that for any finite field `Fq` and any three polynomials `x`, `y`, `z` over `Fq` with an integer `a`, if `x` is "close" to `y` and `y` is "close" to `z` (where "closeness" is measured by the function `Polynomial.cardPowDegree` being less than `a`), then `x` is at least as "close" to `z` (again, with closeness measured by `Polynomial.cardPowDegree` being less than `a`). This is essentially a version of the triangle inequality expressed in terms of the `cardPowDegree` absolute value on the ring of polynomials over a finite field.
More concisely: For any finite field `Fq` and polynomials `x`, `y`, `z` over `Fq` and integer `a`, if `Polynomial.cardPowDegree(x - y)` and `Polynomial.cardPowDegree(y - z)` are both less than `a`, then `Polynomial.cardPowDegree(x - z)` is also less than `a`.
|
Polynomial.exists_approx_polynomial_aux
theorem Polynomial.exists_approx_polynomial_aux :
∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Ring Fq] {d m : ℕ},
Fintype.card Fq ^ d ≤ m →
∀ (b : Polynomial Fq) (A : Fin m.succ → Polynomial Fq),
(∀ (i : Fin m.succ), (A i).degree < b.degree) →
∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
This theorem states that, given a finite ring `Fq` and a family `A` of `m.succ` number of polynomials over `Fq`, each of which has a degree less than a certain polynomial `b`, there exists a pair of polynomials in `A` (with different indices) such that the degree of their difference is less than the difference between the degree of `b` and `d`. This is true provided that `d` is sufficiently large, specifically, it should be such that the number of elements in `Fq` raised to the power `d` is less than or equal to `m`.
More concisely: Given a finite ring `Fq`, a family `A` of `m.succ` polynomials over `Fq` of degree less than a polynomial `b`, and a integer `d` such that `|Fq|^d <= m`, there exist distinct indices `i` and `j` in `A` with degree of `A[i] - A[j]` less than `degree b - d`.
|
Polynomial.exists_partition_polynomial_aux
theorem Polynomial.exists_partition_polynomial_aux :
∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] (n : ℕ) {ε : ℝ},
0 < ε →
∀ {b : Polynomial Fq},
b ≠ 0 →
∀ (A : Fin n → Polynomial Fq),
∃ t,
∀ (i₀ i₁ : Fin n),
t i₀ = t i₁ ↔ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
The theorem `Polynomial.exists_partition_polynomial_aux` states that for any positive real number `ε`, there exists a partition of the remainders of a family of polynomials `A` in a finite field `Fq` into equivalence classes, where the equivalence relation is "closer than `ε`". Here, "closer" is defined with respect to the function `Polynomial.cardPowDegree`, which sends a polynomial to the card number of `Fq` raised to the degree of the polynomial, effectively measuring the size of a polynomial. The theorem stipulates this property for all non-zero polynomials `b` and all families `A` of polynomials, indexed by natural numbers less than some fixed `n`. The partition is represented by a function `t` that assigns to each index an equivalence class, such that two indices have the same class if and only if the absolute value of the difference of their corresponding polynomials' remainders when divided by `b`, as measured by `Polynomial.cardPowDegree`, is less than `ε` times the value of `Polynomial.cardPowDegree b`.
More concisely: For any positive real number ε and finite field Fq, there exists a partition of the remainders of a family of non-zero polynomials in Fq, indexed by natural numbers less than some fixed n, into equivalence classes using an equivalence relation defined by the absolute value of the difference of polynomial remainders being less than ε times the cardinality raised to the degree of the polynomial.
|
Polynomial.exists_eq_polynomial
theorem Polynomial.exists_eq_polynomial :
∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Semiring Fq] {d m : ℕ},
Fintype.card Fq ^ d ≤ m →
∀ (b : Polynomial Fq),
b.natDegree ≤ d →
∀ (A : Fin m.succ → Polynomial Fq),
(∀ (i : Fin m.succ), (A i).degree < b.degree) → ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
This theorem states that if `Fq` is a finite semiring and `A` is a family of polynomials over `Fq` such that the number of elements of `Fq` raised to the power of degree `d` is less than or equal to `m`, and we have a polynomial `b` with natural degree less than or equal to `d`, then for every polynomial `A` in `Fin m.succ`, where each polynomial's degree is less than the degree of `b`, there exists two distinct indices `i₀` and `i₁` such that the polynomials at these indices in `A` are equal. In other words, in a large enough family of low-degree polynomials over a finite semiring, there will be a pair of equal polynomials.
More concisely: Given a finite semiring `Fq` and a family `A` of polynomials over `Fq` of degree less than or equal to `d` such that the number of elements of `Fq` raised to the power of degree `d` is less than or equal to `m`, there exist distinct indices `i0` and `i1` such that the polynomials at `i0` and `i1` in `A` are equal.
|