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]

source

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

Instances For

source

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

FunLike (SummableFamily Γ R α) α (HahnSeries Γ R)

Equations

source

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

source

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

source

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

source

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

Function.Injective DFunLike.coe

source

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

source

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

source

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

Add (SummableFamily Γ R α)

Equations

source

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

Zero (SummableFamily Γ R α)

Equations

source

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

Inhabited (SummableFamily Γ R α)

Equations

source

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

source

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

source

@[simp]

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

⇑0 = 0

source

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

0 a = 0

source

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

Equations

source

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

source

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

source

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

AddCommMonoid (SummableFamily Γ R α)

Equations

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

@[simp]

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

hsum 0 = 0

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

Neg (SummableFamily Γ R α)

Equations

source

@[simp]

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

⇑(-s) = -⇑s

source

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

source

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

Sub (SummableFamily Γ R α)

Equations

source

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

source

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

source

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

AddCommGroup (SummableFamily Γ R α)

Equations

source

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

source

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

source

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

source

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}

source

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

Instances For

source

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

source

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

source

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

source

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)

source

instance HahnSeries.SummableFamily.instSMulOfSMulWithZero {Γ : 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

source

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)

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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}

source

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

Instances For

source

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

source

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

source

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

source

@[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} {β : 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

Alias of HahnSeries.SummableFamily.coeff_hsum_mul.

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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

source

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

source

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)

source

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

source

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}

source

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

source

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.

Equations

Instances For

source

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

source

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

source

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

source

@[simp]

theorem HahnSeries.SummableFamily.powers_zero {Γ : Type u_1} {R : Type u_3} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] :

powers 0 = single 0 1

source

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

source

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 (Finsupp.single 0 1)

source

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

source

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)

source

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

source

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

source

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

source

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

DivInvMonoid (HahnSeries Γ R)

Equations

source

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

source

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

source

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

source

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

Field (HahnSeries Γ R)

Equations

source

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

Documentation

Mathlib.RingTheory.HahnSeries.Summable

Summable families of Hahn Series #

Main Definitions #

Main results #

TODO #

References #