# Hahn Series #

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on HahnSeries Γ R, with the most studied case being when Γ is a linearly ordered abelian group and R is a field, in which case HahnSeries Γ R is a valued field, with value group Γ. These generalize Laurent series (with value group ℤ), and Laurent series are implemented that way in the file RingTheory/LaurentSeries.

## Main Definitions #

• If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered.
• support x is the subset of Γ whose coefficients are nonzero.
• single a r is the Hahn series which has coefficient r at a and zero otherwise.
• orderTop x is a minimal element of WithTop Γ where x has a nonzero coefficient if x ≠ 0, and is ⊤ when x = 0.
• order x is a minimal element of Γ where x has a nonzero coefficient if x ≠ 0, and is zero when x = 0.

## References #

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]
theorem HahnSeries.ext_iff {Γ : Type u_1} {R : Type u_2} :
∀ {inst : } {inst_1 : Zero R} (x y : ), x = y x.coeff = y.coeff
theorem HahnSeries.ext {Γ : Type u_1} {R : Type u_2} :
∀ {inst : } {inst_1 : Zero R} (x y : ), x.coeff = y.coeffx = y
structure HahnSeries (Γ : Type u_1) (R : Type u_2) [] [Zero R] :
Type (max u_1 u_2)

If Γ is linearly ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are well-founded.

• coeff : ΓR

The coefficient function of a Hahn Series.

• isPWO_support' : (Function.support self.coeff).IsPWO
Instances For
theorem HahnSeries.isPWO_support' {Γ : Type u_1} {R : Type u_2} [] [Zero R] (self : ) :
(Function.support self.coeff).IsPWO
theorem HahnSeries.coeff_injective {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
Function.Injective HahnSeries.coeff
@[simp]
theorem HahnSeries.coeff_inj {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } {y : } :
x.coeff = y.coeff x = y
def HahnSeries.support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :
Set Γ

The support of a Hahn series is just the set of indices whose coefficients are nonzero. Notably, it is well-founded.

Equations
Instances For
@[simp]
theorem HahnSeries.isPWO_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :
x.support.IsPWO
@[simp]
theorem HahnSeries.isWF_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :
x.support.IsWF
@[simp]
theorem HahnSeries.mem_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) (a : Γ) :
a x.support x.coeff a 0
instance HahnSeries.instZero {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
Zero ()
Equations
• HahnSeries.instZero = { zero := { coeff := 0, isPWO_support' := } }
instance HahnSeries.instInhabited {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
Equations
• HahnSeries.instInhabited = { default := 0 }
instance HahnSeries.instSubsingleton {Γ : Type u_1} {R : Type u_2} [] [Zero R] [] :
Equations
• =
@[simp]
theorem HahnSeries.zero_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} :
= 0
@[simp]
theorem HahnSeries.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x.coeff = 0 x = 0
theorem HahnSeries.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } {g : Γ} (h : x.coeff g 0) :
x 0
@[simp]
theorem HahnSeries.support_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
@[simp]
theorem HahnSeries.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x.support.Nonempty x 0
@[simp]
theorem HahnSeries.support_eq_empty_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x.support = x = 0
def HahnSeries.ofIterate {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] (x : HahnSeries Γ (HahnSeries Γ' R)) :
HahnSeries (Lex (Γ × Γ')) R

Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product.

Equations
• x.ofIterate = { coeff := fun (g : Lex (Γ × Γ')) => (x.coeff g.1).coeff g.2, isPWO_support' := }
Instances For
@[simp]
theorem HahnSeries.mk_eq_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] (f : ΓR) (h : ().IsPWO) :
{ coeff := f, isPWO_support' := h } = 0 f = 0
def HahnSeries.toIterate {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] (x : HahnSeries (Lex (Γ × Γ')) R) :

Change a Hahn series on a lex product to a Hahn series with coefficients in a Hahn series.

Equations
• x.toIterate = { coeff := fun (g : Γ) => { coeff := fun (g' : Γ') => x.coeff (g, g'), isPWO_support' := }, isPWO_support' := }
Instances For
@[simp]
theorem HahnSeries.iterateEquiv_symm_apply {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] (x : HahnSeries (Lex (Γ × Γ')) R) :
HahnSeries.iterateEquiv.symm x = x.toIterate
@[simp]
theorem HahnSeries.iterateEquiv_apply {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] (x : HahnSeries Γ (HahnSeries Γ' R)) :
HahnSeries.iterateEquiv x = x.ofIterate
def HahnSeries.iterateEquiv {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] :
HahnSeries Γ (HahnSeries Γ' R) HahnSeries (Lex (Γ × Γ')) R

The equivalence between iterated Hahn series and Hahn series on the lex product.

Equations
• HahnSeries.iterateEquiv = { toFun := HahnSeries.ofIterate, invFun := HahnSeries.toIterate, left_inv := , right_inv := }
Instances For
def HahnSeries.single {Γ : Type u_1} {R : Type u_2} [] [Zero R] (a : Γ) :
ZeroHom R ()

single a r is the Hahn series which has coefficient r at a and zero otherwise.

Equations
• = { toFun := fun (r : R) => { coeff := , isPWO_support' := }, map_zero' := }
Instances For
@[simp]
theorem HahnSeries.single_coeff_same {Γ : Type u_1} {R : Type u_2} [] [Zero R] (a : Γ) (r : R) :
( r).coeff a = r
@[simp]
theorem HahnSeries.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {b : Γ} {r : R} (h : b a) :
( r).coeff b = 0
theorem HahnSeries.single_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {b : Γ} {r : R} :
( r).coeff b = if b = a then r else 0
@[simp]
theorem HahnSeries.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} (h : r 0) :
( r).support = {a}
theorem HahnSeries.support_single_subset {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} :
( r).support {a}
theorem HahnSeries.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} {b : Γ} (h : b ( r).support) :
b = a
theorem HahnSeries.single_eq_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} :
0 = 0
theorem HahnSeries.single_injective {Γ : Type u_1} {R : Type u_2} [] [Zero R] (a : Γ) :
theorem HahnSeries.single_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} (h : r 0) :
r 0
@[simp]
theorem HahnSeries.single_eq_zero_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} :
r = 0 r = 0
instance HahnSeries.instNontrivialOfNonempty {Γ : Type u_1} {R : Type u_2} [] [Zero R] [] [] :
Equations
• =
def HahnSeries.orderTop {Γ : Type u_1} {R : Type u_2} [] [Zero R] (x : ) :

The orderTop of a Hahn series x is a minimal element of WithTop Γ where x has a nonzero coefficient if x ≠ 0, and is ⊤ when x = 0.

Equations
• x.orderTop = if h : x = 0 then else (.min )
Instances For
@[simp]
theorem HahnSeries.orderTop_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] :
theorem HahnSeries.orderTop_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } (hx : x 0) :
x.orderTop = (.min )
@[simp]
theorem HahnSeries.ne_zero_iff_orderTop {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x 0 x.orderTop
theorem HahnSeries.orderTop_eq_top_iff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } :
x.orderTop = x = 0
theorem HahnSeries.untop_orderTop_of_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } (hx : x 0) :
x.orderTop.untop = .min
theorem HahnSeries.coeff_orderTop_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } {g : Γ} (hg : x.orderTop = g) :
x.coeff g 0
theorem HahnSeries.orderTop_le_of_coeff_ne_zero {R : Type u_2} [Zero R] {Γ : Type u_3} [] {x : } {g : Γ} (h : x.coeff g 0) :
x.orderTop g
@[simp]
theorem HahnSeries.orderTop_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} (h : r 0) :
( r).orderTop = a
theorem HahnSeries.coeff_eq_zero_of_lt_orderTop {Γ : Type u_1} {R : Type u_2} [] [Zero R] {x : } {i : Γ} (hi : i < x.orderTop) :
x.coeff i = 0
def HahnSeries.order {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] (x : ) :
Γ

The order of a nonzero Hahn series x is a minimal element of Γ where x has a nonzero coefficient, the order of 0 is 0.

Equations
• x.order = if h : x = 0 then 0 else .min
Instances For
@[simp]
theorem HahnSeries.order_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] :
theorem HahnSeries.order_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } (hx : x 0) :
x.order = .min
theorem HahnSeries.order_eq_orderTop_of_ne {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } (hx : x 0) :
x.order = x.orderTop
theorem HahnSeries.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } (hx : x 0) :
x.coeff x.order 0
theorem HahnSeries.order_le_of_coeff_ne_zero {R : Type u_2} [Zero R] {Γ : Type u_3} {x : } {g : Γ} (h : x.coeff g 0) :
x.order g
@[simp]
theorem HahnSeries.order_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {a : Γ} {r : R} [Zero Γ] (h : r 0) :
( r).order = a
theorem HahnSeries.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_2} [] [Zero R] [Zero Γ] {x : } {i : Γ} (hi : i < x.order) :
x.coeff i = 0
def HahnSeries.embDomain {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] (f : Γ ↪o Γ') :
HahnSeries Γ' R

Extends the domain of a HahnSeries by an OrderEmbedding.

Equations
• = { coeff := fun (b : Γ') => if h : b f '' x.support then x.coeff () else 0, isPWO_support' := }
Instances For
@[simp]
theorem HahnSeries.embDomain_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } {a : Γ} :
().coeff (f a) = x.coeff a
@[simp]
theorem HahnSeries.embDomain_mk_coeff {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : ΓΓ'} (hfi : ) (hf : ∀ (g g' : Γ), f g f g' g g') {x : } {a : Γ} :
(HahnSeries.embDomain { toFun := f, inj' := hfi, map_rel_iff' := } x).coeff (f a) = x.coeff a
theorem HahnSeries.embDomain_notin_image_support {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } {b : Γ'} (hb : bf '' x.support) :
().coeff b = 0
theorem HahnSeries.support_embDomain_subset {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } :
().support f '' x.support
theorem HahnSeries.embDomain_notin_range {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {x : } {b : Γ'} (hb : b) :
().coeff b = 0
@[simp]
theorem HahnSeries.embDomain_zero {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} :
@[simp]
theorem HahnSeries.embDomain_single {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} {g : Γ} {r : R} :
= (HahnSeries.single (f g)) r
theorem HahnSeries.embDomain_injective {Γ : Type u_1} {R : Type u_2} [] [Zero R] {Γ' : Type u_3} [] {f : Γ ↪o Γ'} :
theorem HahnSeries.suppBddBelow_supp_PWO {Γ : Type u_1} {R : Type u_2} [Zero R] [] (f : ΓR) (hf : ) :
().IsPWO
theorem HahnSeries.forallLTEqZero_supp_BddBelow {Γ : Type u_1} {R : Type u_2} [Zero R] [] (f : ΓR) (n : Γ) (hn : m < n, f m = 0) :
@[simp]
theorem HahnSeries.ofSuppBddBelow_coeff {Γ : Type u_1} {R : Type u_2} [Zero R] [] (f : ΓR) (hf : ) :
∀ (a : Γ), ().coeff a = f a
def HahnSeries.ofSuppBddBelow {Γ : Type u_1} {R : Type u_2} [Zero R] [] (f : ΓR) (hf : ) :

Construct a Hahn series from any function whose support is bounded below.

Equations
• = { coeff := f, isPWO_support' := }
Instances For
theorem HahnSeries.BddBelow_zero {Γ : Type u_1} {R : Type u_2} [Zero R] [] [] :
@[simp]
theorem HahnSeries.zero_ofSuppBddBelow {Γ : Type u_1} {R : Type u_2} [Zero R] [] [] :
theorem HahnSeries.order_ofForallLtEqZero {Γ : Type u_1} {R : Type u_2} [Zero R] [] [Zero Γ] (f : ΓR) (hf : f 0) (n : Γ) (hn : m < n, f m = 0) :
n .order