English
There exists a partition of a finite family of polynomials into classes such that the variation of residues modulo b within a class is bounded by ε.
Русский
Существует разбиение конечной семейства многочленов на классы так, что вариация остатков в классе ограничена ε.
LaTeX
$$$\exists t: Fin n \to Fin (|F_q|^{\lceil -\log \varepsilon / \log |F_q| \rceil_+}),\; \forall i_0,i_1, t i_0 = t i_1 \Rightarrow (cardPowDegree(A i_1 \% b - A i_0 \% b) : \mathbb{R}) < cardPowDegree b · \varepsilon$$$
Lean4
/-- For all `ε > 0`, we can partition the remainders of any family of polynomials `A`
into classes, where all remainders in a class are close together. -/
theorem exists_partition_polynomial (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : Fq[X]} (hb : b ≠ 0) (A : Fin n → Fq[X]) :
∃ t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (Fintype.card Fq)⌉₊),
∀ i₀ i₁ : Fin n, t i₀ = t i₁ → (cardPowDegree (A i₁ % b - A i₀ % b) : ℝ) < cardPowDegree b • ε :=
by
obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A
exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩
