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

• A 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.
• The formal sum, HahnSeries.SummableFamily.hsum can be bundled as a LinearMap via HahnSeries.SummableFamily.lsum.

Main results

• 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.

TODO

• Remove unnecessary domain hypotheses.
• More general summable families, e.g., define the evaluation homomorphism from a power series ring taking X to a positive order element.

References

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

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

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

Equations

• HahnSeries.SummableFamily.instFunLike = { coe := HahnSeries.SummableFamily.toFun, coe_injective' := ⋯ }

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.support fun (a : α) => (s a).coeff g).Finite

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

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

Equations

• HahnSeries.SummableFamily.instAdd = { add := fun (x y : HahnSeries.SummableFamily Γ R α) => { toFun := ⇑x + ⇑y, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }

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

Equations

• HahnSeries.SummableFamily.instZero = { zero := { toFun := 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }

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

Equations

• HahnSeries.SummableFamily.instInhabited = { default := 0 }

@[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

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

Equations

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

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.

Equations

• s.coeff g = { support := ⋯.toFinset, toFun := fun (a : α) => (s a).coeff g, mem_support_toFun := ⋯ }

@[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 = ⋯.toFinset

@[simp]

theorem HahnSeries.SummableFamily.coeff_toFun {Γ : 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

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.

Equations

• s.hsum = { coeff := fun (g : Γ) => ∑ᶠ (i : α), (s i).coeff g, isPWO_support' := ⋯ }

@[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

@[deprecated HahnSeries.SummableFamily.coeff_hsum (since := "2025-01-31")]

theorem HahnSeries.SummableFamily.hsum_coeff {Γ : 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

Alias of HahnSeries.SummableFamily.coeff_hsum.

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

@[deprecated HahnSeries.SummableFamily.coeff_hsum_eq_sum_of_subset (since := "2025-01-31")]

theorem HahnSeries.SummableFamily.hsum_coeff_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

Alias of HahnSeries.SummableFamily.coeff_hsum_eq_sum_of_subset.

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

@[deprecated HahnSeries.SummableFamily.coeff_hsum_eq_sum (since := "2025-01-31")]

theorem HahnSeries.SummableFamily.hsum_coeff_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

Alias of HahnSeries.SummableFamily.coeff_hsum_eq_sum.

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

The summable family made of a single Hahn series.

Equations

• HahnSeries.SummableFamily.single x = { toFun := fun (x_1 : Unit) => x, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[simp]

theorem HahnSeries.SummableFamily.single_toFun {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] (x : HahnSeries Γ R) (x✝ : Unit) : (single x) x✝ = x

@[simp]

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

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.

Equations

• HahnSeries.SummableFamily.Equiv e s = { toFun := fun (b : β) => s (e.symm b), isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[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.

Equations

• HahnSeries.SummableFamily.smulFamily f s = { toFun := fun (a : α) => f a • s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[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

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

Equations

• HahnSeries.SummableFamily.instNeg = { neg := fun (s : HahnSeries.SummableFamily Γ R α) => { toFun := fun (a : α) => -s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }

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

Equations

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

@[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

@[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

instance HahnSeries.SummableFamily.instSMulOfSMulWithZero {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {β : Type u_6} [PartialOrder Γ'] [AddCommMonoid V] [Zero R] [SMulWithZero R V] : SMul R (SummableFamily Γ' V β)

Equations

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

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.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.support fun (i : α × β) => (s i.1).coeff gh.1 • (t i.2).coeff gh.2).Finite

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}

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.

Equations

• s.smul t = { toFun := fun (ab : α × β) => (HahnModule.of R).symm (s ab.1 • (HahnModule.of R) (t ab.2)), isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[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))

@[deprecated HahnSeries.SummableFamily.smul (since := "2024-11-17")]

def HahnSeries.SummableFamily.FamilySMul {Γ : 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 (α × β)

Alias of HahnSeries.SummableFamily.smul.

---

An elementwise scalar multiplication of one summable family on another.

Equations

• @HahnSeries.SummableFamily.FamilySMul = @HahnSeries.SummableFamily.smul

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

@[deprecated HahnSeries.SummableFamily.coeff_smul (since := "2024-11-17")]

theorem HahnSeries.SummableFamily.family_smul_coeff {Γ : 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

Alias of HahnSeries.SummableFamily.coeff_smul.

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)

@[deprecated HahnSeries.SummableFamily.smul_hsum (since := "2024-11-17")]

theorem HahnSeries.SummableFamily.hsum_family_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 β) : (s.smul t).hsum = (HahnModule.of R).symm (s.hsum • (HahnModule.of R) t.hsum)

Alias of HahnSeries.SummableFamily.smul_hsum.

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

Equations

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

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 β) ((single 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)

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 α)

Equations

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

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

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.

Equations

• HahnSeries.SummableFamily.lsum = { toFun := HahnSeries.SummableFamily.hsum, map_add' := ⋯, map_smul' := ⋯ }

@[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}

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.

Equations

• s.mul t = { toFun := fun (a : α × β) => s a.1 * t a.2, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[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} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {β : Type u_7} (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} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {β : Type u_7} (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

@[deprecated HahnSeries.SummableFamily.coeff_hsum_mul (since := "2025-01-31")]

theorem HahnSeries.SummableFamily.mul_coeff {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {β : Type u_7} (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

Alias of HahnSeries.SummableFamily.coeff_hsum_mul.

theorem HahnSeries.SummableFamily.hsum_mul {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Semiring R] {β : Type u_7} (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} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_7} (f : α →₀ HahnSeries Γ R) : SummableFamily Γ R α

A family with only finitely many nonzero elements is summable.

Equations

• HahnSeries.SummableFamily.ofFinsupp f = { toFun := ⇑f, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• s.embDomain f = { toFun := fun (b : β) => if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

theorem HahnSeries.SummableFamily.embDomain_apply {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_7} {β : Type u_8} (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} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_7} {β : Type u_8} (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} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_7} {β : Type u_8} (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} [PartialOrder Γ] [AddCommMonoid R] {α : Type u_7} {β : Type u_8} (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

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

The powers of an element of positive valuation form a summable family.

Equations

• HahnSeries.SummableFamily.powers x hx = { toFun := fun (n : ℕ) => x ^ n, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[simp]

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

@[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 hx) = 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 hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = powers x hx - ofFinsupp (Finsupp.single 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 hx).hsum = 1

theorem HahnSeries.one_minus_single_neg_mul {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [CommRing R] {x y : HahnSeries Γ R} {r : R} (hr : r * x.leadingCoeff = 1) (hxy : x = y + (single x.order) x.leadingCoeff) (hxo : IsAddUnit x.order) : 1 - (single hxo.addUnit.neg) r * x = -((single hxo.addUnit.neg) r * y)

theorem HahnSeries.unit_aux {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [CommRing R] (x : HahnSeries Γ R) {r : R} (hr : r * x.leadingCoeff = 1) (hxo : IsAddUnit x.order) : 0 < (1 - (single hxo.addUnit.neg) r * x).orderTop

theorem HahnSeries.isUnit_of_isUnit_leadingCoeff_AddUnitOrder {Γ : Type u_1} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [CommRing R] {x : HahnSeries Γ R} (hx : IsUnit x.leadingCoeff) (hxo : IsAddUnit x.order) : IsUnit 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

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

Equations

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