English
If x has positive orderTop, then for any g the set { a ∈ ℕ | (x^a).coeff g ≠ 0 } is finite.
Русский
Если orderTop(x) > 0, то для фиксированного g множество { a ∈ ℕ | (x^a).coeff g ≠ 0 } конечно.
LaTeX
$$$\{a \in \mathbb{N} \mid (x^a).coeff(g) \neq 0\} \\text{ is finite}$$$
Lean4
theorem pow_finite_co_support {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : Γ) :
Set.Finite {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0} :=
by
have hpwo : Set.IsPWO (⋃ n, support (x ^ n)) := isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt hx)
by_cases h0 : x = 0; · exact h0 ▸ Set.Finite.subset (Set.finite_singleton 0) (co_support_zero g)
by_cases hg : g ∈ ⋃ n : ℕ, {g | (x ^ n).coeff g ≠ 0}
swap; · exact Set.finite_empty.subset fun n hn => hg (Set.mem_iUnion.2 ⟨n, hn⟩)
apply hpwo.isWF.induction hg
intro y ys hy
refine
((((addAntidiagonal x.isPWO_support hpwo y).finite_toSet.biUnion fun ij hij =>
hy ij.snd (mem_addAntidiagonal.1 (mem_coe.1 hij)).2.1 ?_).image
Nat.succ).union
(Set.finite_singleton 0)).subset
?_
· obtain ⟨hi, _, rfl⟩ := mem_addAntidiagonal.1 (mem_coe.1 hij)
exact
lt_add_of_pos_left ij.2 <|
lt_of_lt_of_le ((zero_lt_orderTop_iff h0).mp hx) <| order_le_of_coeff_ne_zero <| Function.mem_support.mp hi
· rintro (_ | n) hn
· exact Set.mem_union_right _ (Set.mem_singleton 0)
· obtain ⟨i, hi, j, hj, rfl⟩ := support_mul_subset_add_support hn
refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩
simp only [mem_coe, mem_addAntidiagonal, mem_support, ne_eq, Set.mem_iUnion]
exact ⟨hj, ⟨n, hi⟩, add_comm j i⟩
