English
Under the same assumptions as above, for each g the set { a ∈ ℕ | (x^a).coeff g ≠ 0 } is finite.
Русский
При тех же предположениях множество { a ∈ ℕ | (x^a).coeff g ≠ 0 } конечное для каждого g.
LaTeX
$$$\{a \in \mathbb{N} \mid (x^a).coeff(g) \neq 0\} \\text{finite}$$$
Lean4
/-- A summable family of powers of a Hahn series `x`. If `x` has non-positive `orderTop`, then
return a junk value given by pretending `x = 0`. -/
@[simps]
def powers (x : HahnSeries Γ R) : SummableFamily Γ R ℕ
where
toFun n := (if 0 < x.orderTop then x else 0) ^ n
isPWO_iUnion_support' := by
by_cases h : 0 < x.orderTop
· simp only [h, ↓reduceIte]
exact isPWO_iUnion_support_powers (zero_le_orderTop_iff.mp <| le_of_lt h)
· simp only [h, ↓reduceIte]
apply isPWO_iUnion_support_powers
rw [order_zero]
finite_co_support'
g := by
by_cases h : 0 < x.orderTop
· simp only [h, ↓reduceIte]
exact pow_finite_co_support h g
· simp only [h, ↓reduceIte]
exact pow_finite_co_support (orderTop_zero (R := R) (Γ := Γ) ▸ WithTop.top_pos) g
