English
There exist two polynomials i0,i1 with i0 ≠ i1 such that the difference of their residues modulo b is small in degree
Русский
Существуют два многочлена i0,i1, такие что разность их остатков по модулю b мала по степени.
LaTeX
$$∃ i0 ≠ i1, deg(A(i1) % b - A(i0) % b) < deg(b) · ε$$
Lean4
/-- If `A` is a family of enough low-degree polynomials over a finite field,
there is a pair of elements in `A` (with different indices but not necessarily
distinct), such that the difference of their remainders is close together. -/
theorem exists_approx_polynomial {b : Fq[X]} (hb : b ≠ 0) {ε : ℝ} (hε : 0 < ε)
(A : Fin (Fintype.card Fq ^ ⌈-log ε / log (Fintype.card Fq)⌉₊).succ → Fq[X]) :
∃ i₀ i₁, i₀ ≠ i₁ ∧ (cardPowDegree (A i₁ % b - A i₀ % b) : ℝ) < cardPowDegree b • ε :=
by
have hbε : 0 < cardPowDegree b • ε := by
rw [Algebra.smul_def, eq_intCast]
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
have one_lt_q : 1 < Fintype.card Fq := Fintype.one_lt_card
have one_lt_q' : (1 : ℝ) < Fintype.card Fq := by assumption_mod_cast
have q_pos : 0 < Fintype.card Fq := by omega
have q_pos' : (0 : ℝ) < Fintype.card Fq := by
assumption_mod_cast
-- If `b` is already small enough, then the remainders are equal and we are done.
by_cases le_b : b.natDegree ≤ ⌈-log ε / log (Fintype.card Fq)⌉₊
· obtain ⟨i₀, i₁, i_ne, mod_eq⟩ :=
exists_eq_polynomial le_rfl b le_b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb
refine ⟨i₀, i₁, i_ne, ?_⟩
rwa [mod_eq, sub_self, map_zero, Int.cast_zero]
-- Otherwise, it suffices to choose two elements whose difference is of small enough degree.
rw [not_le] at le_b
obtain ⟨i₀, i₁, i_ne, deg_lt⟩ :=
exists_approx_polynomial_aux le_rfl b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb
use i₀, i₁, i_ne
by_cases h : A i₁ % b = A i₀ % b
· rwa [h, sub_self, map_zero, Int.cast_zero]
have h' : A i₁ % b - A i₀ % b ≠ 0 := mt sub_eq_zero.mp h
suffices (natDegree (A i₁ % b - A i₀ % b) : ℝ) < b.natDegree + log ε / log (Fintype.card Fq) by
rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε, cardPowDegree_nonzero _ h',
cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast, Int.cast_pow, Int.cast_natCast, Int.cast_pow,
Int.cast_natCast, log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div, mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
-- And that result follows from manipulating the result from `exists_approx_polynomial_aux`
-- to turn the `-⌈-stuff⌉₊` into `+ stuff`.
apply lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
swap
· convert deg_lt
rw [degree_eq_natDegree h']; rfl
rw [← sub_neg_eq_add, ← neg_div, Nat.cast_sub le_b.le]
grw [← Nat.le_ceil]
