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.
• PowerSeries.heval: The R-algebra homomorphism from PowerSeries σ R to HahnSeries Γ 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 HahnSeries Γ R (for finite σ) taking each X i 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

def PowerSeries.heval {Γ : Type u_1} {R : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : PowerSeries R →ₐ[R] HahnSeries Γ R

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PowerSeries.heval_apply {Γ : Type u_1} {R : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (f : PowerSeries R) : (heval hx) f = (HahnSeries.SummableFamily.powerSeriesFamily hx f).hsum

theorem PowerSeries.heval_mul {Γ : Type u_1} {R : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) {a b : PowerSeries R} : (heval hx) (a * b) = (heval hx) a * (heval hx) b

theorem PowerSeries.heval_unit {Γ : Type u_1} {R : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (u : (PowerSeries R)ˣ) : IsUnit ((heval hx) ↑u)

theorem PowerSeries.coeff_heval {Γ : Type u_1} {R : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (f : PowerSeries R) (g : Γ) : ((heval hx) f).coeff g = ∑ᶠ (n : ℕ), ((HahnSeries.SummableFamily.powerSeriesFamily hx f).coeff g) n

theorem PowerSeries.coeff_heval_zero {Γ : Type u_1} {R : Type u_3} [LinearOrderedCancelAddCommMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (f : PowerSeries R) : ((heval hx) f).coeff 0 = (constantCoeff R) f