Hahn Series #
If Γ is ordered and R has zero, then hahn_series Γ 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 hahn_series Γ R, with the most studied case being when Γ is
a linearly ordered abelian group and R is a field, in which case hahn_series Γ 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 ring_theory/laurent_series.
Main Definitions #
- If
Γis ordered andRhas zero, thenhahn_series Γ Rconsists of formal series overΓwith coefficients inR, whose supports are partially well-ordered. - If
Ris a (commutative) additive monoid or group, then so ishahn_series Γ R. - If
Ris a (comm_)(semi)ring, then so ishahn_series Γ R. hahn_series.add_val Γ Rdefines anadd_valuationonhahn_series Γ RwhenΓis linearly ordered.- A
hahn_series.summable_familyis a family of Hahn series such that the union of their supports is well-founded and only finitely many are nonzero at any given coefficient. They have a formal sum,hahn_series.summable_family.hsum, which can be bundled as alinear_mapashahn_series.summable_family.lsum. Note that this is different fromsummablein the valuation topology, because there are topologically summable families that do not satisfy the axioms ofhahn_series.summable_family, and formally summable families whose sums do not converge topologically. - Laurent series over
Rare implemented ashahn_series ℤ Rin the filering_theory/laurent_series.
TODO #
- Build an API for the variable
X(defined to besingle 1 1 : hahn_series Γ R) in analogy toX : R[X]andX : power_series R
References #
theorem
hahn_series.ext
{Γ : Type u_1}
{R : Type u_2}
{_inst_1 : partial_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 : partial_order Γ}
{_inst_2 : has_zero R}
(x y : hahn_series Γ R) :
@[ext]
structure
hahn_series
(Γ : Type u_1)
(R : Type u_2)
[partial_order Γ]
[has_zero R] :
Type (max u_1 u_2)
- coeff : Γ → R
- is_pwo_support' : (function.support self.coeff).is_pwo
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.
@[simp]
theorem
hahn_series.coeff_inj
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{x y : hahn_series Γ R} :
def
hahn_series.support
{Γ : Type u_1}
{R : Type u_2}
[partial_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_pwo_support
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
(x : hahn_series Γ R) :
@[simp]
theorem
hahn_series.is_wf_support
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
(x : hahn_series Γ R) :
@[simp]
theorem
hahn_series.mem_support
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
(x : hahn_series Γ R)
(a : Γ) :
@[protected, instance]
def
hahn_series.has_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R] :
has_zero (hahn_series Γ R)
Equations
- hahn_series.has_zero = {zero := {coeff := 0, is_pwo_support' := _}}
@[protected, instance]
def
hahn_series.inhabited
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R] :
inhabited (hahn_series Γ R)
Equations
- hahn_series.inhabited = {default := 0}
@[protected, instance]
def
hahn_series.subsingleton
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[subsingleton R] :
subsingleton (hahn_series Γ R)
@[simp]
theorem
hahn_series.zero_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a : Γ} :
@[simp]
theorem
hahn_series.coeff_fun_eq_zero_iff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{x : hahn_series Γ R} :
theorem
hahn_series.ne_zero_of_coeff_ne_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{x : hahn_series Γ R}
{g : Γ}
(h : x.coeff g ≠ 0) :
x ≠ 0
@[simp]
@[simp]
theorem
hahn_series.support_nonempty_iff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{x : hahn_series Γ R} :
@[simp]
theorem
hahn_series.support_eq_empty_iff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{x : hahn_series Γ R} :
noncomputable
def
hahn_series.single
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
(a : Γ) :
zero_hom R (hahn_series Γ R)
single a r is the Hahn series which has coefficient r at a and zero otherwise.
Equations
- hahn_series.single a = {to_fun := λ (r : R), {coeff := pi.single a r, is_pwo_support' := _}, map_zero' := _}
@[simp]
theorem
hahn_series.single_coeff_same
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
(a : Γ)
(r : R) :
(⇑(hahn_series.single a) r).coeff a = r
@[simp]
theorem
hahn_series.single_coeff_of_ne
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a b : Γ}
{r : R}
(h : b ≠ a) :
(⇑(hahn_series.single a) r).coeff b = 0
theorem
hahn_series.single_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a b : Γ}
{r : R} :
@[simp]
theorem
hahn_series.support_single_of_ne
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a : Γ}
{r : R}
(h : r ≠ 0) :
(⇑(hahn_series.single a) r).support = {a}
theorem
hahn_series.support_single_subset
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a : Γ}
{r : R} :
(⇑(hahn_series.single a) r).support ⊆ {a}
theorem
hahn_series.eq_of_mem_support_single
{Γ : Type u_1}
{R : Type u_2}
[partial_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}
[partial_order Γ]
[has_zero R]
{a : Γ} :
⇑(hahn_series.single a) 0 = 0
theorem
hahn_series.single_injective
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
(a : Γ) :
theorem
hahn_series.single_ne_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a : Γ}
{r : R}
(h : r ≠ 0) :
⇑(hahn_series.single a) r ≠ 0
@[simp]
theorem
hahn_series.single_eq_zero_iff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a : Γ}
{r : R} :
⇑(hahn_series.single a) r = 0 ↔ r = 0
@[protected, instance]
def
hahn_series.nontrivial
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[nonempty Γ]
[nontrivial R] :
nontrivial (hahn_series Γ R)
noncomputable
def
hahn_series.order
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[has_zero Γ]
(x : hahn_series Γ 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.
@[simp]
theorem
hahn_series.order_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[has_zero Γ] :
theorem
hahn_series.order_of_ne
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[has_zero Γ]
{x : hahn_series Γ R}
(hx : x ≠ 0) :
theorem
hahn_series.coeff_order_ne_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[has_zero Γ]
{x : hahn_series Γ R}
(hx : x ≠ 0) :
theorem
hahn_series.order_le_of_coeff_ne_zero
{R : Type u_2}
[has_zero R]
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
{x : hahn_series Γ R}
{g : Γ}
(h : x.coeff g ≠ 0) :
@[simp]
theorem
hahn_series.order_single
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{a : Γ}
{r : R}
[has_zero Γ]
(h : r ≠ 0) :
(⇑(hahn_series.single a) r).order = a
theorem
hahn_series.coeff_eq_zero_of_lt_order
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
[has_zero Γ]
{x : hahn_series Γ R}
{i : Γ}
(hi : i < x.order) :
noncomputable
def
hahn_series.emb_domain
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
(f : Γ ↪o Γ') :
hahn_series Γ R → hahn_series Γ' R
Extends the domain of a hahn_series by an order_embedding.
@[simp]
theorem
hahn_series.emb_domain_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'}
{x : hahn_series Γ R}
{a : Γ} :
(hahn_series.emb_domain f x).coeff (⇑f a) = x.coeff a
@[simp]
theorem
hahn_series.emb_domain_mk_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ → Γ'}
(hfi : function.injective f)
(hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g')
{x : hahn_series Γ R}
{a : Γ} :
(hahn_series.emb_domain {to_embedding := {to_fun := f, inj' := hfi}, map_rel_iff' := hf} x).coeff (f a) = x.coeff a
theorem
hahn_series.emb_domain_notin_image_support
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'}
{x : hahn_series Γ R}
{b : Γ'}
(hb : b ∉ ⇑f '' x.support) :
(hahn_series.emb_domain f x).coeff b = 0
theorem
hahn_series.support_emb_domain_subset
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'}
{x : hahn_series Γ R} :
theorem
hahn_series.emb_domain_notin_range
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'}
{x : hahn_series Γ R}
{b : Γ'}
(hb : b ∉ set.range ⇑f) :
(hahn_series.emb_domain f x).coeff b = 0
@[simp]
theorem
hahn_series.emb_domain_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'} :
hahn_series.emb_domain f 0 = 0
@[simp]
theorem
hahn_series.emb_domain_single
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'}
{g : Γ}
{r : R} :
hahn_series.emb_domain f (⇑(hahn_series.single g) r) = ⇑(hahn_series.single (⇑f g)) r
theorem
hahn_series.emb_domain_injective
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[has_zero R]
{Γ' : Type u_3}
[partial_order Γ']
{f : Γ ↪o Γ'} :
@[protected, instance]
def
hahn_series.has_add
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R] :
has_add (hahn_series Γ R)
Equations
- hahn_series.has_add = {add := λ (x y : hahn_series Γ R), {coeff := x.coeff + y.coeff, is_pwo_support' := _}}
@[protected, instance]
def
hahn_series.add_monoid
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R] :
add_monoid (hahn_series Γ R)
Equations
- hahn_series.add_monoid = {add := has_add.add hahn_series.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec (add_zero_class.to_has_add (hahn_series Γ R)), nsmul_zero' := _, nsmul_succ' := _}
@[simp]
theorem
hahn_series.add_coeff'
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
{x y : hahn_series Γ R} :
theorem
hahn_series.add_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
{x y : hahn_series Γ R}
{a : Γ} :
theorem
hahn_series.support_add_subset
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
{x y : hahn_series Γ R} :
theorem
hahn_series.min_order_le_order_add
{R : Type u_2}
[add_monoid R]
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
{x y : hahn_series Γ R}
(hxy : x + y ≠ 0) :
@[simp]
theorem
hahn_series.single.add_monoid_hom_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
(a : Γ)
(ᾰ : R) :
⇑(hahn_series.single.add_monoid_hom a) ᾰ = (hahn_series.single a).to_fun ᾰ
noncomputable
def
hahn_series.single.add_monoid_hom
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
(a : Γ) :
R →+ hahn_series Γ R
single as an additive monoid/group homomorphism
Equations
- hahn_series.single.add_monoid_hom a = {to_fun := (hahn_series.single a).to_fun, map_zero' := _, map_add' := _}
@[simp]
theorem
hahn_series.coeff.add_monoid_hom_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
(g : Γ)
(f : hahn_series Γ R) :
⇑(hahn_series.coeff.add_monoid_hom g) f = f.coeff g
def
hahn_series.coeff.add_monoid_hom
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
(g : Γ) :
hahn_series Γ R →+ R
coeff g as an additive monoid/group homomorphism
Equations
- hahn_series.coeff.add_monoid_hom g = {to_fun := λ (f : hahn_series Γ R), f.coeff g, map_zero' := _, map_add' := _}
theorem
hahn_series.emb_domain_add
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_monoid R]
{Γ' : Type u_3}
[partial_order Γ']
(f : Γ ↪o Γ')
(x y : hahn_series Γ R) :
hahn_series.emb_domain f (x + y) = hahn_series.emb_domain f x + hahn_series.emb_domain f y
@[protected, instance]
def
hahn_series.add_comm_monoid
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R] :
add_comm_monoid (hahn_series Γ R)
Equations
- hahn_series.add_comm_monoid = {add := add_monoid.add hahn_series.add_monoid, add_assoc := _, zero := add_monoid.zero hahn_series.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul hahn_series.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
def
hahn_series.add_group
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_group R] :
add_group (hahn_series Γ R)
Equations
- hahn_series.add_group = {add := add_monoid.add hahn_series.add_monoid, add_assoc := _, zero := add_monoid.zero hahn_series.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul hahn_series.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (x : hahn_series Γ R), {coeff := λ (a : Γ), -x.coeff a, is_pwo_support' := _}, sub := sub_neg_monoid.sub._default add_monoid.add hahn_series.add_group._proof_7 add_monoid.zero hahn_series.add_group._proof_8 hahn_series.add_group._proof_9 add_monoid.nsmul hahn_series.add_group._proof_10 hahn_series.add_group._proof_11 (λ (x : hahn_series Γ R), {coeff := λ (a : Γ), -x.coeff a, is_pwo_support' := _}), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul._default add_monoid.add hahn_series.add_group._proof_13 add_monoid.zero hahn_series.add_group._proof_14 hahn_series.add_group._proof_15 add_monoid.nsmul hahn_series.add_group._proof_16 hahn_series.add_group._proof_17 (λ (x : hahn_series Γ R), {coeff := λ (a : Γ), -x.coeff a, is_pwo_support' := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[simp]
theorem
hahn_series.neg_coeff'
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_group R]
{x : hahn_series Γ R} :
theorem
hahn_series.neg_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_group R]
{x : hahn_series Γ R}
{a : Γ} :
@[simp]
theorem
hahn_series.support_neg
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_group R]
{x : hahn_series Γ R} :
@[simp]
theorem
hahn_series.sub_coeff'
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_group R]
{x y : hahn_series Γ R} :
theorem
hahn_series.sub_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_group R]
{x y : hahn_series Γ R}
{a : Γ} :
@[protected, instance]
def
hahn_series.add_comm_group
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_group R] :
add_comm_group (hahn_series Γ R)
Equations
- hahn_series.add_comm_group = {add := add_comm_monoid.add hahn_series.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero hahn_series.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul hahn_series.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg hahn_series.add_group, sub := add_group.sub hahn_series.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul hahn_series.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
hahn_series.has_scalar
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
{V : Type u_3}
[monoid R]
[add_monoid V]
[distrib_mul_action R V] :
has_scalar R (hahn_series Γ V)
Equations
- hahn_series.has_scalar = {smul := λ (r : R) (x : hahn_series Γ V), {coeff := r • x.coeff, is_pwo_support' := _}}
@[simp]
theorem
hahn_series.smul_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
{V : Type u_3}
[monoid R]
[add_monoid V]
[distrib_mul_action R V]
{r : R}
{x : hahn_series Γ V}
{a : Γ} :
@[protected, instance]
def
hahn_series.distrib_mul_action
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
{V : Type u_3}
[monoid R]
[add_monoid V]
[distrib_mul_action R V] :
distrib_mul_action R (hahn_series Γ V)
Equations
- hahn_series.distrib_mul_action = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul hahn_series.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[protected, instance]
def
hahn_series.is_scalar_tower
{Γ : Type u_1}
{R : Type u_2}
[partial_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] :
is_scalar_tower R S (hahn_series Γ V)
@[protected, instance]
def
hahn_series.smul_comm_class
{Γ : Type u_1}
{R : Type u_2}
[partial_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] :
smul_comm_class R S (hahn_series Γ V)
@[protected, instance]
def
hahn_series.module
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
{V : Type u_3}
[add_comm_monoid V]
[module R V] :
module R (hahn_series Γ V)
Equations
- hahn_series.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action hahn_series.distrib_mul_action, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
hahn_series.single.linear_map_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
(a : Γ)
(ᾰ : R) :
noncomputable
def
hahn_series.single.linear_map
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
(a : Γ) :
R →ₗ[R] hahn_series Γ R
single as a linear map
Equations
- hahn_series.single.linear_map a = {to_fun := (hahn_series.single.add_monoid_hom a).to_fun, map_add' := _, map_smul' := _}
def
hahn_series.coeff.linear_map
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
(g : Γ) :
hahn_series Γ R →ₗ[R] R
coeff g as a linear map
Equations
- hahn_series.coeff.linear_map g = {to_fun := (hahn_series.coeff.add_monoid_hom g).to_fun, map_add' := _, map_smul' := _}
@[simp]
theorem
hahn_series.coeff.linear_map_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
(g : Γ)
(ᾰ : hahn_series Γ R) :
theorem
hahn_series.emb_domain_smul
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
{Γ' : Type u_4}
[partial_order Γ']
(f : Γ ↪o Γ')
(r : R)
(x : hahn_series Γ R) :
hahn_series.emb_domain f (r • x) = r • hahn_series.emb_domain f x
@[simp]
theorem
hahn_series.emb_domain_linear_map_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
{Γ' : Type u_4}
[partial_order Γ']
(f : Γ ↪o Γ')
(ᾰ : hahn_series Γ R) :
noncomputable
def
hahn_series.emb_domain_linear_map
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[semiring R]
{Γ' : Type u_4}
[partial_order Γ']
(f : Γ ↪o Γ') :
hahn_series Γ R →ₗ[R] hahn_series Γ' R
Extending the domain of Hahn series is a linear map.
Equations
- hahn_series.emb_domain_linear_map f = {to_fun := hahn_series.emb_domain f, map_add' := _, map_smul' := _}
@[protected, instance]
noncomputable
def
hahn_series.has_one
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[has_zero R]
[has_one R] :
has_one (hahn_series Γ R)
Equations
- hahn_series.has_one = {one := ⇑(hahn_series.single 0) 1}
@[simp]
theorem
hahn_series.one_coeff
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[has_zero R]
[has_one R]
{a : Γ} :
@[simp]
theorem
hahn_series.single_zero_one
{R : Type u_2}
[has_zero R]
[has_one R] :
⇑(hahn_series.single 0) 1 = 1
@[simp]
theorem
hahn_series.support_one
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[mul_zero_one_class R]
[nontrivial R] :
@[simp]
theorem
hahn_series.order_one
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[mul_zero_one_class R] :
@[protected, instance]
noncomputable
def
hahn_series.has_mul
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R] :
has_mul (hahn_series Γ R)
Equations
- hahn_series.has_mul = {mul := λ (x y : hahn_series Γ R), {coeff := λ (a : Γ), ∑ (ij : Γ × Γ) in finset.add_antidiagonal _ _ a, (x.coeff ij.fst) * y.coeff ij.snd, is_pwo_support' := _}}
@[simp]
theorem
hahn_series.mul_coeff
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{x y : hahn_series Γ R}
{a : Γ} :
theorem
hahn_series.mul_coeff_right'
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{x y : hahn_series Γ R}
{a : Γ}
{s : set Γ}
(hs : s.is_pwo)
(hys : y.support ⊆ s) :
theorem
hahn_series.mul_coeff_left'
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{x y : hahn_series Γ R}
{a : Γ}
{s : set Γ}
(hs : s.is_pwo)
(hxs : x.support ⊆ s) :
@[protected, instance]
noncomputable
def
hahn_series.distrib
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R] :
distrib (hahn_series Γ R)
Equations
- hahn_series.distrib = {mul := has_mul.mul hahn_series.has_mul, add := has_add.add hahn_series.has_add, left_distrib := _, right_distrib := _}
theorem
hahn_series.single_mul_coeff_add
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{r : R}
{x : hahn_series Γ R}
{a b : Γ} :
theorem
hahn_series.mul_single_coeff_add
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{r : R}
{x : hahn_series Γ R}
{a b : Γ} :
@[simp]
theorem
hahn_series.mul_single_zero_coeff
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{r : R}
{x : hahn_series Γ R}
{a : Γ} :
theorem
hahn_series.single_zero_mul_coeff
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{r : R}
{x : hahn_series Γ R}
{a : Γ} :
@[simp]
theorem
hahn_series.single_zero_mul_eq_smul
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{r : R}
{x : hahn_series Γ R} :
(⇑(hahn_series.single 0) r) * x = r • x
theorem
hahn_series.support_mul_subset_add_support
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{x y : hahn_series Γ R} :
theorem
hahn_series.mul_coeff_order_add_order
{R : Type u_2}
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
(x y : hahn_series Γ R) :
@[protected, instance]
noncomputable
def
hahn_series.non_unital_non_assoc_semiring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R] :
Equations
- hahn_series.non_unital_non_assoc_semiring = {add := has_add.add hahn_series.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul hahn_series.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul hahn_series.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
noncomputable
def
hahn_series.non_unital_semiring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_semiring R] :
Equations
- hahn_series.non_unital_semiring = {add := has_add.add hahn_series.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul hahn_series.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul hahn_series.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
noncomputable
def
hahn_series.non_assoc_semiring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R] :
Equations
- hahn_series.non_assoc_semiring = {add := has_add.add hahn_series.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul hahn_series.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul hahn_series.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := 1, one_mul := _, mul_one := _}
@[protected, instance]
noncomputable
def
hahn_series.semiring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R] :
semiring (hahn_series Γ R)
Equations
- hahn_series.semiring = {add := has_add.add hahn_series.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul hahn_series.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul hahn_series.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid_with_zero.npow._default 1 has_mul.mul hahn_series.semiring._proof_14 hahn_series.semiring._proof_15, npow_zero' := _, npow_succ' := _}
@[protected, instance]
noncomputable
def
hahn_series.comm_semiring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R] :
comm_semiring (hahn_series Γ R)
Equations
- hahn_series.comm_semiring = {add := semiring.add hahn_series.semiring, add_assoc := _, zero := semiring.zero hahn_series.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul hahn_series.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul hahn_series.semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one hahn_series.semiring, one_mul := _, mul_one := _, npow := semiring.npow hahn_series.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
noncomputable
def
hahn_series.non_unital_non_assoc_ring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_ring R] :
Equations
- hahn_series.non_unital_non_assoc_ring = {add := non_unital_non_assoc_semiring.add hahn_series.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero hahn_series.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul hahn_series.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg hahn_series.add_group, sub := add_group.sub hahn_series.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul hahn_series.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul hahn_series.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
@[protected, instance]
noncomputable
def
hahn_series.non_unital_ring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_ring R] :
non_unital_ring (hahn_series Γ R)
Equations
- hahn_series.non_unital_ring = {add := non_unital_non_assoc_ring.add hahn_series.non_unital_non_assoc_ring, add_assoc := _, zero := non_unital_non_assoc_ring.zero hahn_series.non_unital_non_assoc_ring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_ring.nsmul hahn_series.non_unital_non_assoc_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_non_assoc_ring.neg hahn_series.non_unital_non_assoc_ring, sub := non_unital_non_assoc_ring.sub hahn_series.non_unital_non_assoc_ring, sub_eq_add_neg := _, zsmul := non_unital_non_assoc_ring.zsmul hahn_series.non_unital_non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_non_assoc_ring.mul hahn_series.non_unital_non_assoc_ring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
@[protected, instance]
noncomputable
def
hahn_series.non_assoc_ring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_ring R] :
non_assoc_ring (hahn_series Γ R)
Equations
- hahn_series.non_assoc_ring = {add := non_unital_non_assoc_ring.add hahn_series.non_unital_non_assoc_ring, add_assoc := _, zero := non_unital_non_assoc_ring.zero hahn_series.non_unital_non_assoc_ring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_ring.nsmul hahn_series.non_unital_non_assoc_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_non_assoc_ring.neg hahn_series.non_unital_non_assoc_ring, sub := non_unital_non_assoc_ring.sub hahn_series.non_unital_non_assoc_ring, sub_eq_add_neg := _, zsmul := non_unital_non_assoc_ring.zsmul hahn_series.non_unital_non_assoc_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_non_assoc_ring.mul hahn_series.non_unital_non_assoc_ring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := non_assoc_semiring.one hahn_series.non_assoc_semiring, one_mul := _, mul_one := _}
@[protected, instance]
noncomputable
def
hahn_series.ring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[ring R] :
ring (hahn_series Γ R)
Equations
- hahn_series.ring = {add := semiring.add hahn_series.semiring, add_assoc := _, zero := semiring.zero hahn_series.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul hahn_series.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg hahn_series.add_comm_group, sub := add_comm_group.sub hahn_series.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul hahn_series.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := semiring.mul hahn_series.semiring, mul_assoc := _, one := semiring.one hahn_series.semiring, one_mul := _, mul_one := _, npow := semiring.npow hahn_series.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
noncomputable
def
hahn_series.comm_ring
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_ring R] :
comm_ring (hahn_series Γ R)
Equations
- hahn_series.comm_ring = {add := comm_semiring.add hahn_series.comm_semiring, add_assoc := _, zero := comm_semiring.zero hahn_series.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul hahn_series.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg hahn_series.ring, sub := ring.sub hahn_series.ring, sub_eq_add_neg := _, zsmul := ring.zsmul hahn_series.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_semiring.mul hahn_series.comm_semiring, mul_assoc := _, one := comm_semiring.one hahn_series.comm_semiring, one_mul := _, mul_one := _, npow := comm_semiring.npow hahn_series.comm_semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[protected, instance]
def
hahn_series.no_zero_divisors
{R : Type u_2}
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
[no_zero_divisors R] :
no_zero_divisors (hahn_series Γ R)
@[protected, instance]
def
hahn_series.is_domain
{R : Type u_2}
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
[ring R]
[is_domain R] :
is_domain (hahn_series Γ R)
@[simp]
theorem
hahn_series.order_mul
{R : Type u_2}
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
[no_zero_divisors R]
{x y : hahn_series Γ R}
(hx : x ≠ 0)
(hy : y ≠ 0) :
@[simp]
theorem
hahn_series.order_pow
{R : Type u_2}
{Γ : Type u_1}
[linear_ordered_cancel_add_comm_monoid Γ]
[semiring R]
[no_zero_divisors R]
(x : hahn_series Γ R)
(n : ℕ) :
@[simp]
theorem
hahn_series.single_mul_single
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_unital_non_assoc_semiring R]
{a b : Γ}
{r s : R} :
(⇑(hahn_series.single a) r) * ⇑(hahn_series.single b) s = ⇑(hahn_series.single (a + b)) (r * s)
@[simp]
theorem
hahn_series.C_apply
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R]
(ᾰ : R) :
⇑hahn_series.C ᾰ = ⇑(hahn_series.single 0) ᾰ
noncomputable
def
hahn_series.C
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R] :
R →+* hahn_series Γ R
C a is the constant Hahn Series a. C is provided as a ring homomorphism.
Equations
- hahn_series.C = {to_fun := ⇑(hahn_series.single 0), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
hahn_series.C_zero
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R] :
⇑hahn_series.C 0 = 0
@[simp]
theorem
hahn_series.C_one
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R] :
⇑hahn_series.C 1 = 1
theorem
hahn_series.C_injective
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R] :
theorem
hahn_series.C_ne_zero
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R]
{r : R}
(h : r ≠ 0) :
⇑hahn_series.C r ≠ 0
theorem
hahn_series.order_C
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[non_assoc_semiring R]
{r : R} :
(⇑hahn_series.C r).order = 0
theorem
hahn_series.C_mul_eq_smul
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{r : R}
{x : hahn_series Γ R} :
(⇑hahn_series.C r) * x = r • x
theorem
hahn_series.emb_domain_mul
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
{Γ' : Type u_3}
[ordered_cancel_add_comm_monoid Γ']
[non_unital_non_assoc_semiring R]
(f : Γ ↪o Γ')
(hf : ∀ (x y : Γ), ⇑f (x + y) = ⇑f x + ⇑f y)
(x y : hahn_series Γ R) :
hahn_series.emb_domain f (x * y) = (hahn_series.emb_domain f x) * hahn_series.emb_domain f y
theorem
hahn_series.emb_domain_one
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
{Γ' : Type u_3}
[ordered_cancel_add_comm_monoid Γ']
[non_assoc_semiring R]
(f : Γ ↪o Γ')
(hf : ⇑f 0 = 0) :
hahn_series.emb_domain f 1 = 1
noncomputable
def
hahn_series.emb_domain_ring_hom
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
{Γ' : Type u_3}
[ordered_cancel_add_comm_monoid Γ']
[non_assoc_semiring R]
(f : Γ →+ Γ')
(hfi : function.injective ⇑f)
(hf : ∀ (g g' : Γ), ⇑f g ≤ ⇑f g' ↔ g ≤ g') :
hahn_series Γ R →+* hahn_series Γ' R
Extending the domain of Hahn series is a ring homomorphism.
Equations
- hahn_series.emb_domain_ring_hom f hfi hf = {to_fun := hahn_series.emb_domain {to_embedding := {to_fun := ⇑f, inj' := hfi}, map_rel_iff' := hf}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
hahn_series.emb_domain_ring_hom_apply
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
{Γ' : Type u_3}
[ordered_cancel_add_comm_monoid Γ']
[non_assoc_semiring R]
(f : Γ →+ Γ')
(hfi : function.injective ⇑f)
(hf : ∀ (g g' : Γ), ⇑f g ≤ ⇑f g' ↔ g ≤ g')
(ᾰ : hahn_series Γ R) :
⇑(hahn_series.emb_domain_ring_hom f hfi hf) ᾰ = hahn_series.emb_domain {to_embedding := {to_fun := ⇑f, inj' := hfi}, map_rel_iff' := hf} ᾰ
theorem
hahn_series.emb_domain_ring_hom_C
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
{Γ' : Type u_3}
[ordered_cancel_add_comm_monoid Γ']
[non_assoc_semiring R]
{f : Γ →+ Γ'}
{hfi : function.injective ⇑f}
{hf : ∀ (g g' : Γ), ⇑f g ≤ ⇑f g' ↔ g ≤ g'}
{r : R} :
⇑(hahn_series.emb_domain_ring_hom f hfi hf) (⇑hahn_series.C r) = ⇑hahn_series.C r
@[protected, instance]
noncomputable
def
hahn_series.algebra
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A] :
algebra R (hahn_series Γ A)
Equations
- hahn_series.algebra = {to_has_scalar := hahn_series.has_scalar module.to_distrib_mul_action, to_ring_hom := hahn_series.C.comp (algebra_map R A), commutes' := _, smul_def' := _}
theorem
hahn_series.C_eq_algebra_map
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R] :
hahn_series.C = algebra_map R (hahn_series Γ R)
theorem
hahn_series.algebra_map_apply
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
{r : R} :
⇑(algebra_map R (hahn_series Γ A)) r = ⇑hahn_series.C (⇑(algebra_map R A) r)
@[protected, instance]
def
hahn_series.subalgebra.nontrivial
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R]
[nontrivial Γ]
[nontrivial R] :
nontrivial (subalgebra R (hahn_series Γ R))
@[simp]
theorem
hahn_series.emb_domain_alg_hom_apply
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
{Γ' : Type u_4}
[ordered_cancel_add_comm_monoid Γ']
(f : Γ →+ Γ')
(hfi : function.injective ⇑f)
(hf : ∀ (g g' : Γ), ⇑f g ≤ ⇑f g' ↔ g ≤ g')
(ᾰ : hahn_series Γ A) :
⇑(hahn_series.emb_domain_alg_hom f hfi hf) ᾰ = (hahn_series.emb_domain_ring_hom f hfi hf).to_fun ᾰ
noncomputable
def
hahn_series.emb_domain_alg_hom
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
{Γ' : Type u_4}
[ordered_cancel_add_comm_monoid Γ']
(f : Γ →+ Γ')
(hfi : function.injective ⇑f)
(hf : ∀ (g g' : Γ), ⇑f g ≤ ⇑f g' ↔ g ≤ g') :
hahn_series Γ A →ₐ[R] hahn_series Γ' A
Extending the domain of Hahn series is an algebra homomorphism.
@[simp]
theorem
hahn_series.to_power_series_symm_apply_coeff
{R : Type u_2}
[semiring R]
(f : power_series R)
(n : ℕ) :
(⇑(hahn_series.to_power_series.symm) f).coeff n = ⇑(power_series.coeff R n) f
noncomputable
def
hahn_series.to_power_series
{R : Type u_2}
[semiring R] :
hahn_series ℕ R ≃+* power_series R
The ring hahn_series ℕ R is isomorphic to power_series R.
Equations
- hahn_series.to_power_series = {to_fun := λ (f : hahn_series ℕ R), power_series.mk f.coeff, inv_fun := λ (f : power_series R), {coeff := λ (n : ℕ), ⇑(power_series.coeff R n) f, is_pwo_support' := _}, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
hahn_series.coeff_to_power_series
{R : Type u_2}
[semiring R]
{f : hahn_series ℕ R}
{n : ℕ} :
⇑(power_series.coeff R n) (⇑hahn_series.to_power_series f) = f.coeff n
theorem
hahn_series.coeff_to_power_series_symm
{R : Type u_2}
[semiring R]
{f : power_series R}
{n : ℕ} :
(⇑(hahn_series.to_power_series.symm) f).coeff n = ⇑(power_series.coeff R n) f
noncomputable
def
hahn_series.of_power_series
(Γ : Type u_1)
(R : Type u_2)
[semiring R]
[ordered_semiring Γ]
[nontrivial Γ] :
power_series R →+* hahn_series Γ R
Casts a power series as a Hahn series with coefficients from an ordered_semiring.
theorem
hahn_series.of_power_series_injective
{Γ : Type u_1}
{R : Type u_2}
[semiring R]
[ordered_semiring Γ]
[nontrivial Γ] :
@[simp]
theorem
hahn_series.of_power_series_apply
{Γ : Type u_1}
{R : Type u_2}
[semiring R]
[ordered_semiring Γ]
[nontrivial Γ]
(x : power_series R) :
⇑(hahn_series.of_power_series Γ R) x = hahn_series.emb_domain {to_embedding := {to_fun := coe coe_to_lift, inj' := _}, map_rel_iff' := _} (⇑(hahn_series.to_power_series.symm) x)
theorem
hahn_series.of_power_series_apply_coeff
{Γ : Type u_1}
{R : Type u_2}
[semiring R]
[ordered_semiring Γ]
[nontrivial Γ]
(x : power_series R)
(n : ℕ) :
(⇑(hahn_series.of_power_series Γ R) x).coeff ↑n = ⇑(power_series.coeff R n) x
@[simp]
theorem
hahn_series.of_power_series_C
{Γ : Type u_1}
{R : Type u_2}
[semiring R]
[ordered_semiring Γ]
[nontrivial Γ]
(r : R) :
⇑(hahn_series.of_power_series Γ R) (⇑(power_series.C R) r) = ⇑hahn_series.C r
@[simp]
theorem
hahn_series.of_power_series_X
{Γ : Type u_1}
{R : Type u_2}
[semiring R]
[ordered_semiring Γ]
[nontrivial Γ] :
@[simp]
theorem
hahn_series.of_power_series_X_pow
{Γ : Type u_1}
[ordered_semiring Γ]
[nontrivial Γ]
{R : Type u_2}
[comm_semiring R]
(n : ℕ) :
⇑(hahn_series.of_power_series Γ R) (power_series.X ^ n) = ⇑(hahn_series.single ↑n) 1
@[simp]
theorem
hahn_series.to_mv_power_series_apply
{R : Type u_2}
[semiring R]
{σ : Type u_1}
[fintype σ]
(f : hahn_series (σ →₀ ℕ) R)
(ᾰ : σ →₀ ℕ) :
⇑hahn_series.to_mv_power_series f ᾰ = f.coeff ᾰ
def
hahn_series.to_mv_power_series
{R : Type u_2}
[semiring R]
{σ : Type u_1}
[fintype σ] :
hahn_series (σ →₀ ℕ) R ≃+* mv_power_series σ R
The ring hahn_series (σ →₀ ℕ) R is isomorphic to mv_power_series σ R for a fintype σ.
We take the index set of the hahn series to be finsupp rather than pi,
even though we assume fintype σ as this is more natural for alignment with mv_power_series.
After importing algebra.order.pi the ring hahn_series (σ → ℕ) R could be constructed instead.
Equations
- hahn_series.to_mv_power_series = {to_fun := λ (f : hahn_series (σ →₀ ℕ) R), f.coeff, inv_fun := λ (f : mv_power_series σ R), {coeff := f, is_pwo_support' := _}, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
hahn_series.to_mv_power_series_symm_apply_coeff
{R : Type u_2}
[semiring R]
{σ : Type u_1}
[fintype σ]
(f : mv_power_series σ R) :
(⇑(hahn_series.to_mv_power_series.symm) f).coeff = f
theorem
hahn_series.coeff_to_mv_power_series
{R : Type u_2}
[semiring R]
{σ : Type u_3}
[fintype σ]
{f : hahn_series (σ →₀ ℕ) R}
{n : σ →₀ ℕ} :
⇑(mv_power_series.coeff R n) (⇑hahn_series.to_mv_power_series f) = f.coeff n
theorem
hahn_series.coeff_to_mv_power_series_symm
{R : Type u_2}
[semiring R]
{σ : Type u_3}
[fintype σ]
{f : mv_power_series σ R}
{n : σ →₀ ℕ} :
(⇑(hahn_series.to_mv_power_series.symm) f).coeff n = ⇑(mv_power_series.coeff R n) f
@[simp]
theorem
hahn_series.to_power_series_alg_apply
(R : Type u_2)
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
(ᾰ : hahn_series ℕ A) :
noncomputable
def
hahn_series.to_power_series_alg
(R : Type u_2)
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A] :
hahn_series ℕ A ≃ₐ[R] power_series A
The R-algebra hahn_series ℕ A is isomorphic to power_series A.
Equations
- hahn_series.to_power_series_alg R = {to_fun := hahn_series.to_power_series.to_fun, inv_fun := hahn_series.to_power_series.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
hahn_series.to_power_series_alg_symm_apply
(R : Type u_2)
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
(ᾰ : power_series A) :
noncomputable
def
hahn_series.of_power_series_alg
(Γ : Type u_1)
(R : Type u_2)
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
[ordered_semiring Γ]
[nontrivial Γ] :
power_series A →ₐ[R] hahn_series Γ A
Casting a power series as a Hahn series with coefficients from an ordered_semiring
is an algebra homomorphism.
Equations
@[simp]
theorem
hahn_series.of_power_series_alg_apply_coeff
(Γ : Type u_1)
(R : Type u_2)
[comm_semiring R]
{A : Type u_3}
[semiring A]
[algebra R A]
[ordered_semiring Γ]
[nontrivial Γ]
(ᾰ : power_series A)
(b : Γ) :
@[protected, instance]
noncomputable
def
hahn_series.power_series_algebra
(Γ : Type u_1)
(R : Type u_2)
[comm_semiring R]
[ordered_semiring Γ]
[nontrivial Γ]
{S : Type u_3}
[comm_semiring S]
[algebra S (power_series R)] :
algebra S (hahn_series Γ R)
Equations
- hahn_series.power_series_algebra Γ R = ((hahn_series.of_power_series Γ R).comp (algebra_map S (power_series R))).to_algebra
theorem
hahn_series.algebra_map_apply'
(Γ : Type u_1)
{R : Type u_2}
[comm_semiring R]
[ordered_semiring Γ]
[nontrivial Γ]
{S : Type u_4}
[comm_semiring S]
[algebra S (power_series R)]
(x : S) :
⇑(algebra_map S (hahn_series Γ R)) x = ⇑(hahn_series.of_power_series Γ R) (⇑(algebra_map S (power_series R)) x)
@[simp]
theorem
polynomial.algebra_map_hahn_series_apply
(Γ : Type u_1)
{R : Type u_2}
[comm_semiring R]
[ordered_semiring Γ]
[nontrivial Γ]
(f : R[X]) :
⇑(algebra_map R[X] (hahn_series Γ R)) f = ⇑(hahn_series.of_power_series Γ R) ↑f
theorem
polynomial.algebra_map_hahn_series_injective
(Γ : Type u_1)
{R : Type u_2}
[comm_semiring R]
[ordered_semiring Γ]
[nontrivial Γ] :
function.injective ⇑(algebra_map R[X] (hahn_series Γ R))
@[protected, instance]
def
hahn_series.multiplicative.linear_ordered_comm_group
{Γ : Type u_1}
[linear_ordered_add_comm_group Γ] :
Equations
- hahn_series.multiplicative.linear_ordered_comm_group = {mul := ordered_comm_group.mul infer_instance, mul_assoc := _, one := ordered_comm_group.one infer_instance, one_mul := _, mul_one := _, npow := ordered_comm_group.npow infer_instance, npow_zero' := _, npow_succ' := _, inv := ordered_comm_group.inv infer_instance, div := ordered_comm_group.div infer_instance, div_eq_mul_inv := _, zpow := ordered_comm_group.zpow infer_instance, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _, le := linear_order.le infer_instance, lt := linear_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance, max := max infer_instance, max_def := _, min := min infer_instance, min_def := _}
@[protected, instance]
def
hahn_series.with_zero.linear_ordered_comm_group_with_zero
{Γ : Type u_1}
[linear_ordered_add_comm_group Γ] :
Equations
- hahn_series.with_zero.linear_ordered_comm_group_with_zero = {le := ordered_comm_monoid.le with_zero.ordered_comm_monoid, lt := ordered_comm_monoid.lt with_zero.ordered_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le infer_instance, decidable_eq := linear_order.decidable_eq infer_instance, decidable_lt := linear_order.decidable_lt infer_instance, max := max infer_instance, max_def := _, min := min infer_instance, min_def := _, mul := ordered_comm_monoid.mul with_zero.ordered_comm_monoid, mul_assoc := _, one := ordered_comm_monoid.one with_zero.ordered_comm_monoid, one_mul := _, mul_one := _, npow := ordered_comm_monoid.npow with_zero.ordered_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, mul_le_mul_left := _, zero := comm_group_with_zero.zero infer_instance, zero_mul := _, mul_zero := _, zero_le_one := _, inv := comm_group_with_zero.inv infer_instance, div := comm_group_with_zero.div infer_instance, div_eq_mul_inv := _, zpow := comm_group_with_zero.zpow infer_instance, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
noncomputable
def
hahn_series.add_val
(Γ : Type u_1)
(R : Type u_2)
[linear_ordered_add_comm_group Γ]
[ring R]
[is_domain R] :
add_valuation (hahn_series Γ R) (with_top Γ)
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
- hahn_series.add_val Γ R = add_valuation.of (λ (x : hahn_series Γ R), ite (x = 0) ⊤ ↑(x.order)) _ _ _ _
theorem
hahn_series.add_val_apply
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[ring R]
[is_domain R]
{x : hahn_series Γ R} :
@[simp]
theorem
hahn_series.add_val_apply_of_ne
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[ring R]
[is_domain R]
{x : hahn_series Γ R}
(hx : x ≠ 0) :
⇑(hahn_series.add_val Γ R) x = ↑(x.order)
theorem
hahn_series.add_val_le_of_coeff_ne_zero
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[ring R]
[is_domain R]
{x : hahn_series Γ R}
{g : Γ}
(h : x.coeff g ≠ 0) :
⇑(hahn_series.add_val Γ R) x ≤ ↑g
theorem
hahn_series.is_pwo_Union_support_powers
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[ring R]
[is_domain R]
{x : hahn_series Γ R}
(hx : 0 < ⇑(hahn_series.add_val Γ R) x) :
structure
hahn_series.summable_family
(Γ : Type u_1)
(R : Type u_2)
[partial_order Γ]
[add_comm_monoid R]
(α : Type u_3) :
Type (max u_1 u_2 u_3)
- to_fun : α → hahn_series Γ R
- is_pwo_Union_support' : (⋃ (a : α), (self.to_fun a).support).is_pwo
- finite_co_support' : ∀ (g : Γ), {a : α | (self.to_fun a).coeff g ≠ 0}.finite
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.
@[protected, instance]
def
hahn_series.summable_family.has_coe_to_fun
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
has_coe_to_fun (hahn_series.summable_family Γ R α) (λ (_x : hahn_series.summable_family Γ R α), α → hahn_series Γ R)
theorem
hahn_series.summable_family.is_pwo_Union_support
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
(s : hahn_series.summable_family Γ R α) :
theorem
hahn_series.summable_family.finite_co_support
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
(s : hahn_series.summable_family Γ R α)
(g : Γ) :
(function.support (λ (a : α), (⇑s a).coeff g)).finite
theorem
hahn_series.summable_family.coe_injective
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
@[ext]
theorem
hahn_series.summable_family.ext
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{s t : hahn_series.summable_family Γ R α}
(h : ∀ (a : α), ⇑s a = ⇑t a) :
s = t
@[protected, instance]
def
hahn_series.summable_family.has_add
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
has_add (hahn_series.summable_family Γ R α)
Equations
- hahn_series.summable_family.has_add = {add := λ (x y : hahn_series.summable_family Γ R α), {to_fun := ⇑x + ⇑y, is_pwo_Union_support' := _, finite_co_support' := _}}
@[protected, instance]
def
hahn_series.summable_family.has_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
has_zero (hahn_series.summable_family Γ R α)
Equations
- hahn_series.summable_family.has_zero = {zero := {to_fun := 0, is_pwo_Union_support' := _, finite_co_support' := _}}
@[protected, instance]
def
hahn_series.summable_family.inhabited
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
inhabited (hahn_series.summable_family Γ R α)
Equations
@[simp]
theorem
hahn_series.summable_family.coe_add
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{s t : hahn_series.summable_family Γ R α} :
theorem
hahn_series.summable_family.add_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{s t : hahn_series.summable_family Γ R α}
{a : α} :
@[simp]
theorem
hahn_series.summable_family.coe_zero
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
theorem
hahn_series.summable_family.zero_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{a : α} :
@[protected, instance]
def
hahn_series.summable_family.add_comm_monoid
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3} :
Equations
- hahn_series.summable_family.add_comm_monoid = {add := has_add.add hahn_series.summable_family.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default 0 has_add.add hahn_series.summable_family.add_comm_monoid._proof_4 hahn_series.summable_family.add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
noncomputable
def
hahn_series.summable_family.hsum
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
(s : hahn_series.summable_family Γ R α) :
hahn_series Γ R
The infinite sum of a summable_family of Hahn series.
@[simp]
theorem
hahn_series.summable_family.hsum_coeff
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{s : hahn_series.summable_family Γ R α}
{g : Γ} :
theorem
hahn_series.summable_family.support_hsum_subset
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{s : hahn_series.summable_family Γ R α} :
@[simp]
theorem
hahn_series.summable_family.hsum_add
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{s t : hahn_series.summable_family Γ R α} :
@[protected, instance]
def
hahn_series.summable_family.add_comm_group
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_group R]
{α : Type u_3} :
Equations
- hahn_series.summable_family.add_comm_group = {add := add_comm_monoid.add hahn_series.summable_family.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero hahn_series.summable_family.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul hahn_series.summable_family.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := λ (s : hahn_series.summable_family Γ R α), {to_fun := λ (a : α), -⇑s a, is_pwo_Union_support' := _, finite_co_support' := _}, sub := add_group.sub._default add_comm_monoid.add hahn_series.summable_family.add_comm_group._proof_8 add_comm_monoid.zero hahn_series.summable_family.add_comm_group._proof_9 hahn_series.summable_family.add_comm_group._proof_10 add_comm_monoid.nsmul hahn_series.summable_family.add_comm_group._proof_11 hahn_series.summable_family.add_comm_group._proof_12 (λ (s : hahn_series.summable_family Γ R α), {to_fun := λ (a : α), -⇑s a, is_pwo_Union_support' := _, finite_co_support' := _}), sub_eq_add_neg := _, zsmul := add_group.zsmul._default add_comm_monoid.add hahn_series.summable_family.add_comm_group._proof_14 add_comm_monoid.zero hahn_series.summable_family.add_comm_group._proof_15 hahn_series.summable_family.add_comm_group._proof_16 add_comm_monoid.nsmul hahn_series.summable_family.add_comm_group._proof_17 hahn_series.summable_family.add_comm_group._proof_18 (λ (s : hahn_series.summable_family Γ R α), {to_fun := λ (a : α), -⇑s a, is_pwo_Union_support' := _, finite_co_support' := _}), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[simp]
theorem
hahn_series.summable_family.coe_neg
{Γ : Type u_1}
{R : Type u_2}
[partial_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}
[partial_order Γ]
[add_comm_group R]
{α : Type u_3}
{s : hahn_series.summable_family Γ R α}
{a : α} :
@[simp]
theorem
hahn_series.summable_family.coe_sub
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_group R]
{α : Type u_3}
{s t : hahn_series.summable_family Γ R α} :
theorem
hahn_series.summable_family.sub_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_group R]
{α : Type u_3}
{s t : hahn_series.summable_family Γ R α}
{a : α} :
@[protected, instance]
noncomputable
def
hahn_series.summable_family.has_scalar
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{α : Type u_3} :
has_scalar (hahn_series Γ R) (hahn_series.summable_family Γ R α)
Equations
- hahn_series.summable_family.has_scalar = {smul := λ (x : hahn_series Γ R) (s : hahn_series.summable_family Γ R α), {to_fun := λ (a : α), x * ⇑s a, is_pwo_Union_support' := _, finite_co_support' := _}}
@[simp]
theorem
hahn_series.summable_family.smul_apply
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{α : Type u_3}
{x : hahn_series Γ R}
{s : hahn_series.summable_family Γ R α}
{a : α} :
@[protected, instance]
noncomputable
def
hahn_series.summable_family.module
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{α : Type u_3} :
module (hahn_series Γ R) (hahn_series.summable_family Γ R α)
Equations
- hahn_series.summable_family.module = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul hahn_series.summable_family.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[simp]
theorem
hahn_series.summable_family.hsum_smul
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{α : Type u_3}
{x : hahn_series Γ R}
{s : hahn_series.summable_family Γ R α} :
@[simp]
theorem
hahn_series.summable_family.lsum_apply
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{α : Type u_3}
(s : hahn_series.summable_family Γ R α) :
noncomputable
def
hahn_series.summable_family.lsum
{Γ : Type u_1}
{R : Type u_2}
[ordered_cancel_add_comm_monoid Γ]
[semiring R]
{α : Type u_3} :
hahn_series.summable_family Γ R α →ₗ[hahn_series Γ R] hahn_series Γ R
The summation of a summable_family as a linear_map.
Equations
- hahn_series.summable_family.lsum = {to_fun := hahn_series.summable_family.hsum α, map_add' := _, map_smul' := _}
@[simp]
theorem
hahn_series.summable_family.hsum_sub
{Γ : Type u_1}
[ordered_cancel_add_comm_monoid Γ]
{α : Type u_3}
{R : Type u_2}
[ring R]
{s t : hahn_series.summable_family Γ R α} :
def
hahn_series.summable_family.of_finsupp
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
(f : α →₀ hahn_series Γ R) :
A family with only finitely many nonzero elements is summable.
Equations
- hahn_series.summable_family.of_finsupp f = {to_fun := ⇑f, is_pwo_Union_support' := _, finite_co_support' := _}
@[simp]
theorem
hahn_series.summable_family.coe_of_finsupp
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{f : α →₀ hahn_series Γ R} :
@[simp]
theorem
hahn_series.summable_family.hsum_of_finsupp
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{f : α →₀ hahn_series Γ R} :
(hahn_series.summable_family.of_finsupp f).hsum = f.sum (λ (a : α), id)
noncomputable
def
hahn_series.summable_family.emb_domain
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{β : Type u_4}
(s : hahn_series.summable_family Γ R α)
(f : α ↪ β) :
A summable family can be reindexed by an embedding without changing its sum.
Equations
- s.emb_domain f = {to_fun := λ (b : β), dite (b ∈ set.range ⇑f) (λ (h : b ∈ set.range ⇑f), ⇑s (classical.some h)) (λ (h : b ∉ set.range ⇑f), 0), is_pwo_Union_support' := _, finite_co_support' := _}
theorem
hahn_series.summable_family.emb_domain_apply
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{β : Type u_4}
(s : hahn_series.summable_family Γ R α)
(f : α ↪ β)
{b : β} :
@[simp]
theorem
hahn_series.summable_family.emb_domain_image
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{β : Type u_4}
(s : hahn_series.summable_family Γ R α)
(f : α ↪ β)
{a : α} :
⇑(s.emb_domain f) (⇑f a) = ⇑s a
@[simp]
theorem
hahn_series.summable_family.emb_domain_notin_range
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{β : Type u_4}
(s : hahn_series.summable_family Γ R α)
(f : α ↪ β)
{b : β}
(h : b ∉ set.range ⇑f) :
⇑(s.emb_domain f) b = 0
@[simp]
theorem
hahn_series.summable_family.hsum_emb_domain
{Γ : Type u_1}
{R : Type u_2}
[partial_order Γ]
[add_comm_monoid R]
{α : Type u_3}
{β : Type u_4}
(s : hahn_series.summable_family Γ R α)
(f : α ↪ β) :
(s.emb_domain f).hsum = s.hsum
noncomputable
def
hahn_series.summable_family.powers
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[comm_ring R]
[is_domain R]
(x : hahn_series Γ R)
(hx : 0 < ⇑(hahn_series.add_val Γ R) x) :
The powers of an element of positive valuation form a summable family.
Equations
- hahn_series.summable_family.powers x hx = {to_fun := λ (n : ℕ), x ^ n, is_pwo_Union_support' := _, finite_co_support' := _}
@[simp]
theorem
hahn_series.summable_family.coe_powers
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[comm_ring R]
[is_domain R]
{x : hahn_series Γ R}
(hx : 0 < ⇑(hahn_series.add_val Γ R) x) :
⇑(hahn_series.summable_family.powers x hx) = pow x
theorem
hahn_series.summable_family.emb_domain_succ_smul_powers
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[comm_ring R]
[is_domain R]
{x : hahn_series Γ R}
(hx : 0 < ⇑(hahn_series.add_val Γ R) x) :
theorem
hahn_series.summable_family.one_sub_self_mul_hsum_powers
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[comm_ring R]
[is_domain R]
{x : hahn_series Γ R}
(hx : 0 < ⇑(hahn_series.add_val Γ R) x) :
(1 - x) * (hahn_series.summable_family.powers x hx).hsum = 1
theorem
hahn_series.unit_aux
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[comm_ring R]
[is_domain R]
(x : hahn_series Γ R)
{r : R}
(hr : r * x.coeff x.order = 1) :
0 < ⇑(hahn_series.add_val Γ R) (1 - ((⇑hahn_series.C r) * ⇑(hahn_series.single (-x.order)) 1) * x)
theorem
hahn_series.is_unit_iff
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[comm_ring R]
[is_domain R]
{x : hahn_series Γ R} :
@[protected, instance]
noncomputable
def
hahn_series.field
{Γ : Type u_1}
{R : Type u_2}
[linear_ordered_add_comm_group Γ]
[field R] :
field (hahn_series Γ R)
Equations
- hahn_series.field = {add := comm_ring.add hahn_series.comm_ring, add_assoc := _, zero := comm_ring.zero hahn_series.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul hahn_series.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg hahn_series.comm_ring, sub := comm_ring.sub hahn_series.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul hahn_series.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul hahn_series.comm_ring, mul_assoc := _, one := comm_ring.one hahn_series.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow hahn_series.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (x : hahn_series Γ R), dite (x = 0) (λ (x0 : x = 0), 0) (λ (x0 : ¬x = 0), ((⇑hahn_series.C (x.coeff x.order)⁻¹) * ⇑(hahn_series.single (-x.order)) 1) * (hahn_series.summable_family.powers (1 - ((⇑hahn_series.C (x.coeff x.order)⁻¹) * ⇑(hahn_series.single (-x.order)) 1) * x) _).hsum), div := div_inv_monoid.div._default comm_ring.mul hahn_series.field._proof_21 comm_ring.one hahn_series.field._proof_22 hahn_series.field._proof_23 comm_ring.npow hahn_series.field._proof_24 hahn_series.field._proof_25 (λ (x : hahn_series Γ R), dite (x = 0) (λ (x0 : x = 0), 0) (λ (x0 : ¬x = 0), ((⇑hahn_series.C (x.coeff x.order)⁻¹) * ⇑(hahn_series.single (-x.order)) 1) * (hahn_series.summable_family.powers (1 - ((⇑hahn_series.C (x.coeff x.order)⁻¹) * ⇑(hahn_series.single (-x.order)) 1) * x) _).hsum)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default comm_ring.mul hahn_series.field._proof_27 comm_ring.one hahn_series.field._proof_28 hahn_series.field._proof_29 comm_ring.npow hahn_series.field._proof_30 hahn_series.field._proof_31 (λ (x : hahn_series Γ R), dite (x = 0) (λ (x0 : x = 0), 0) (λ (x0 : ¬x = 0), ((⇑hahn_series.C (x.coeff x.order)⁻¹) * ⇑(hahn_series.single (-x.order)) 1) * (hahn_series.summable_family.powers (1 - ((⇑hahn_series.C (x.coeff x.order)⁻¹) * ⇑(hahn_series.single (-x.order)) 1) * x) _).hsum)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}