Eventual agreement of coefficients of Hahn series

Over a locally finite index order, a family of Hahn series whose supports are eventually bounded below by one common index, and each of whose coefficients eventually agrees with the corresponding coefficient of a fixed series, eventually agrees with that series at every coefficient below any prescribed index. This upgrades pointwise stabilization to stabilization of every initial segment of coefficients, which is the form in which order-based convergence statements consume it.

The proof adapts the finite-interval assembly in LaurentSeries.Cauchy.coeff_eventually_equal from Mathlib. Here its Cauchy-filter-specific coefficient limit is replaced by an arbitrary fixed Hahn series and an arbitrary filter.

Main results

• TauCeti.hahnSeries_eventually_forall_lt_coeff_eq: a common eventual lower support bound and eventual equality of each coefficient give eventual equality of all coefficients below any given index.

theorem TauCeti.hahnSeries_eventually_forall_lt_coeff_eq {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [LocallyFiniteOrder Γ] [Zero R] {ι : Type u_3} {l : Filter ι} {f : ι → HahnSeries Γ R} {g : HahnSeries Γ R} {b : Γ} (hlb : ∀ᶠ (i : ι) in l, ∀ z < b, (f i).coeff z = 0) (hcoeff : ∀ (z : Γ), ∀ᶠ (i : ι) in l, (f i).coeff z = g.coeff z) (D : Γ) : ∀ᶠ (i : ι) in l, ∀ z < D, (f i).coeff z = g.coeff z

If the supports of a family of Hahn series are eventually bounded below by a common index b, and each coefficient eventually agrees with the corresponding coefficient of g, then for every D the family eventually agrees with g at all coefficients below D.