English
The weighted order equals a natural n iff there is a coefficient of weight n that is nonzero, and all coefficients of weight < n vanish.
Русский
Взвешенный порядок равен натуральному n тогда и только тогда, существует коэффициент веса n, не равный нулю, и все коэффициенты веса меньшего n равны нулю.
LaTeX
$$$f.weightedOrder w = n \iff \big( \exists d, \ coeff_d f \neq 0 \land weight w d = n \big) \land \forall d, weight w d < n \to coeff_d f = 0$$$
Lean4
/-- The order of a formal power series is exactly `n` if and only if some coefficient of weight `n`
is nonzero, and the `d`th coefficient is `0` for all `d` such that `weight w d < n`. -/
theorem weightedOrder_eq_nat {n : ℕ} :
f.weightedOrder w = n ↔ (∃ d, coeff d f ≠ 0 ∧ weight w d = n) ∧ ∀ d, weight w d < n → coeff d f = 0 :=
by
constructor
· intro h
obtain ⟨d, hd⟩ := f.exists_coeff_ne_zero_and_weightedOrder w (by simp only [h, toNat_coe])
exact
⟨⟨d, by simpa [h, Nat.cast_inj, ne_eq] using hd⟩, fun e he ↦
f.coeff_eq_zero_of_lt_weightedOrder w (by simp only [h, Nat.cast_lt, he])⟩
· rintro ⟨⟨d, hd', hd⟩, h⟩
exact le_antisymm (hd.symm ▸ f.weightedOrder_le w hd') (nat_le_weightedOrder w h)
