mathlib documentation

ring_theory.hahn_series

Hahn Series #

Main Definitions #

TODO #

theorem hahn_series.ext {Γ : Type u_1} {R : Type u_2} {_inst_1 : linear_order Γ} {_inst_2 : has_zero R} (x y : hahn_series Γ R) (h : x.coeff = y.coeff) :
x = y
theorem hahn_series.ext_iff {Γ : Type u_1} {R : Type u_2} {_inst_1 : linear_order Γ} {_inst_2 : has_zero R} (x y : hahn_series Γ R) :
x = y x.coeff = y.coeff
@[ext]
structure hahn_series (Γ : Type u_1) (R : Type u_2) [linear_order Γ] [has_zero R] :
Type (max u_1 u_2)

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

def hahn_series.support {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] (x : hahn_series Γ R) :
set Γ

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

Equations
@[simp]
theorem hahn_series.is_wf_support {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] (x : hahn_series Γ R) :
@[simp]
theorem hahn_series.mem_support {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] (x : hahn_series Γ R) (a : Γ) :
a x.support x.coeff a 0
@[instance]
def hahn_series.has_zero {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] :
Equations
@[instance]
def hahn_series.inhabited {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] :
Equations
@[instance]
def hahn_series.subsingleton {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] [subsingleton R] :
@[simp]
theorem hahn_series.zero_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a : Γ} :
0.coeff a = 0
@[simp]
theorem hahn_series.support_zero {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] :
@[simp]
theorem hahn_series.support_nonempty_iff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {x : hahn_series Γ R} :
def hahn_series.single {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] (a : Γ) :

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

Equations
@[simp]
theorem hahn_series.single_coeff_same {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] (a : Γ) (r : R) :
@[simp]
theorem hahn_series.single_coeff_of_ne {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a b : Γ} {r : R} (h : b a) :
theorem hahn_series.single_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a b : Γ} {r : R} :
((hahn_series.single a) r).coeff b = ite (b = a) r 0
@[simp]
theorem hahn_series.support_single_of_ne {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a : Γ} {r : R} (h : r 0) :
theorem hahn_series.support_single_subset {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a : Γ} {r : R} :
theorem hahn_series.eq_of_mem_support_single {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a : Γ} {r : R} {b : Γ} (h : b ((hahn_series.single a) r).support) :
b = a
@[simp]
theorem hahn_series.single_eq_zero {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {a : Γ} :
@[instance]
def hahn_series.nontrivial {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] [nonempty Γ] [nontrivial R] :
theorem hahn_series.coeff_min_ne_zero {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [has_zero R] {x : hahn_series Γ R} (hx : x 0) :
x.coeff (_.min _) 0
@[instance]
def hahn_series.has_add {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] :
Equations
@[simp]
theorem hahn_series.add_coeff' {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] {x y : hahn_series Γ R} :
(x + y).coeff = x.coeff + y.coeff
theorem hahn_series.add_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] {x y : hahn_series Γ R} {a : Γ} :
(x + y).coeff a = x.coeff a + y.coeff a
theorem hahn_series.support_add_subset {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] {x y : hahn_series Γ R} :
@[simp]
theorem hahn_series.single.add_monoid_hom_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] (a : Γ) (ᾰ : R) :
def hahn_series.single.add_monoid_hom {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] (a : Γ) :

single as an additive monoid/group homomorphism

Equations
@[simp]
theorem hahn_series.coeff.add_monoid_hom_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] (g : Γ) (f : hahn_series Γ R) :
def hahn_series.coeff.add_monoid_hom {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_monoid R] (g : Γ) :

coeff g as an additive monoid/group homomorphism

Equations
@[instance]
def hahn_series.add_group {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_group R] :
Equations
@[simp]
theorem hahn_series.neg_coeff' {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_group R] {x : hahn_series Γ R} :
theorem hahn_series.neg_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_group R] {x : hahn_series Γ R} {a : Γ} :
(-x).coeff a = -x.coeff a
@[simp]
theorem hahn_series.support_neg {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_group R] {x : hahn_series Γ R} :
@[simp]
theorem hahn_series.sub_coeff' {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_group R] {x y : hahn_series Γ R} :
(x - y).coeff = x.coeff - y.coeff
theorem hahn_series.sub_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_group R] {x y : hahn_series Γ R} {a : Γ} :
(x - y).coeff a = x.coeff a - y.coeff a
@[instance]
def hahn_series.has_scalar {Γ : Type u_1} {R : Type u_2} [linear_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] :
Equations
@[simp]
theorem hahn_series.smul_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] {r : R} {x : hahn_series Γ V} {a : Γ} :
(r x).coeff a = r x.coeff a
@[instance]
def hahn_series.is_scalar_tower {Γ : Type u_1} {R : Type u_2} [linear_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] {S : Type u_4} [monoid S] [distrib_mul_action S V] [has_scalar R S] [is_scalar_tower R S V] :
@[instance]
def hahn_series.smul_comm_class {Γ : Type u_1} {R : Type u_2} [linear_order Γ] {V : Type u_3} [monoid R] [add_monoid V] [distrib_mul_action R V] {S : Type u_4} [monoid S] [distrib_mul_action S V] [smul_comm_class R S V] :
@[simp]
theorem hahn_series.single.linear_map_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [semiring R] (a : Γ) (ᾰ : R) :
def hahn_series.single.linear_map {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [semiring R] (a : Γ) :

single as a linear map

Equations
def hahn_series.coeff.linear_map {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [semiring R] (g : Γ) :

coeff g as a linear map

Equations
@[simp]
theorem hahn_series.coeff.linear_map_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [semiring R] (g : Γ) (ᾰ : hahn_series Γ R) :
@[instance]
def hahn_series.has_one {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [has_zero R] [has_one R] :
Equations
@[simp]
theorem hahn_series.one_coeff {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [has_zero R] [has_one R] {a : Γ} :
1.coeff a = ite (a = 0) 1 0
@[simp]
theorem hahn_series.single_zero_one {R : Type u_2} [has_zero R] [has_one R] :
@[simp]
theorem hahn_series.support_one {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] [nontrivial R] :
1.support = {0}
@[instance]
def hahn_series.has_mul {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] :
Equations
@[simp]
theorem hahn_series.mul_coeff {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {x y : hahn_series Γ R} {a : Γ} :
(x * y).coeff a = ∑ (ij : Γ × Γ) in finset.add_antidiagonal _ _ a, (x.coeff ij.fst) * y.coeff ij.snd
theorem hahn_series.mul_coeff_right' {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {x y : hahn_series Γ R} {a : Γ} {s : set Γ} (hs : s.is_wf) (hys : y.support s) :
(x * y).coeff a = ∑ (ij : Γ × Γ) in finset.add_antidiagonal _ hs a, (x.coeff ij.fst) * y.coeff ij.snd
theorem hahn_series.mul_coeff_left' {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {x y : hahn_series Γ R} {a : Γ} {s : set Γ} (hs : s.is_wf) (hxs : x.support s) :
(x * y).coeff a = ∑ (ij : Γ × Γ) in finset.add_antidiagonal hs _ a, (x.coeff ij.fst) * y.coeff ij.snd
theorem hahn_series.single_mul_coeff_add {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} {a b : Γ} :
(((hahn_series.single b) r) * x).coeff (a + b) = r * x.coeff a
theorem hahn_series.mul_single_coeff_add {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} {a b : Γ} :
(x * (hahn_series.single b) r).coeff (a + b) = (x.coeff a) * r
@[simp]
theorem hahn_series.mul_single_zero_coeff {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} {a : Γ} :
(x * (hahn_series.single 0) r).coeff a = (x.coeff a) * r
theorem hahn_series.single_zero_mul_coeff {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} {a : Γ} :
(((hahn_series.single 0) r) * x).coeff a = r * x.coeff a
@[simp]
theorem hahn_series.single_zero_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} :
@[simp]
theorem hahn_series.mul_coeff_min_add_min {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {x y : hahn_series Γ R} (hx : x 0) (hy : y 0) :
(x * y).coeff (_.min _ + _.min _) = (x.coeff (_.min _)) * y.coeff (_.min _)
@[instance]
def hahn_series.semiring {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] :
Equations
@[simp]
theorem hahn_series.single_mul_single {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {a b : Γ} {r s : R} :
@[simp]
theorem hahn_series.C_apply {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] (ᾰ : R) :
def hahn_series.C {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] :

C a is the constant Hahn Series a. C is provided as a ring homomorphism.

Equations
@[simp]
theorem hahn_series.C_zero {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] :
@[simp]
theorem hahn_series.C_one {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] :
theorem hahn_series.C_mul_eq_smul {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [semiring R] {r : R} {x : hahn_series Γ R} :
theorem hahn_series.algebra_map_apply {Γ : Type u_1} {R : Type u_2} [linear_ordered_cancel_add_comm_monoid Γ] [comm_semiring R] {A : Type u_3} [semiring A] [algebra R A] {r : R} :

The ring hahn_series ℕ R is isomorphic to power_series R.

Equations
def hahn_series.add_val (Γ : Type u_1) (R : Type u_2) [linear_ordered_add_comm_group Γ] [integral_domain R] [nontrivial R] :

The additive valuation on hahn_series Γ R, returning the smallest index at which a Hahn Series has a nonzero coefficient, or for the 0 series.

Equations
theorem hahn_series.add_val_apply {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [integral_domain R] [nontrivial R] {x : hahn_series Γ R} :
(hahn_series.add_val Γ R) x = dite (x = 0) (λ (h : x = 0), ) (λ (h : ¬x = 0), (_.min _))
@[simp]
theorem hahn_series.add_val_apply_of_ne {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [integral_domain R] [nontrivial R] {x : hahn_series Γ R} (hx : x 0) :
structure hahn_series.summable_family (Γ : Type u_1) (R : Type u_2) [linear_order Γ] [add_comm_monoid R] (α : Type u_3) :
Type (max u_1 u_2 u_3)

An infinite family of Hahn series which has a formal coefficient-wise sum. The requirements for this are that the union of the supports of the series is well-founded, and that only finitely many series are nonzero at any given coefficient.

theorem hahn_series.summable_family.is_wf_Union_support {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} (s : hahn_series.summable_family Γ R α) :
(⋃ (a : α), (s a).support).is_wf
@[simp]
theorem hahn_series.summable_family.mem_co_support {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} {a : α} {g : Γ} :
a s.co_support g (s a).coeff g 0
theorem hahn_series.summable_family.coe_injective {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} :
@[ext]
theorem hahn_series.summable_family.ext {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} (h : ∀ (a : α), s a = t a) :
s = t
@[instance]
def hahn_series.summable_family.has_add {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
@[instance]
def hahn_series.summable_family.has_zero {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
@[instance]
def hahn_series.summable_family.inhabited {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.coe_add {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} :
(s + t) = s + t
theorem hahn_series.summable_family.add_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} {a : α} :
(s + t) a = s a + t a
@[simp]
theorem hahn_series.summable_family.coe_zero {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} :
0 = 0
theorem hahn_series.summable_family.zero_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {a : α} :
0 a = 0
@[instance]
def hahn_series.summable_family.add_comm_monoid {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} :
Equations
def hahn_series.summable_family.hsum {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} (s : hahn_series.summable_family Γ R α) :

The infinite sum of a summable_family of Hahn series.

Equations
@[simp]
theorem hahn_series.summable_family.hsum_coeff {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} {g : Γ} :
s.hsum.coeff g = ∑ (i : α) in s.co_support g, (s i).coeff g
theorem hahn_series.summable_family.support_hsum_subset {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} :
s.hsum.support ⋃ (a : α), (s a).support
theorem hahn_series.summable_family.co_support_add_subset {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} {g : Γ} :
@[simp]
theorem hahn_series.summable_family.hsum_add {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} :
(s + t).hsum = s.hsum + t.hsum
@[instance]
def hahn_series.summable_family.add_comm_group {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_group R] {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.coe_neg {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_group R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} :
theorem hahn_series.summable_family.neg_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_group R] {α : Type u_3} {s : hahn_series.summable_family Γ R α} {a : α} :
(-s) a = -s a
theorem hahn_series.summable_family.coe_sub {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_group R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} :
(s - t) = s - t
theorem hahn_series.summable_family.sub_apply {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_group R] {α : Type u_3} {s t : hahn_series.summable_family Γ R α} {a : α} :
(s - t) a = s a - t a
@[instance]
def hahn_series.summable_family.has_scalar {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [semiring R] {α : Type u_3} :
Equations
@[simp]
theorem hahn_series.summable_family.smul_apply {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [semiring R] {α : Type u_3} {x : hahn_series Γ R} {s : hahn_series.summable_family Γ R α} {a : α} :
(x s) a = x * s a
@[simp]
theorem hahn_series.summable_family.hsum_smul {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [semiring R] {α : Type u_3} {x : hahn_series Γ R} {s : hahn_series.summable_family Γ R α} :
(x s).hsum = x * s.hsum
@[simp]
def hahn_series.summable_family.lsum {Γ : Type u_1} {R : Type u_2} [linear_ordered_add_comm_group Γ] [semiring R] {α : Type u_3} :

The summation of a summable_family as a linear_map.

Equations
def hahn_series.summable_family.of_finsupp {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} (f : α →₀ hahn_series Γ R) :

A family with only finitely many nonzero elements is summable.

Equations
@[simp]
theorem hahn_series.summable_family.coe_of_finsupp {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {f : α →₀ hahn_series Γ R} :
@[simp]
theorem hahn_series.summable_family.co_support_of_finsupp {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {f : α →₀ hahn_series Γ R} {g : Γ} :
@[simp]
theorem hahn_series.summable_family.hsum_of_finsupp {Γ : Type u_1} {R : Type u_2} [linear_order Γ] [add_comm_monoid R] {α : Type u_3} {f : α →₀ hahn_series Γ R} :