Documentation

Mathlib.RingTheory.HahnSeries.Basic

Hahn Series #

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered. With further structure on R and Γ, we can add further structure on HahnSeries Γ R, with the most studied case being when Γ is a linearly ordered abelian group and R is a field, in which case HahnSeries Γ R is a valued field, with value group Γ. These generalize Laurent series (with value group ℤ), and Laurent series are implemented that way in the file Mathlib/RingTheory/LaurentSeries.lean.

Main Definitions #

If Γ is ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are partially well-ordered.
support x is the subset of Γ whose coefficients are nonzero.
single a r is the Hahn series which has coefficient r at a and zero otherwise.
orderTop x is a minimal element of WithTop Γ where x has a nonzero coefficient if x ≠ 0, and is ⊤ when x = 0.
order x is a minimal element of Γ where x has a nonzero coefficient if x ≠ 0, and is zero when x = 0.
map takes each coefficient of a Hahn series to its target under a zero-preserving map.
embDomain preserves coefficients, but embeds the index set Γ in a larger poset.

References #

J. van der Hoeven, Operators on Generalized Power Series

structure HahnSeries (Γ : Type u_1) (R : Type u_2) [PartialOrder Γ] [Zero R] :

Type (max u_1 u_2)

If Γ is linearly ordered and R has zero, then HahnSeries Γ R consists of formal series over Γ with coefficients in R, whose supports are well-founded.

coeff : Γ → R
The coefficient function of a Hahn Series.
isPWO_support' : (Function.support self.coeff).IsPWO

Instances For

theorem HahnSeries.ext_iff {Γ : Type u_1} {R : Type u_2} {inst✝ : PartialOrder Γ} {inst✝¹ : Zero R} {x y : HahnSeries Γ R} :

x = y ↔ x.coeff = y.coeff

theorem HahnSeries.ext {Γ : Type u_1} {R : Type u_2} {inst✝ : PartialOrder Γ} {inst✝¹ : Zero R} {x y : HahnSeries Γ R} (coeff : x.coeff = y.coeff) :

x = y

theorem HahnSeries.coeff_injective {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

Function.Injective coeff

@[simp]

theorem HahnSeries.coeff_inj {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x y : HahnSeries Γ R} :

x.coeff = y.coeff ↔ x = y

def HahnSeries.support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

Set Γ

The support of a Hahn series is just the set of indices whose coefficients are nonzero. Notably, it is well-founded.

Equations

x.support = Function.support x.coeff

Instances For

@[simp]

theorem HahnSeries.isPWO_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

x.support.IsPWO

@[simp]

theorem HahnSeries.isWF_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

@[simp]

theorem HahnSeries.mem_support {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) (a : Γ) :

a ∈ x.support ↔ x.coeff a ≠ 0

instance HahnSeries.instZero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

Zero (HahnSeries Γ R)

Equations

HahnSeries.instZero = { zero := { coeff := 0, isPWO_support' := ⋯ } }

instance HahnSeries.instInhabited {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

Inhabited (HahnSeries Γ R)

Equations

HahnSeries.instInhabited = { default := 0 }

instance HahnSeries.instSubsingleton {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Subsingleton R] :

Subsingleton (HahnSeries Γ R)

theorem HahnSeries.coeff_zero' {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

@[simp]

theorem HahnSeries.coeff_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} :

coeff 0 a = 0

@[simp]

theorem HahnSeries.coeff_fun_eq_zero_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.coeff = 0 ↔ x = 0

theorem HahnSeries.ne_zero_of_coeff_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) :

x ≠ 0

@[simp]

theorem HahnSeries.support_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

support 0 = ∅

@[simp]

theorem HahnSeries.support_nonempty_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.support.Nonempty ↔ x ≠ 0

@[simp]

theorem HahnSeries.support_eq_empty_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.support = ∅ ↔ x = 0

def HahnSeries.map {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] [Zero S] (x : HahnSeries Γ R) {F : Type u_5} [FunLike F R S] [ZeroHomClass F R S] (f : F) :

HahnSeries Γ S

The map of Hahn series induced by applying a zero-preserving map to each coefficient.

Equations

x.map f = { coeff := fun (g : Γ) => f (x.coeff g), isPWO_support' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.map_coeff {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] [Zero S] (x : HahnSeries Γ R) {F : Type u_5} [FunLike F R S] [ZeroHomClass F R S] (f : F) (g : Γ) :

(x.map f).coeff g = f (x.coeff g)

@[simp]

theorem HahnSeries.map_zero {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] [Zero S] (f : ZeroHom R S) :

map 0 f = 0

def HahnSeries.ofIterate {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) :

HahnSeries (Lex (Γ × Γ')) R

Change a HahnSeries with coefficients in HahnSeries to a HahnSeries on the Lex product.

Equations

x.ofIterate = { coeff := fun (g : Lex (Γ × Γ')) => (x.coeff g.1).coeff g.2, isPWO_support' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.mk_eq_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (f : Γ → R) (h : (Function.support f).IsPWO) :

{ coeff := f, isPWO_support' := h } = 0 ↔ f = 0

def HahnSeries.toIterate {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries (Lex (Γ × Γ')) R) :

HahnSeries Γ (HahnSeries Γ' R)

Change a Hahn series on a lex product to a Hahn series with coefficients in a Hahn series.

Equations

x.toIterate = { coeff := fun (g : Γ) => { coeff := fun (g' : Γ') => x.coeff (g, g'), isPWO_support' := ⋯ }, isPWO_support' := ⋯ }

Instances For

def HahnSeries.iterateEquiv {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] :

HahnSeries Γ (HahnSeries Γ' R) ≃ HahnSeries (Lex (Γ × Γ')) R

The equivalence between iterated Hahn series and Hahn series on the lex product.

Equations

HahnSeries.iterateEquiv = { toFun := HahnSeries.ofIterate, invFun := HahnSeries.toIterate, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem HahnSeries.iterateEquiv_apply {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries Γ (HahnSeries Γ' R)) :

iterateEquiv x = x.ofIterate

@[simp]

theorem HahnSeries.iterateEquiv_symm_apply {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (x : HahnSeries (Lex (Γ × Γ')) R) :

iterateEquiv.symm x = x.toIterate

def HahnSeries.single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (a : Γ) :

ZeroHom R (HahnSeries Γ R)

single a r is the Hahn series which has coefficient r at a and zero otherwise.

Equations

HahnSeries.single a = { toFun := fun (r : R) => { coeff := Pi.single a r, isPWO_support' := ⋯ }, map_zero' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.coeff_single_same {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (a : Γ) (r : R) :

((single a) r).coeff a = r

@[simp]

theorem HahnSeries.coeff_single_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a b : Γ} {r : R} (h : b ≠ a) :

((single a) r).coeff b = 0

theorem HahnSeries.coeff_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a b : Γ} {r : R} :

((single a) r).coeff b = if b = a then r else 0

@[simp]

theorem HahnSeries.support_single_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) :

((single a) r).support = {a}

theorem HahnSeries.support_single_subset {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :

((single a) r).support ⊆ {a}

theorem HahnSeries.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} {b : Γ} (h : b ∈ ((single a) r).support) :

b = a

theorem HahnSeries.single_eq_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} :

(single a) 0 = 0

theorem HahnSeries.single_injective {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (a : Γ) :

Function.Injective ⇑(single a)

theorem HahnSeries.single_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) :

(single a) r ≠ 0

@[simp]

theorem HahnSeries.single_eq_zero_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :

(single a) r = 0 ↔ r = 0

@[simp]

theorem HahnSeries.map_single {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} [Zero S] (f : ZeroHom R S) :

((single a) r).map f = (single a) (f r)

instance HahnSeries.instNontrivialOfNonempty {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Nonempty Γ] [Nontrivial R] :

Nontrivial (HahnSeries Γ R)

def HahnSeries.orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

The orderTop of a Hahn series x is a minimal element of WithTop Γ where x has a nonzero coefficient if x ≠ 0, and is ⊤ when x = 0.

Equations

x.orderTop = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)

Instances For

@[simp]

theorem HahnSeries.orderTop_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

orderTop 0 = ⊤

@[simp]

theorem HahnSeries.orderTop_of_subsingleton {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} [Subsingleton R] :

x.orderTop = ⊤

@[deprecated HahnSeries.orderTop_of_subsingleton (since := "2025-08-19")]

theorem HahnSeries.orderTop_of_Subsingleton {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} [Subsingleton R] :

x.orderTop = ⊤

Alias of HahnSeries.orderTop_of_subsingleton.

theorem HahnSeries.orderTop_of_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.orderTop = ↑(⋯.min ⋯)

@[deprecated HahnSeries.orderTop_of_ne_zero (since := "2025-08-19")]

theorem HahnSeries.orderTop_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.orderTop = ↑(⋯.min ⋯)

Alias of HahnSeries.orderTop_of_ne_zero.

@[simp]

theorem HahnSeries.orderTop_eq_top {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.orderTop = ⊤ ↔ x = 0

@[simp]

theorem HahnSeries.orderTop_lt_top {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.orderTop < ⊤ ↔ x ≠ 0

theorem HahnSeries.orderTop_ne_top {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.orderTop ≠ ⊤ ↔ x ≠ 0

@[deprecated HahnSeries.orderTop_eq_top (since := "2025-08-19")]

theorem HahnSeries.orderTop_eq_top_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.orderTop = ⊤ ↔ x = 0

Alias of HahnSeries.orderTop_eq_top.

@[deprecated HahnSeries.orderTop_ne_top (since := "2025-08-19")]

theorem HahnSeries.ne_zero_iff_orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x ≠ 0 ↔ x.orderTop ≠ ⊤

theorem HahnSeries.orderTop_eq_of_le {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (hg : g ∈ x.support) (hx : ∀ g' ∈ x.support, g ≤ g') :

x.orderTop = ↑g

theorem HahnSeries.untop_orderTop_of_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.orderTop.untop ⋯ = ⋯.min ⋯

theorem HahnSeries.coeff_orderTop_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {g : Γ} (hg : x.orderTop = ↑g) :

x.coeff g ≠ 0

theorem HahnSeries.orderTop_le_of_coeff_ne_zero {R : Type u_3} [Zero R] {Γ : Type u_5} [LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) :

x.orderTop ≤ ↑g

@[simp]

theorem HahnSeries.orderTop_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} (h : r ≠ 0) :

((single a) r).orderTop = ↑a

theorem HahnSeries.orderTop_single_le {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :

↑a ≤ ((single a) r).orderTop

theorem HahnSeries.lt_orderTop_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {r : R} {g g' : Γ} (hgg' : g < g') :

↑g < ((single g') r).orderTop

theorem HahnSeries.coeff_eq_zero_of_lt_orderTop {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} {i : Γ} (hi : ↑i < x.orderTop) :

x.coeff i = 0

def HahnSeries.leadingCoeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (x : HahnSeries Γ R) :

R

A leading coefficient of a Hahn series is the coefficient of a lowest-order nonzero term, or zero if the series vanishes.

Equations

x.leadingCoeff = WithTop.recTopCoe 0 x.coeff x.orderTop

Instances For

@[simp]

theorem HahnSeries.leadingCoeff_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

leadingCoeff 0 = 0

theorem HahnSeries.leadingCoeff_of_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.leadingCoeff = x.coeff (x.orderTop.untop ⋯)

@[deprecated HahnSeries.leadingCoeff_of_ne_zero (since := "2025-08-19")]

theorem HahnSeries.leadingCoeff_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.leadingCoeff = x.coeff (x.orderTop.untop ⋯)

Alias of HahnSeries.leadingCoeff_of_ne_zero.

@[simp]

theorem HahnSeries.leadingCoeff_eq_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.leadingCoeff = 0 ↔ x = 0

theorem HahnSeries.leadingCoeff_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.leadingCoeff ≠ 0 ↔ x ≠ 0

@[deprecated HahnSeries.leadingCoeff_eq_zero (since := "2025-08-19")]

theorem HahnSeries.leadingCoeff_eq_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.leadingCoeff = 0 ↔ x = 0

Alias of HahnSeries.leadingCoeff_eq_zero.

@[deprecated HahnSeries.leadingCoeff_ne_zero (since := "2025-08-19")]

theorem HahnSeries.leadingCoeff_ne_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} :

x.leadingCoeff ≠ 0 ↔ x ≠ 0

Alias of HahnSeries.leadingCoeff_ne_zero.

@[simp]

theorem HahnSeries.leadingCoeff_of_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} :

((single a) r).leadingCoeff = r

theorem HahnSeries.coeff_untop_eq_leadingCoeff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} (hx : x.orderTop ≠ ⊤) :

x.coeff (x.orderTop.untop hx) = x.leadingCoeff

def HahnSeries.order {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] (x : HahnSeries Γ R) :

Γ

The order of a nonzero Hahn series x is a minimal element of Γ where x has a nonzero coefficient, the order of 0 is 0.

Equations

x.order = if h : x = 0 then 0 else ⋯.min ⋯

Instances For

@[simp]

theorem HahnSeries.order_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] :

theorem HahnSeries.order_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.order = ⋯.min ⋯

theorem HahnSeries.order_eq_orderTop_of_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} [Zero Γ] (hx : x ≠ 0) :

↑x.order = x.orderTop

@[deprecated HahnSeries.order_eq_orderTop_of_ne_zero (since := "2025-08-19")]

theorem HahnSeries.order_eq_orderTop_of_ne {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {x : HahnSeries Γ R} [Zero Γ] (hx : x ≠ 0) :

↑x.order = x.orderTop

Alias of HahnSeries.order_eq_orderTop_of_ne_zero.

theorem HahnSeries.coeff_order_ne_zero {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) :

x.coeff x.order ≠ 0

theorem HahnSeries.order_le_of_coeff_ne_zero {R : Type u_3} [Zero R] {Γ : Type u_5} [Zero Γ] [LinearOrder Γ] {x : HahnSeries Γ R} {g : Γ} (h : x.coeff g ≠ 0) :

@[simp]

theorem HahnSeries.order_single {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] {a : Γ} {r : R} [Zero Γ] (h : r ≠ 0) :

((single a) r).order = a

theorem HahnSeries.coeff_eq_zero_of_lt_order {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} {i : Γ} (hi : i < x.order) :

x.coeff i = 0

theorem HahnSeries.zero_lt_orderTop_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : x ≠ 0) :

0 < x.orderTop ↔ 0 < x.order

theorem HahnSeries.zero_lt_orderTop_of_order {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} (hx : 0 < x.order) :

theorem HahnSeries.zero_le_orderTop_iff {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} :

0 ≤ x.orderTop ↔ 0 ≤ x.order

theorem HahnSeries.leadingCoeff_eq {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] [Zero Γ] {x : HahnSeries Γ R} :

x.leadingCoeff = x.coeff x.order

def HahnSeries.ofFinsupp {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] :

ZeroHom (Γ →₀ R) (HahnSeries Γ R)

Create a HahnSeries with a Finsupp as coefficients.

Equations

HahnSeries.ofFinsupp = { toFun := fun (f : Γ →₀ R) => { coeff := ⇑f, isPWO_support' := ⋯ }, map_zero' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.coeff_ofFinsupp {Γ : Type u_1} {R : Type u_3} [PartialOrder Γ] [Zero R] (f : Γ →₀ R) (a : Γ) :

(ofFinsupp f).coeff a = f a

def HahnSeries.embDomain {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] (f : Γ ↪o Γ') :

HahnSeries Γ R → HahnSeries Γ' R

Extends the domain of a HahnSeries by an OrderEmbedding.

Equations

HahnSeries.embDomain f x = { coeff := fun (b : Γ') => if h : b ∈ ⇑f '' x.support then x.coeff (Classical.choose h) else 0, isPWO_support' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.embDomain_coeff {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {a : Γ} :

(embDomain f x).coeff (f a) = x.coeff a

@[simp]

theorem HahnSeries.embDomain_mk_coeff {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ → Γ'} (hfi : Function.Injective f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') {x : HahnSeries Γ R} {a : Γ} :

(embDomain { toFun := f, inj' := hfi, map_rel_iff' := ⋯ } x).coeff (f a) = x.coeff a

theorem HahnSeries.embDomain_notin_image_support {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ ⇑f '' x.support) :

(embDomain f x).coeff b = 0

theorem HahnSeries.support_embDomain_subset {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :

(embDomain f x).support ⊆ ⇑f '' x.support

theorem HahnSeries.embDomain_notin_range {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ Set.range ⇑f) :

(embDomain f x).coeff b = 0

@[simp]

theorem HahnSeries.embDomain_zero {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} :

embDomain f 0 = 0

@[simp]

theorem HahnSeries.embDomain_single {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} {g : Γ} {r : R} :

embDomain f ((single g) r) = (single (f g)) r

theorem HahnSeries.embDomain_injective {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [PartialOrder Γ] [Zero R] [PartialOrder Γ'] {f : Γ ↪o Γ'} :

Function.Injective (embDomain f)

@[simp]

theorem HahnSeries.orderTop_embDomain {Γ' : Type u_2} {R : Type u_3} [Zero R] [PartialOrder Γ'] {Γ : Type u_5} [LinearOrder Γ] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :

(embDomain f x).orderTop = WithTop.map (⇑f) x.orderTop

theorem HahnSeries.forallLTEqZero_supp_BddBelow {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] (f : Γ → R) (n : Γ) (hn : ∀ m < n, f m = 0) :

BddBelow (Function.support f)

theorem HahnSeries.BddBelow_zero {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [Nonempty Γ] :

BddBelow (Function.support 0)

theorem HahnSeries.suppBddBelow_supp_PWO {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R) (hf : BddBelow (Function.support f)) :

(Function.support f).IsPWO

def HahnSeries.ofSuppBddBelow {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R) (hf : BddBelow (Function.support f)) :

HahnSeries Γ R

Construct a Hahn series from any function whose support is bounded below.

Equations

HahnSeries.ofSuppBddBelow f hf = { coeff := f, isPWO_support' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.ofSuppBddBelow_coeff {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] (f : Γ → R) (hf : BddBelow (Function.support f)) (a✝ : Γ) :

(ofSuppBddBelow f hf).coeff a✝ = f a✝

@[simp]

theorem HahnSeries.zero_ofSuppBddBelow {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] [Nonempty Γ] :

ofSuppBddBelow 0 ⋯ = 0

theorem HahnSeries.order_ofForallLtEqZero {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] [LocallyFiniteOrder Γ] [Zero Γ] (f : Γ → R) (hf : f ≠ 0) (n : Γ) (hn : ∀ m < n, f m = 0) :

n ≤ (ofSuppBddBelow f ⋯).order

def HahnSeries.truncLT {Γ : Type u_1} {R : Type u_3} [Zero R] [PartialOrder Γ] [DecidableLT Γ] (c : Γ) :

ZeroHom (HahnSeries Γ R) (HahnSeries Γ R)

Zeroes out coefficients of a HahnSeries at indices not less than c.

Equations

HahnSeries.truncLT c = { toFun := fun (x : HahnSeries Γ R) => { coeff := fun (i : Γ) => if i < c then x.coeff i else 0, isPWO_support' := ⋯ }, map_zero' := ⋯ }

Instances For

@[simp]

theorem HahnSeries.coeff_truncLT {Γ : Type u_1} {R : Type u_3} [Zero R] [PartialOrder Γ] [DecidableLT Γ] (c : Γ) (x : HahnSeries Γ R) (i : Γ) :

((truncLT c) x).coeff i = if i < c then x.coeff i else 0

theorem HahnSeries.coeff_truncLT_of_lt {Γ : Type u_1} {R : Type u_3} [Zero R] [PartialOrder Γ] [DecidableLT Γ] {c i : Γ} (h : i < c) (x : HahnSeries Γ R) :

((truncLT c) x).coeff i = x.coeff i

theorem HahnSeries.coeff_truncLT_of_le {Γ : Type u_1} {R : Type u_3} [Zero R] [LinearOrder Γ] {c i : Γ} (h : c ≤ i) (x : HahnSeries Γ R) :

((truncLT c) x).coeff i = 0