# Comparison between Hahn series and power 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. When R is a semiring and Γ = ℕ, then we get the more familiar semiring of formal power series with coefficients in R.

## Main Definitions #

• toPowerSeries the isomorphism from HahnSeries ℕ R to PowerSeries R.
• ofPowerSeries the inverse, casting a PowerSeries R to a HahnSeries ℕ R.

## TODO #

• Build an API for the variable X (defined to be single 1 1 : HahnSeries Γ R) in analogy to X : R[X] and X : PowerSeries R

## References #

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]
@[simp]
theorem HahnSeries.toPowerSeries_symm_apply_coeff {R : Type u_2} [] (f : ) (n : ) :
(HahnSeries.toPowerSeries.symm f).coeff n = () f
@[simp]
theorem HahnSeries.toPowerSeries_apply {R : Type u_2} [] (f : ) :
HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff
def HahnSeries.toPowerSeries {R : Type u_2} [] :

The ring HahnSeries ℕ R is isomorphic to PowerSeries R.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HahnSeries.coeff_toPowerSeries {R : Type u_2} [] {f : } {n : } :
() (HahnSeries.toPowerSeries f) = f.coeff n
theorem HahnSeries.coeff_toPowerSeries_symm {R : Type u_2} [] {f : } {n : } :
(HahnSeries.toPowerSeries.symm f).coeff n = () f
def HahnSeries.ofPowerSeries (Γ : Type u_1) (R : Type u_2) [] :

Casts a power series as a Hahn series with coefficients from a StrictOrderedSemiring.

Equations
• = .comp HahnSeries.toPowerSeries.symm.toRingHom
Instances For
theorem HahnSeries.ofPowerSeries_injective {Γ : Type u_1} {R : Type u_2} [] :
theorem HahnSeries.ofPowerSeries_apply {Γ : Type u_1} {R : Type u_2} [] (x : ) :
() x = HahnSeries.embDomain { toFun := Nat.cast, inj' := , map_rel_iff' := } (HahnSeries.toPowerSeries.symm x)
theorem HahnSeries.ofPowerSeries_apply_coeff {Γ : Type u_1} {R : Type u_2} [] (x : ) (n : ) :
(() x).coeff n = () x
@[simp]
theorem HahnSeries.ofPowerSeries_C {Γ : Type u_1} {R : Type u_2} [] (r : R) :
() (() r) = HahnSeries.C r
@[simp]
theorem HahnSeries.ofPowerSeries_X {Γ : Type u_1} {R : Type u_2} [] :
() PowerSeries.X = 1
theorem HahnSeries.ofPowerSeries_X_pow {Γ : Type u_1} {R : Type u_3} [] (n : ) :
() (PowerSeries.X ^ n) = () 1
@[simp]
theorem HahnSeries.toMvPowerSeries_symm_apply_coeff {R : Type u_2} [] {σ : Type u_3} [] (f : ) :
(HahnSeries.toMvPowerSeries.symm f).coeff = f
@[simp]
theorem HahnSeries.toMvPowerSeries_apply {R : Type u_2} [] {σ : Type u_3} [] (f : HahnSeries (σ →₀ ) R) :
∀ (a : σ →₀ ), HahnSeries.toMvPowerSeries f a = f.coeff a
def HahnSeries.toMvPowerSeries {R : Type u_2} [] {σ : Type u_3} [] :

The ring HahnSeries (σ →₀ ℕ) R is isomorphic to MvPowerSeries σ R for a Finite σ. We take the index set of the hahn series to be Finsupp rather than pi, even though we assume Finite σ as this is more natural for alignment with MvPowerSeries. After importing Algebra.Order.Pi the ring HahnSeries (σ → ℕ) R could be constructed instead.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HahnSeries.coeff_toMvPowerSeries {R : Type u_2} [] {σ : Type u_3} [] {f : HahnSeries (σ →₀ ) R} {n : σ →₀ } :
() (HahnSeries.toMvPowerSeries f) = f.coeff n
theorem HahnSeries.coeff_toMvPowerSeries_symm {R : Type u_2} [] {σ : Type u_3} [] {f : } {n : σ →₀ } :
(HahnSeries.toMvPowerSeries.symm f).coeff n = () f
@[simp]
theorem HahnSeries.toPowerSeriesAlg_apply (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] (f : ) :
= PowerSeries.mk f.coeff
@[simp]
theorem HahnSeries.toPowerSeriesAlg_symm_apply_coeff (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] (f : ) (n : ) :
(.symm f).coeff n = () f
def HahnSeries.toPowerSeriesAlg (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] :

The R-algebra HahnSeries ℕ A is isomorphic to PowerSeries A.

Equations
• = let __src := HahnSeries.toPowerSeries; { toEquiv := __src.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem HahnSeries.ofPowerSeriesAlg_apply_coeff (Γ : Type u_1) (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] :
∀ (a : ) (b : Γ), ( a).coeff b = if h : ∃ (x : ), ¬() a = 0 x = b then () a else 0
def HahnSeries.ofPowerSeriesAlg (Γ : Type u_1) (R : Type u_2) [] {A : Type u_3} [] [Algebra R A] :

Casting a power series as a Hahn series with coefficients from a StrictOrderedSemiring is an algebra homomorphism.

Equations
• = .comp .symm
Instances For
instance HahnSeries.powerSeriesAlgebra (Γ : Type u_1) (R : Type u_2) [] {S : Type u_4} [] [Algebra S ()] :
Algebra S ()
Equations
• = (().comp ()).toAlgebra
theorem HahnSeries.algebraMap_apply' (Γ : Type u_1) {R : Type u_2} [] {S : Type u_4} [] [Algebra S ()] (x : S) :
(algebraMap S ()) x = () (() x)
@[simp]
theorem Polynomial.algebraMap_hahnSeries_apply (Γ : Type u_1) {R : Type u_2} [] (f : ) :
(algebraMap () ()) f = () f