English
For RatFunc K, the valuation defined via LaurentSeries agrees with the valuation defined via RatFunc embedding.
Русский
Для RatFunc K валюация, заданная через LaurentSeries, совпадает с валюацией, заданной через вложение RatFunc.
LaTeX
$$$\mathrm{Valuation}_{RatFunc}(f) = \mathrm{Valuation}_{LaurentSeries}(f)$$$
Lean4
theorem valuation_le_iff_coeff_lt_eq_zero {D : ℤ} {f : K⸨X⸩} :
Valued.v f ≤ exp (-D : ℤ) ↔ ∀ n : ℤ, n < D → f.coeff n = 0 :=
by
refine ⟨fun hnD n hn => coeff_zero_of_lt_valuation K hnD hn, fun h_val_f => ?_⟩
let F := powerSeriesPart f
by_cases ord_nonpos : f.order ≤ 0
· obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos
rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, neg_neg, mul_comm, ← le_mul_inv_iff₀,
exp_neg, ← mul_inv, ← exp_add, ← exp_neg]
· by_cases hDs : D + s ≤ 0
· apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]
· obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (le_of_lt <| not_le.mp hDs)
rw [hd]
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
intro n hn
rw [powerSeriesPart_coeff f n, hs]
apply h_val_f
cutsat
· simp [ne_eq, zero_lt_iff]
· obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat <| neg_nonpos_of_nonneg <| le_of_lt <| not_le.mp ord_nonpos
rw [neg_inj] at hs
rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, mul_comm, ← le_mul_inv_iff₀, ←
exp_neg, ← exp_add, neg_neg]
· by_cases hDs : D - s ≤ 0
· apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
rw [← log_le_iff_le_exp one_ne_zero, log_one]
cutsat
· obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (le_of_lt <| not_le.mp hDs)
rw [← neg_neg (-D + ↑s), ← sub_eq_neg_add, neg_sub, hd]
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
intro n hn
rw [powerSeriesPart_coeff f n, hs]
apply h_val_f (s + n)
cutsat
· simp [ne_eq, zero_lt_iff]
