English
Assume Algebra Is Algebraic over R. For any a ∈ S and any nonzero b ∈ R, there exist q ∈ S and r ∈ finsetApprox(b_S, adm) such that the absolute value of the norm of r·a − b·q is strictly smaller than the absolute value of the norm of algebraMap_R^S(b).
Русский
Пусть S — кольцевая оболочка, удовлетворяющая условию алгебраичности. Для любого a ∈ S и любого ненулевого b ∈ R существуют q ∈ S и r ∈ finsetApprox(b_S, adm), такие что модуль нормы элемента r·a − b·q меньше модуля нормы алгебраического отображения b.
LaTeX
$$$ \\exists q \\in S,\\ \\exists r \\in \\mathrm{finsetApprox}(b_S, adm),\\ abv(\\mathrm{Algebra.norm}_R(r \\cdot a - b \\cdot q)) < abv(\\mathrm{Algebra.norm}_R(\\mathrm{algebraMap}_R S\\, b)) $$$
Lean4
/-- We can approximate `a / b : L` with `q / r`, where `r` has finitely many options for `L`. -/
theorem exists_mem_finsetApprox (a : S) {b} (hb : b ≠ (0 : R)) :
∃ q : S,
∃ r ∈ finsetApprox bS adm, abv (Algebra.norm R (r • a - b • q)) < abv (Algebra.norm R (algebraMap R S b)) :=
by
have dim_pos := Fintype.card_pos_iff.mpr bS.index_nonempty
set ε : ℝ := normBound abv bS ^ (-1 / Fintype.card ι : ℝ) with ε_eq
have hε : 0 < ε := Real.rpow_pos_of_pos (Int.cast_pos.mpr (normBound_pos abv bS)) _
have ε_le : (normBound abv bS : ℝ) * (abv b • ε) ^ (Fintype.card ι : ℝ) ≤ abv b ^ (Fintype.card ι : ℝ) :=
by
have := normBound_pos abv bS
have := abv.nonneg b
rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one, mul_left_comm,
mul_inv_cancel₀, mul_one, rpow_natCast] <;>
try norm_cast; cutsat
· exact Iff.mpr Int.cast_nonneg this
· linarith
set μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
let s : ι →₀ R := bS.repr a
have s_eq : ∀ i, s i = bS.repr a i := fun i => rfl
let qs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i / b
let rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b
have r_eq : ∀ j i, rs j i = μ j * s i % b := fun i j => rfl
have μ_eq : ∀ i j, μ j * s i = b * qs j i + rs j i := by
intro i j
rw [r_eq, EuclideanDomain.div_add_mod]
have μ_mul_a_eq : ∀ j, μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i :=
by
intro j
rw [← bS.sum_repr a]
simp only [μ, qs, rs, Finset.smul_sum, ← Finset.sum_add_distrib]
refine Finset.sum_congr rfl fun i _ => ?_
rw [← s_eq, ← mul_smul, μ_eq, add_smul, mul_smul, ← μ_eq]
obtain ⟨j, k, j_ne_k, hjk⟩ := adm.exists_approx hε hb fun j i => μ j * s i
have hjk' : ∀ i, (abv (rs k i - rs j i) : ℝ) < abv b • ε := by simpa only [r_eq] using hjk
let q := ∑ i, (qs k i - qs j i) • bS i
set r := μ k - μ j with r_eq
refine ⟨q, r, (mem_finsetApprox bS adm).mpr ?_, ?_⟩
· exact ⟨k, j, j_ne_k.symm, rfl⟩
have : r • a - b • q = ∑ x : ι, (rs k x • bS x - rs j x • bS x) :=
by
simp only [q, r_eq, sub_smul, μ_mul_a_eq, Finset.smul_sum, ← Finset.sum_add_distrib, ← Finset.sum_sub_distrib,
smul_sub]
refine Finset.sum_congr rfl fun x _ => ?_
ring
rw [this, Algebra.norm_algebraMap_of_basis bS, abv.map_pow]
refine Int.cast_lt.mp ((norm_lt abv bS _ fun i => lt_of_le_of_lt ?_ (hjk' i)).trans_le ?_)
· apply le_of_eq
congr
simp_rw [map_sum, map_sub, map_smul, Finset.sum_apply', Finsupp.sub_apply, Finsupp.smul_apply,
Finset.sum_sub_distrib, Basis.repr_self_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq', Finset.mem_univ,
if_true]
· exact mod_cast ε_le
