English
If you have a sufficiently large finite family of polynomials over a finite field and a nonzero polynomial b, there exist two indices i0,i1 such that the degree of A(i1) − A(i0) is bounded by d-1 relative to deg b.
Русский
Для достаточно большой конечной семейства многочленов над конечным полем и ненулевого b существует пара индексов, дающая ограничение на степень разности.
LaTeX
$$$\exists i_0,i_1, i_0 \neq i_1 \land \deg(A(i_1) - A(i_0)) < \deg(b) - d$ (в эквивалентной версии).$$
Lean4
/-- If `A` is a family of enough low-degree polynomials over a finite ring,
there is a pair of elements in `A` (with different indices but not necessarily
distinct), such that their difference has small degree. -/
theorem exists_approx_polynomial_aux [Ring Fq] {d : ℕ} {m : ℕ} (hm : Fintype.card Fq ^ d ≤ m) (b : Fq[X])
(A : Fin m.succ → Fq[X]) (hA : ∀ i, degree (A i) < degree b) :
∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(natDegree b - d) :=
by
have hb : b ≠ 0 := by
rintro rfl
specialize hA 0
rw [degree_zero] at hA
exact not_lt_of_ge bot_le hA
set f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (natDegree b - j.succ)
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
simpa using
lt_of_le_of_lt hm
(Nat.lt_succ_self m)
-- Therefore, the differences have all coefficients higher than `deg b - d` equal.
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
use i₀, i₁, i_ne
refine
(degree_lt_iff_coeff_zero _ _).mpr fun j hj =>
?_
-- The coefficients higher than `deg b` are the same because they are equal to 0.
by_cases hbj : degree b ≤ j
· refine coeff_eq_zero_of_degree_lt (lt_of_lt_of_le ?_ hbj)
exact
lt_of_le_of_lt (degree_sub_le _ _)
(max_lt (hA _) (hA _))
-- So we only need to look for the coefficients between `deg b - d` and `deg b`.
rw [coeff_sub, sub_eq_zero]
rw [not_le, degree_eq_natDegree hb] at hbj
have hbj : j < natDegree b := (@WithBot.coe_lt_coe _ _ _).mp hbj
have hj : natDegree b - j.succ < d := by
by_cases hd : natDegree b < d
· exact lt_of_le_of_lt tsub_le_self hd
· rw [not_lt] at hd
have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
rwa [tsub_lt_iff_tsub_lt hd hbj] at this
have : j = b.natDegree - (natDegree b - j.succ).succ := by
rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
convert congr_fun i_eq.symm ⟨natDegree b - j.succ, hj⟩
