Evaluation of power series in Hahn Series

We describe a class of ring homomorphisms from formal power series to Hahn series, given by substitution of the generating variable to an element of strictly positive order.

Main Definitions

• HahnSeries.SummableFamily.powerSeriesFamily: A summable family of Hahn series whose elements are non-negative powers of a fixed positive-order Hahn series multiplied by the coefficients of a formal power series.
• PowerSeries.heval: The R-algebra homomorphism from PowerSeries σ R to R⟦Γ⟧ that takes X to a fixed positive-order Hahn Series and extends to formal infinite sums.

TODO

• MvPowerSeries.heval: An R-algebra homomorphism from MvPowerSeries σ R to R⟦Γ⟧ (for finite σ) taking each X i to a positive order Hahn Series.

@[reducible, inline]

noncomputable abbrev HahnSeries.SummableFamily.powerSeriesFamily {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] (x : HahnSeries Γ V) (f : PowerSeries R) : SummableFamily Γ V ℕ

A summable family given by scalar multiples of powers of a positive order Hahn series.

The scalar multiples are given by the coefficients of a power series.

Equations

• HahnSeries.SummableFamily.powerSeriesFamily x f = HahnSeries.SummableFamily.smulFamily (fun (n : ℕ) => (PowerSeries.coeff n) f) (HahnSeries.SummableFamily.powers x)

theorem HahnSeries.SummableFamily.powerSeriesFamily_of_not_orderTop_pos {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : ¬0 < x.orderTop) (f : PowerSeries R) : powerSeriesFamily x f = powerSeriesFamily 0 f

theorem HahnSeries.SummableFamily.powerSeriesFamily_of_orderTop_pos {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (f : PowerSeries R) (n : ℕ) : (powerSeriesFamily x f) n = (PowerSeries.coeff n) f • x ^ n

theorem HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] (f : PowerSeries R) : (powerSeriesFamily 0 f).hsum = PowerSeries.constantCoeff f • 1

theorem HahnSeries.SummableFamily.powerSeriesFamily_add {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (f g : PowerSeries R) : powerSeriesFamily x (f + g) = powerSeriesFamily x f + powerSeriesFamily x g

theorem HahnSeries.SummableFamily.powerSeriesFamily_smul {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (f : PowerSeries R) (r : R) : powerSeriesFamily x (r • f) = (HahnSeries.single 0) r • powerSeriesFamily x f

theorem HahnSeries.SummableFamily.support_powerSeriesFamily_subset {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (a b : PowerSeries R) (g : Γ) : ((powerSeriesFamily x (a * b)).coeff g).support ⊆ Finset.image (fun (i : ℕ × ℕ) => i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support

theorem HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (a b : PowerSeries R) : (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum

noncomputable def PowerSeries.heval {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) : PowerSeries R →ₐ[R] HahnSeries Γ R

The R-algebra homomorphism from R⟦X⟧ to R⟦Γ⟧ given by sending the power series variable X to a positive order element x and extending to infinite sums.

Equations

• PowerSeries.heval x = { toFun := fun (f : PowerSeries R) => (HahnSeries.SummableFamily.powerSeriesFamily x f).hsum, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem PowerSeries.heval_apply {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (f : PowerSeries R) : (heval x) f = (HahnSeries.SummableFamily.powerSeriesFamily x f).hsum

theorem PowerSeries.heval_mul {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) {a b : PowerSeries R} : (heval x) (a * b) = (heval x) a * (heval x) b

theorem PowerSeries.heval_C {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (r : R) : (heval x) (C r) = r • 1

theorem PowerSeries.heval_X {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (hx : 0 < x.orderTop) : (heval x) X = x

theorem PowerSeries.heval_unit {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (u : (PowerSeries R)ˣ) : IsUnit ((heval x) ↑u)

theorem PowerSeries.coeff_heval {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (f : PowerSeries R) (g : Γ) : ((heval x) f).coeff g = ∑ᶠ (n : ℕ), ((HahnSeries.SummableFamily.powerSeriesFamily x f).coeff g) n

theorem PowerSeries.coeff_heval_zero {Γ : Type u_1} {R : Type u_2} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (f : PowerSeries R) : ((heval x) f).coeff 0 = constantCoeff f