English
An inductive strengthening of partitioning polynomials into classes where closeness is controlled by ε.
Русский
Индуктивно усиливается разбиение многочленов по классам с контролируемым близостью по ε.
LaTeX
$$exists_partition_polynomial_aux n ε b A$$
Lean4
/-- A slightly stronger version of `exists_partition` on which we perform induction on `n`:
for all `ε > 0`, we can partition the remainders of any family of polynomials `A`
into equivalence classes, where the equivalence(!) relation is "closer than `ε`". -/
theorem exists_partition_polynomial_aux (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
have hbε : 0 < cardPowDegree b • ε := by
rw [Algebra.smul_def, eq_intCast]
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
induction n with
| zero => refine ⟨finZeroElim, finZeroElim⟩
| succ n ih =>
-- Show `anti_archimedean` also holds for real distances.
have anti_archim' :
∀ {i j k} {ε : ℝ},
(cardPowDegree (A i % b - A j % b) : ℝ) < ε →
(cardPowDegree (A j % b - A k % b) : ℝ) < ε → (cardPowDegree (A i % b - A k % b) : ℝ) < ε :=
by
intro i j k ε
simp_rw [← Int.lt_ceil]
exact cardPowDegree_anti_archimedean
obtain ⟨t', ht'⟩ :=
ih
(Fin.tail A)
-- We got rid of `A 0`, so determine the index `j` of the partition we'll re-add it to.
rsuffices ⟨j, hj⟩ : ∃ j, ∀ i, t' i = j ↔ (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε
· refine ⟨Fin.cons j t', fun i₀ i₁ => ?_⟩
refine Fin.cases ?_ (fun i₀ => ?_) i₀ <;> refine Fin.cases ?_ (fun i₁ => ?_) i₁
· simpa using hbε
· rw [Fin.cons_succ, Fin.cons_zero, eq_comm, AbsoluteValue.map_sub]
exact hj i₁
· rw [Fin.cons_succ, Fin.cons_zero]
exact hj i₀
· rw [Fin.cons_succ, Fin.cons_succ]
exact ht' i₀ i₁
obtain ⟨j, hj⟩ : ∃ j, ∀ i : Fin n, t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε :=
by
by_contra! hg
obtain ⟨j₀, j₁, j_ne, approx⟩ :=
exists_approx_polynomial hb hε (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))
revert j_ne approx
refine Fin.cases ?_ (fun j₀ => ?_) j₀ <;> refine Fin.cases (fun j_ne approx => ?_) (fun j₁ j_ne approx => ?_) j₁
· exact absurd rfl j_ne
· rw [Fin.cons_succ, Fin.cons_zero, ← not_le, AbsoluteValue.map_sub] at approx
have := (Classical.choose_spec (hg j₁)).2
contradiction
· rw [Fin.cons_succ, Fin.cons_zero, ← not_le] at approx
have := (Classical.choose_spec (hg j₀)).2
contradiction
· rw [Fin.cons_succ, Fin.cons_succ] at approx
rw [Ne, Fin.succ_inj] at j_ne
have : j₀ = j₁ :=
(Classical.choose_spec (hg j₀)).1.symm.trans
(((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans
(Classical.choose_spec (hg j₁)).1)
contradiction
-- However, if one of those partitions `j` is inhabited by some `i`, then this `j` works.
by_cases exists_nonempty_j :
∃ j, (∃ i, t' i = j) ∧ ∀ i, t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε
· obtain ⟨j, ⟨i, hi⟩, hj⟩ := exists_nonempty_j
refine ⟨j, fun i' => ⟨hj i', fun hi' => _root_.trans ((ht' _ _).mpr ?_) hi⟩⟩
apply anti_archim' _ hi'
rw [AbsoluteValue.map_sub]
exact hj _ hi
refine ⟨j, fun i => ⟨hj i, fun hi => ?_⟩⟩
have := exists_nonempty_j ⟨t' i, ⟨i, rfl⟩, fun i' hi' => anti_archim' hi ((ht' _ _).mp hi')⟩
contradiction
