valuation_le_iff_coeff_lt_log_eq_zero

English

A refined version: for any Laurent series f and D a nonzero log, Valued.v f ≤ D if and only if all coefficients below -log D vanish.

Русский

Уточнённая версия: для любого LaurentSeries f и не нулевого D, Valued.v f ≤ D тогда и только тогда, когда коэффициенты ниже -log D равны нулю.

LaTeX

$$$\forall D\in WithZero (Multiplicative\ Int),\; D\neq 0 \Rightarrow v(f) \le D \iff \forall n< -\log D,\; f.coeff n = 0$$$

Lean4

theorem valuation_le_iff_coeff_lt_log_eq_zero {D : ℤᵐ⁰} (hD : D ≠ 0) {f : K⸨X⸩} :
    Valued.v f ≤ D ↔ ∀ n : ℤ, n < -log D → f.coeff n = 0 :=
  by
  cases D
  · simp_all
  · rename_i D
    cases D
    rename_i D
    rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]
      /- Two Laurent series whose difference has small valuation have the same coefficients for
      small enough indices. -/

Похожие утверждения