English
Another variant: for a given F and bound η there is a polynomial P with valuation dominated by η.
Русский
Ещё одно: для данного F и границы η существует многочлен P с валюацией, ограниченной η.
LaTeX
$$$\exists P : K[X], (PowerSeries.idealX K).intValuation (F - P) < η$$$
Lean4
theorem exists_Polynomial_intValuation_lt (F : K⟦X⟧) (η : ℤᵐ⁰ˣ) :
∃ P : K[X], (PowerSeries.idealX K).intValuation (F - P) < η :=
by
by_cases h_neg : 1 < η
· use 0
simpa using (intValuation_le_one (PowerSeries.idealX K) F).trans_lt h_neg
· rw [not_lt, ← Units.val_le_val, Units.val_one, ← WithZero.coe_one, ← coe_unzero η.ne_zero, coe_le_coe, ←
Multiplicative.toAdd_le, toAdd_one] at h_neg
obtain ⟨d, hd⟩ := Int.exists_eq_neg_ofNat h_neg
use F.trunc (d + 1)
have : Valued.v ((ofPowerSeries ℤ K) (F - (trunc (d + 1) F))) ≤ (Multiplicative.ofAdd (-(d + 1 : ℤ))) :=
by
apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr
simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using fun _ h ↦ (if_pos h).symm
rw [neg_add, ofAdd_add, ← hd, ofAdd_toAdd, WithZero.coe_mul, coe_unzero, ← coe_algebraMap] at this
rw [← valuation_of_algebraMap (K := K⸨X⸩) (PowerSeries.idealX K) (F - F.trunc (d + 1))]
apply lt_of_le_of_lt this
rw [← mul_one (η : ℤᵐ⁰), mul_assoc, one_mul]
gcongr
· exact zero_lt_iff.2 η.ne_zero
rw [← WithZero.coe_one, coe_lt_coe, ofAdd_neg, Right.inv_lt_one_iff, ← ofAdd_zero, Multiplicative.ofAdd_lt]
exact Int.zero_lt_one
