Summable families of Hahn Series

We introduce a notion of formal summability for families of Hahn series, and define a formal sum function. This theory is applied to characterize invertible Hahn series whose coefficients are in a commutative domain.

Main Definitions

• HahnSeries.SummableFamily is a family of Hahn series such that the union of the supports is partially well-ordered and only finitely many are nonzero at any given coefficient. Note that this is different from Summable in the valuation topology, because there are topologically summable families that do not satisfy the axioms of HahnSeries.SummableFamily, and formally summable families whose sums do not converge topologically.
• HahnSeries.SummableFamily.hsum is the formal sum of a summable family.
• HahnSeries.SummableFamily.lsum is the formal sum bundled as a LinearMap.
• HahnSeries.SummableFamily.smul is the summable family given by pointwise scalar multiplication of component Hahn series.
• HahnSeries.SummableFamily.mul is the summable family given by pointwise multiplication.
• HahnSeries.SummableFamily.powers is the summable family given by non-negative powers of a Hahn series, if the series has strictly positive order. If the series has non-positive order, then the summable family takes the junk value of zero.

Main results

• HahnSeries.isUnit_iff: If R is a commutative domain, and Γ is a linearly ordered additive commutative group, then a Hahn series is a unit if and only if its leading term is a unit in R.
• HahnSeries.SummableFamily.hsum_smul: smul is compatible with hsum.
• HahnSeries.SummableFamily.hsum_mul: mul is compatible with hsum. That is, the product of sums is equal to the sum of pointwise products.

TODO

• Summable Pi families

References

• [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]

structure HahnSeries.SummableFamily (Γ : Type u_8) (R : Type u_9) [PartialOrder Γ] [AddCommMonoid R] (α : Type u_7) : Type (max (max u_7 u_8) u_9)

A family of Hahn series whose formal coefficient-wise sum is a Hahn series. For each coefficient of the sum to be well-defined, we require that only finitely many series are nonzero at any given coefficient. For the formal sum to be a Hahn series, we require that the union of the supports of the constituent series is partially well-ordered.

• toFun : α → HahnSeries Γ R

  A parametrized family of Hahn series.

• isPWO_iUnion_support' : (⋃ (a : α), (self.toFun a).support).IsPWO
• finite_co_support' (g : Γ) : {a : α | (self.toFun a).coeff g ≠ 0}.Finite

@[implicit_reducible]

instance HahnSeries.SummableFamily.instFunLike {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : FunLike (SummableFamily Γ R α) α (HahnSeries Γ R)

@[simp]

theorem HahnSeries.SummableFamily.coe_mk {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (toFun : α → HahnSeries Γ R) (h1 : (⋃ (a : α), (toFun a).support).IsPWO) (h2 : ∀ (g : Γ), {a : α | (toFun a).coeff g ≠ 0}.Finite) : ⇑{ toFun := toFun, isPWO_iUnion_support' := h1, finite_co_support' := h2 } = toFun

theorem HahnSeries.SummableFamily.isPWO_iUnion_support {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) : (⋃ (a : α), (s a).support).IsPWO

theorem HahnSeries.SummableFamily.finite_co_support {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (g : Γ) : Function.HasFiniteSupport fun (a : α) => (s a).coeff g

theorem HahnSeries.SummableFamily.coe_injective {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : Function.Injective DFunLike.coe

theorem HahnSeries.SummableFamily.ext {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s t : SummableFamily Γ R α} (h : ∀ (a : α), s a = t a) : s = t

theorem HahnSeries.SummableFamily.ext_iff {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s t : SummableFamily Γ R α} : s = t ↔ ∀ (a : α), s a = t a

@[implicit_reducible]

instance HahnSeries.SummableFamily.instAdd {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : Add (SummableFamily Γ R α)

@[implicit_reducible]

instance HahnSeries.SummableFamily.instZero {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : Zero (SummableFamily Γ R α)

@[implicit_reducible]

instance HahnSeries.SummableFamily.instInhabited {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : Inhabited (SummableFamily Γ R α)

@[simp]

theorem HahnSeries.SummableFamily.coe_add {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s t : SummableFamily Γ R α) : ⇑(s + t) = ⇑s + ⇑t

theorem HahnSeries.SummableFamily.add_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s t : SummableFamily Γ R α} {a : α} : (s + t) a = s a + t a

@[simp]

theorem HahnSeries.SummableFamily.coe_zero {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : ⇑0 = 0

theorem HahnSeries.SummableFamily.zero_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {a : α} : 0 a = 0

@[implicit_reducible]

instance HahnSeries.SummableFamily.instSMul {Γ : Type u_1} {R : Type u_3} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] {M : Type u_7} [SMulZeroClass M R] : SMul M (SummableFamily Γ R β)

@[simp]

theorem HahnSeries.SummableFamily.coe_smul' {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {M : Type u_7} [SMulZeroClass M R] (m : M) (s : SummableFamily Γ R α) : ⇑(m • s) = m • ⇑s

theorem HahnSeries.SummableFamily.smul_apply' {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {M : Type u_7} [SMulZeroClass M R] (m : M) (s : SummableFamily Γ R α) (a : α) : (m • s) a = m • s a

@[implicit_reducible]

instance HahnSeries.SummableFamily.instAddCommMonoid {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : AddCommMonoid (SummableFamily Γ R α)

noncomputable def HahnSeries.SummableFamily.coeff {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (g : Γ) : α →₀ R

The coefficient function of a summable family, as a finsupp on the parameter type.

@[simp]

theorem HahnSeries.SummableFamily.coeff_support {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (g : Γ) : (s.coeff g).support = Set.Finite.toFinset ⋯

@[simp]

theorem HahnSeries.SummableFamily.coeff_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (g : Γ) (a : α) : (s.coeff g) a = (s a).coeff g

@[simp]

theorem HahnSeries.SummableFamily.coeff_def {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (a : α) (g : Γ) : (s.coeff g) a = (s a).coeff g

noncomputable def HahnSeries.SummableFamily.hsum {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) : HahnSeries Γ R

The infinite sum of a SummableFamily of Hahn series.

@[simp]

theorem HahnSeries.SummableFamily.coeff_hsum {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} {g : Γ} : s.hsum.coeff g = ∑ᶠ (i : α), (s i).coeff g

@[simp]

theorem HahnSeries.SummableFamily.hsum_zero {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] : hsum 0 = 0

theorem HahnSeries.SummableFamily.support_hsum_subset {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} : s.hsum.support ⊆ ⋃ (a : α), (s a).support

@[simp]

theorem HahnSeries.SummableFamily.hsum_add {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s t : SummableFamily Γ R α} : (s + t).hsum = s.hsum + t.hsum

theorem HahnSeries.SummableFamily.coeff_hsum_eq_sum_of_subset {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} {g : Γ} {t : Finset α} (h : {a : α | (s a).coeff g ≠ 0} ⊆ ↑t) : s.hsum.coeff g = ∑ i ∈ t, (s i).coeff g

theorem HahnSeries.SummableFamily.coeff_hsum_eq_sum {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} {g : Γ} : s.hsum.coeff g = ∑ i ∈ (s.coeff g).support, (s i).coeff g

def HahnSeries.SummableFamily.single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] {ι : Type u_7} [DecidableEq ι] (i : ι) (x : HahnSeries Γ R) : SummableFamily Γ R ι

The summable family made of a single Hahn series.

@[simp]

theorem HahnSeries.SummableFamily.single_toFun {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] {ι : Type u_7} [DecidableEq ι] (i : ι) (x : HahnSeries Γ R) (j : ι) : (single i x) j = Pi.single i x j

@[simp]

theorem HahnSeries.SummableFamily.hsum_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] {ι : Type u_7} [DecidableEq ι] (i : ι) (x : HahnSeries Γ R) : (single i x).hsum = x

def HahnSeries.SummableFamily.const {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] (ι : Type u_7) [Finite ι] (x : HahnSeries Γ R) : SummableFamily Γ R ι

The summable family made of a constant Hahn series.

@[simp]

theorem HahnSeries.SummableFamily.const_toFun {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] (ι : Type u_7) [Finite ι] (x : HahnSeries Γ R) (x✝ : ι) : (const ι x) x✝ = x

@[simp]

theorem HahnSeries.SummableFamily.hsum_unique {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] {ι : Type u_7} [Unique ι] (x : SummableFamily Γ R ι) : x.hsum = x default

def HahnSeries.SummableFamily.Equiv {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (e : α ≃ β) (s : SummableFamily Γ R α) : SummableFamily Γ R β

A summable family induced by an equivalence of the parametrizing type.

@[simp]

theorem HahnSeries.SummableFamily.Equiv_toFun {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (e : α ≃ β) (s : SummableFamily Γ R α) (b : β) : (Equiv e s) b = s (e.symm b)

@[simp]

theorem HahnSeries.SummableFamily.hsum_equiv {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (e : α ≃ β) (s : SummableFamily Γ R α) : (Equiv e s).hsum = s.hsum

def HahnSeries.SummableFamily.smulFamily {Γ : Type u_1} {R : Type u_3} {V : Type u_4} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] [AddCommMonoid V] [SMulWithZero R V] (f : α → R) (s : SummableFamily Γ V α) : SummableFamily Γ V α

The summable family given by multiplying every series in a summable family by a scalar.

@[simp]

theorem HahnSeries.SummableFamily.smulFamily_toFun {Γ : Type u_1} {R : Type u_3} {V : Type u_4} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] [AddCommMonoid V] [SMulWithZero R V] (f : α → R) (s : SummableFamily Γ V α) (a : α) : (smulFamily f s) a = f a • s a

theorem HahnSeries.SummableFamily.hsum_smulFamily {Γ : Type u_1} {R : Type u_3} {V : Type u_4} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] [AddCommMonoid V] [SMulWithZero R V] (f : α → R) (s : SummableFamily Γ V α) (g : Γ) : (smulFamily f s).hsum.coeff g = ∑ᶠ (i : α), f i • (s i).coeff g

theorem HahnSeries.SummableFamily.le_hsum_support_mem {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} {g g' : Γ} (hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g') (hg' : g' ∈ s.hsum.support) : g ≤ g'

theorem HahnSeries.SummableFamily.hsum_orderTop_of_le {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} {g : Γ} {a : α} (ha : ↑g = (s a).orderTop) (hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g') (hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0) : s.hsum.orderTop = ↑g

theorem HahnSeries.SummableFamily.hsum_leadingCoeff_of_le {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {s : SummableFamily Γ R α} {g : Γ} {a : α} (ha : ↑g = (s a).orderTop) (hg : ∀ (b : α), ∀ g' ∈ (s b).support, g ≤ g') (hna : ∀ (b : α), b ≠ a → (s b).coeff g = 0) : s.hsum.leadingCoeff = (s a).coeff g

@[implicit_reducible]

instance HahnSeries.SummableFamily.instNeg {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] : Neg (SummableFamily Γ R α)

@[simp]

theorem HahnSeries.SummableFamily.coe_neg {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] (s : SummableFamily Γ R α) : ⇑(-s) = -⇑s

theorem HahnSeries.SummableFamily.neg_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] {s : SummableFamily Γ R α} {a : α} : (-s) a = -s a

@[implicit_reducible]

instance HahnSeries.SummableFamily.instSub {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] : Sub (SummableFamily Γ R α)

@[simp]

theorem HahnSeries.SummableFamily.coe_sub {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] (s t : SummableFamily Γ R α) : ⇑(s - t) = ⇑s - ⇑t

theorem HahnSeries.SummableFamily.sub_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] {s t : SummableFamily Γ R α} {a : α} : (s - t) a = s a - t a

@[implicit_reducible]

instance HahnSeries.SummableFamily.instAddCommGroup {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommGroup R] : AddCommGroup (SummableFamily Γ R α)

theorem HahnSeries.SummableFamily.smul_support_subset_prod {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (gh : Γ × Γ') : (Function.support fun (i : α × β) => (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset

theorem HahnSeries.SummableFamily.hasFiniteSupport_smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (gh : Γ × Γ') : Function.HasFiniteSupport fun (i : α × β) => (s i.1).coeff gh.1 • (t i.2).coeff gh.2

@[deprecated HahnSeries.SummableFamily.hasFiniteSupport_smul (since := "2026-03-03")]

theorem HahnSeries.SummableFamily.smul_support_finite {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (gh : Γ × Γ') : Function.HasFiniteSupport fun (i : α × β) => (s i.1).coeff gh.1 • (t i.2).coeff gh.2

Alias of HahnSeries.SummableFamily.hasFiniteSupport_smul.

theorem HahnSeries.SummableFamily.isPWO_iUnion_support_prod_smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ' V} (hs : (⋃ (a : α), (s a).support).IsPWO) (ht : (⋃ (b : β), (t b).support).IsPWO) : (⋃ (a : α × β), ((fun (a : α × β) => (HahnModule.of R).symm (s a.1 • (HahnModule.of R) (t a.2))) a).support).IsPWO

theorem HahnSeries.SummableFamily.finite_co_support_prod_smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ') : Finite ↑{ab : α × β | ((fun (ab : α × β) => (HahnModule.of R).symm (s ab.1 • (HahnModule.of R) (t ab.2))) ab).coeff g ≠ 0}

noncomputable def HahnSeries.SummableFamily.smul {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) : SummableFamily Γ' V (α × β)

An elementwise scalar multiplication of one summable family on another.

@[simp]

theorem HahnSeries.SummableFamily.smul_toFun {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (ab : α × β) : (s.smul t) ab = (HahnModule.of R).symm (s ab.1 • (HahnModule.of R) (t ab.2))

theorem HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ') (a : α × β) : ∑ x ∈ Finset.VAddAntidiagonal ⋯ ⋯ g, (s a.1).coeff x.1 • (t a.2).coeff x.2 = ∑ x ∈ Finset.VAddAntidiagonal ⋯ ⋯ g, (s a.1).coeff x.1 • (t a.2).coeff x.2

theorem HahnSeries.SummableFamily.coeff_smul {Γ : Type u_1} {Γ' : Type u_2} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] {R : Type u_7} {V : Type u_8} [Semiring R] [AddCommMonoid V] [Module R V] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ') : (s.smul t).hsum.coeff g = ∑ gh ∈ Finset.VAddAntidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 • t.hsum.coeff gh.2

theorem HahnSeries.SummableFamily.smul_hsum {Γ : Type u_1} {Γ' : Type u_2} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] {R : Type u_7} {V : Type u_8} [Semiring R] [AddCommMonoid V] [Module R V] (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) : (s.smul t).hsum = (HahnModule.of R).symm (s.hsum • (HahnModule.of R) t.hsum)

@[implicit_reducible]

noncomputable instance HahnSeries.SummableFamily.instSMul_1 {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] : SMul (HahnSeries Γ R) (SummableFamily Γ' V β)

theorem HahnSeries.SummableFamily.smul_eq {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {β : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] {x : HahnSeries Γ R} {t : SummableFamily Γ' V β} : x • t = Equiv (Equiv.punitProd β) ((const Unit x).smul t)

@[simp]

theorem HahnSeries.SummableFamily.smul_apply {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [AddCommMonoid V] [AddCommMonoid R] [SMulWithZero R V] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] {x : HahnSeries Γ R} {s : SummableFamily Γ' V α} {a : α} : (x • s) a = (HahnModule.of R).symm (x • (HahnModule.of R) (s a))

@[simp]

theorem HahnSeries.SummableFamily.hsum_smul_module {Γ : Type u_1} {Γ' : Type u_2} {α : Type u_5} [PartialOrder Γ] [PartialOrder Γ'] [VAdd Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] {R : Type u_7} {V : Type u_8} [Semiring R] [AddCommMonoid V] [Module R V] {x : HahnSeries Γ R} {s : SummableFamily Γ' V α} : (x • s).hsum = (HahnModule.of R).symm (x • (HahnModule.of R) s.hsum)

@[implicit_reducible]

noncomputable instance HahnSeries.SummableFamily.instModule {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [PartialOrder Γ'] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ'] [Semiring R] [AddCommMonoid V] [Module R V] : Module (HahnSeries Γ R) (SummableFamily Γ' V α)

theorem HahnSeries.SummableFamily.hsum_smul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {x : HahnSeries Γ R} {s : SummableFamily Γ R α} : (x • s).hsum = x * s.hsum

noncomputable def HahnSeries.SummableFamily.lsum {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] : SummableFamily Γ R α →ₗ[HahnSeries Γ R] HahnSeries Γ R

The summation of a summable_family as a LinearMap.

@[simp]

theorem HahnSeries.SummableFamily.lsum_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) : lsum s = s.hsum

@[simp]

theorem HahnSeries.SummableFamily.hsum_sub {Γ : Type u_1} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] {R : Type u_7} [Ring R] {s t : SummableFamily Γ R α} : (s - t).hsum = s.hsum - t.hsum

theorem HahnSeries.SummableFamily.isPWO_iUnion_support_prod_mul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {s : α → HahnSeries Γ R} {t : β → HahnSeries Γ R} (hs : (⋃ (a : α), (s a).support).IsPWO) (ht : (⋃ (b : β), (t b).support).IsPWO) : (⋃ (a : α × β), ((fun (a : α × β) => s a.1 * t a.2) a).support).IsPWO

theorem HahnSeries.SummableFamily.finite_co_support_prod_mul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) (g : Γ) : Finite ↑{a : α × β | ((fun (a : α × β) => s a.1 * t a.2) a).coeff g ≠ 0}

noncomputable def HahnSeries.SummableFamily.mul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) : SummableFamily Γ R (α × β)

A summable family given by pointwise multiplication of a pair of summable families.

@[simp]

theorem HahnSeries.SummableFamily.mul_toFun {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) (a : α × β) : (s.mul t) a = s a.1 * t a.2

theorem HahnSeries.SummableFamily.mul_eq_smul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) : s.mul t = s.smul t

theorem HahnSeries.SummableFamily.coeff_hsum_mul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) (g : Γ) : (s.mul t).hsum.coeff g = ∑ gh ∈ Finset.addAntidiagonal ⋯ ⋯ g, s.hsum.coeff gh.1 * t.hsum.coeff gh.2

theorem HahnSeries.SummableFamily.hsum_mul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) : (s.mul t).hsum = s.hsum * t.hsum

def HahnSeries.SummableFamily.ofFinsupp {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] (f : α →₀ HahnSeries Γ R) : SummableFamily Γ R α

A family with only finitely many nonzero elements is summable.

@[simp]

theorem HahnSeries.SummableFamily.coe_ofFinsupp {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {f : α →₀ HahnSeries Γ R} : ⇑(ofFinsupp f) = ⇑f

@[simp]

theorem HahnSeries.SummableFamily.hsum_ofFinsupp {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [PartialOrder Γ] [AddCommMonoid R] {f : α →₀ HahnSeries Γ R} : (ofFinsupp f).hsum = f.sum fun (x : α) => id

noncomputable def HahnSeries.SummableFamily.embDomain {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (f : α ↪ β) : SummableFamily Γ R β

A summable family can be reindexed by an embedding without changing its sum.

theorem HahnSeries.SummableFamily.embDomain_apply {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (f : α ↪ β) {b : β} : (s.embDomain f) b = if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0

@[simp]

theorem HahnSeries.SummableFamily.embDomain_image {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (f : α ↪ β) {a : α} : (s.embDomain f) (f a) = s a

@[simp]

theorem HahnSeries.SummableFamily.embDomain_notin_range {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (f : α ↪ β) {b : β} (h : b ∉ Set.range ⇑f) : (s.embDomain f) b = 0

@[simp]

theorem HahnSeries.SummableFamily.hsum_embDomain {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [PartialOrder Γ] [AddCommMonoid R] (s : SummableFamily Γ R α) (f : α ↪ β) : (s.embDomain f).hsum = s.hsum

theorem HahnSeries.SummableFamily.support_pow_subset_closure {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (x : HahnSeries Γ R) (n : ℕ) : (x ^ n).support ⊆ ↑(AddSubmonoid.closure x.support)

theorem HahnSeries.SummableFamily.isPWO_iUnion_support_powers {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {x : HahnSeries Γ R} (hx : 0 ≤ x.order) : (⋃ (n : ℕ), (x ^ n).support).IsPWO

theorem HahnSeries.SummableFamily.co_support_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] (g : Γ) : {a : ℕ | ¬(0 ^ a).coeff g = 0} ⊆ {0}

theorem HahnSeries.SummableFamily.pow_finite_co_support {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : Γ) : {a : ℕ | ((fun (n : ℕ) => x ^ n) a).coeff g ≠ 0}.Finite

noncomputable def HahnSeries.SummableFamily.powers {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) : SummableFamily Γ R ℕ

A summable family of powers of a Hahn series x. If x has non-positive orderTop, then return a junk value given by pretending x = 0.

@[simp]

theorem HahnSeries.SummableFamily.powers_toFun {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) (n : ℕ) : (powers x) n = (if 0 < x.orderTop then x else 0) ^ n

theorem HahnSeries.SummableFamily.powers_of_orderTop_pos {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (n : ℕ) : (powers x) n = x ^ n

theorem HahnSeries.SummableFamily.powers_of_not_orderTop_pos {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : ¬0 < x.orderTop) : powers x = single 0 1

@[simp]

theorem HahnSeries.SummableFamily.powers_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] : powers 0 = single 0 1

@[simp]

theorem HahnSeries.SummableFamily.coe_powers {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : ⇑(powers x) = HPow.hPow x

theorem HahnSeries.SummableFamily.embDomain_succ_smul_powers {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (x • powers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = powers x - ofFinsupp fun₀ | 0 => 1

theorem HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (1 - x) * (powers x).hsum = 1

theorem HahnSeries.one_minus_single_neg_mul {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x y : HahnSeries Γ R} {r : R} (hr : r * x.leadingCoeff = 1) (hxy : x = y + (single x.order) x.leadingCoeff) (oinv : Γ) (hxo : oinv + x.order = 0) : 1 - (single oinv) r * x = -((single oinv) r * y)

theorem HahnSeries.unit_aux {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1) (oinv : Γ) (hxo : oinv + x.order = 0) : 0 < (1 - (single oinv) r * x).orderTop

theorem HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : IsUnit x.leadingCoeff) (hxo : IsAddUnit x.order) : IsUnit x

theorem HahnSeries.isUnit_of_orderTop_pos {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (h : 0 < (x - 1).orderTop) : IsUnit x

noncomputable def HahnSeries.toOrderTopSubOnePos {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (h : 0 < (x - 1).orderTop) : ↥(orderTopSubOnePos Γ R)

Make an element of orderTopSubOnePos

@[simp]

theorem HahnSeries.val_inv_toOrderTopSubOnePos_coe {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (h : 0 < (x - 1).orderTop) : ↑(↑(toOrderTopSubOnePos h))⁻¹ = ⋯.unit.inv

@[simp]

theorem HahnSeries.val_toOrderTopSubOnePos_coe {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (h : 0 < (x - 1).orderTop) : ↑↑(toOrderTopSubOnePos h) = x

theorem HahnSeries.isUnit_iff {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [CommRing R] [IsDomain R] {x : HahnSeries Γ R} : IsUnit x ↔ IsUnit x.leadingCoeff

@[implicit_reducible]

noncomputable instance HahnSeries.instDivInvMonoid {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field R] : DivInvMonoid (HahnSeries Γ R)

theorem HahnSeries.inv_def {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field R] (x : HahnSeries Γ R) : x⁻¹ = (single (-x.order)) x.leadingCoeff⁻¹ * (SummableFamily.powers (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum

@[simp]

theorem HahnSeries.inv_single {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field R] (a : Γ) (r : R) : ((single a) r)⁻¹ = (single (-a)) r⁻¹

@[simp]

theorem HahnSeries.single_div_single {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field R] (a b : Γ) (r s : R) : (single a) r / (single b) s = (single (a - b)) (r / s)

@[implicit_reducible]

noncomputable instance HahnSeries.instField {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field R] : Field (HahnSeries Γ R)

theorem HahnSeries.single_zero_ofScientific {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field R] (m : ℕ) (e : Bool) (s : ℕ) : (single 0) (OfScientific.ofScientific m e s) = OfScientific.ofScientific m e s