nat_le_weightedOrder — Mathlib

English

If all coefficients with weight less than n vanish, then the weighted order of f is at least n; i.e., n ≤ weightedOrder_w(f).

Русский

Если все коэффициенты с весом меньше n равны нулю, то взвешенный порядок f не меньше n; т.е. n ≤ weightedOrder_w(f).

LaTeX

$$$n \le f.weightedOrder w$$$

Lean4

/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `weight w d < n`. -/
theorem nat_le_weightedOrder {n : ℕ} (h : ∀ d, weight w d < n → coeff d f = 0) : n ≤ f.weightedOrder w :=
  by
  by_contra! H
  have : (f.weightedOrder w).toNat = f.weightedOrder w := by rw [coe_toNat_eq_self]; exact ne_top_of_lt H
  obtain ⟨d, hfd, hd⟩ := exists_coeff_ne_zero_and_weightedOrder w this
  rw [← hd, Nat.cast_lt] at H
  exact hfd (h d H)

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