A summable family given by a power series

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.

TODO

• PowerSeries.heval: An R-algebra homomorphism from PowerSeries R to HahnSeries Γ R taking X to a positive order Hahn Series.

@[reducible, inline]

abbrev HahnSeries.SummableFamily.powerSeriesFamily {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (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 hx f = HahnSeries.SummableFamily.smulFamily (fun (n : ℕ) => (PowerSeries.coeff R n) f) (HahnSeries.SummableFamily.powers x hx)

@[simp]

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

theorem HahnSeries.SummableFamily.powerSeriesFamily_add {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (f g : PowerSeries R) : powerSeriesFamily hx (f + g) = powerSeriesFamily hx f + powerSeriesFamily hx g

theorem HahnSeries.SummableFamily.powerSeriesFamily_smul {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (f : PowerSeries R) (r : R) : powerSeriesFamily hx (r • f) = (HahnSeries.single 0) r • powerSeriesFamily hx f

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

theorem HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] [CommRing V] [Algebra R V] {x : HahnSeries Γ V} (hx : 0 < x.orderTop) (a b : PowerSeries R) : (powerSeriesFamily hx (a * b)).hsum = ((powerSeriesFamily hx a).mul (powerSeriesFamily hx b)).hsum