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. We introduce valuations and a notion of
summability for possibly infinite families of series.
Main Definitions #
HahnSeries.addVal Γ Rdefines anAddValuationonHahnSeries Γ RwhenΓis linearly ordered.- A
HahnSeries.SummableFamilyis 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,HahnSeries.SummableFamily.hsum, which can be bundled as aLinearMapasHahnSeries.SummableFamily.lsum. Note that this is different fromSummablein the valuation topology, because there are topologically summable families that do not satisfy the axioms ofHahnSeries.SummableFamily, and formally summable families whose sums do not converge topologically.
References #
- [J. van der Hoeven, Operators on Generalized Power Series][van_der_hoeven]
def
HahnSeries.addVal
(Γ : Type u_1)
(R : Type u_2)
[LinearOrderedCancelAddCommMonoid Γ]
[Ring R]
[IsDomain R]
:
AddValuation (HahnSeries Γ R) (WithTop Γ)
The additive valuation on HahnSeries Γ R, returning the smallest index at which
a Hahn Series has a nonzero coefficient, or ⊤ for the 0 series.
Equations
- HahnSeries.addVal Γ R = AddValuation.of (fun (x : HahnSeries Γ R) => if x = 0 then ⊤ else ↑(HahnSeries.order x)) ⋯ ⋯ ⋯ ⋯
Instances For
theorem
HahnSeries.addVal_apply
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[Ring R]
[IsDomain R]
{x : HahnSeries Γ R}
:
(HahnSeries.addVal Γ R) x = if x = 0 then ⊤ else ↑(HahnSeries.order x)
@[simp]
theorem
HahnSeries.addVal_apply_of_ne
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[Ring R]
[IsDomain R]
{x : HahnSeries Γ R}
(hx : x ≠ 0)
:
(HahnSeries.addVal Γ R) x = ↑(HahnSeries.order x)
theorem
HahnSeries.addVal_le_of_coeff_ne_zero
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[Ring R]
[IsDomain R]
{x : HahnSeries Γ R}
{g : Γ}
(h : x.coeff g ≠ 0)
:
(HahnSeries.addVal Γ R) x ≤ ↑g
theorem
HahnSeries.isPWO_iUnion_support_powers
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[Ring R]
[IsDomain R]
{x : HahnSeries Γ R}
(hx : 0 < (HahnSeries.addVal Γ R) x)
:
Set.IsPWO (⋃ (n : ℕ), HahnSeries.support (x ^ n))
structure
HahnSeries.SummableFamily
(Γ : Type u_1)
(R : Type u_2)
[PartialOrder Γ]
[AddCommMonoid R]
(α : Type u_3)
:
Type (max (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.
- toFun : α → HahnSeries Γ R
- isPWO_iUnion_support' : Set.IsPWO (⋃ (a : α), HahnSeries.support (self.toFun a))
- finite_co_support' : ∀ (g : Γ), Set.Finite {a : α | (self.toFun a).coeff g ≠ 0}
Instances For
instance
HahnSeries.SummableFamily.instFunLikeSummableFamilyHahnSeriesToZeroToAddMonoid
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
FunLike (HahnSeries.SummableFamily Γ R α) α (HahnSeries Γ R)
Equations
- HahnSeries.SummableFamily.instFunLikeSummableFamilyHahnSeriesToZeroToAddMonoid = { coe := HahnSeries.SummableFamily.toFun, coe_injective' := ⋯ }
theorem
HahnSeries.SummableFamily.isPWO_iUnion_support
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
(s : HahnSeries.SummableFamily Γ R α)
:
Set.IsPWO (⋃ (a : α), HahnSeries.support (s a))
theorem
HahnSeries.SummableFamily.finite_co_support
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
(s : HahnSeries.SummableFamily Γ R α)
(g : Γ)
:
Set.Finite (Function.support fun (a : α) => (s a).coeff g)
theorem
HahnSeries.SummableFamily.coe_injective
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
Function.Injective DFunLike.coe
theorem
HahnSeries.SummableFamily.ext
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
(h : ∀ (a : α), s a = t a)
:
s = t
instance
HahnSeries.SummableFamily.instAddSummableFamily
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
Add (HahnSeries.SummableFamily Γ R α)
Equations
- HahnSeries.SummableFamily.instAddSummableFamily = { add := fun (x y : HahnSeries.SummableFamily Γ R α) => { toFun := ⇑x + ⇑y, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
instance
HahnSeries.SummableFamily.instZeroSummableFamily
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
Zero (HahnSeries.SummableFamily Γ R α)
Equations
- HahnSeries.SummableFamily.instZeroSummableFamily = { zero := { toFun := 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
instance
HahnSeries.SummableFamily.instInhabitedSummableFamily
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
Inhabited (HahnSeries.SummableFamily Γ R α)
Equations
- HahnSeries.SummableFamily.instInhabitedSummableFamily = { default := 0 }
@[simp]
theorem
HahnSeries.SummableFamily.coe_add
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
:
theorem
HahnSeries.SummableFamily.add_apply
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
{a : α}
:
@[simp]
theorem
HahnSeries.SummableFamily.coe_zero
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
⇑0 = 0
theorem
HahnSeries.SummableFamily.zero_apply
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{a : α}
:
0 a = 0
instance
HahnSeries.SummableFamily.instAddCommMonoidSummableFamily
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
:
Equations
- HahnSeries.SummableFamily.instAddCommMonoidSummableFamily = AddCommMonoid.mk ⋯
def
HahnSeries.SummableFamily.hsum
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
(s : HahnSeries.SummableFamily Γ R α)
:
HahnSeries Γ R
The infinite sum of a SummableFamily of Hahn series.
Equations
- HahnSeries.SummableFamily.hsum s = { coeff := fun (g : Γ) => finsum fun (i : α) => (s i).coeff g, isPWO_support' := ⋯ }
Instances For
@[simp]
theorem
HahnSeries.SummableFamily.hsum_coeff
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{g : Γ}
:
(HahnSeries.SummableFamily.hsum s).coeff g = finsum fun (i : α) => (s i).coeff g
theorem
HahnSeries.SummableFamily.support_hsum_subset
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
:
HahnSeries.support (HahnSeries.SummableFamily.hsum s) ⊆ ⋃ (a : α), HahnSeries.support (s a)
@[simp]
theorem
HahnSeries.SummableFamily.hsum_add
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
:
instance
HahnSeries.SummableFamily.instNegSummableFamilyToAddCommMonoid
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommGroup R]
{α : Type u_3}
:
Neg (HahnSeries.SummableFamily Γ R α)
Equations
- One or more equations did not get rendered due to their size.
instance
HahnSeries.SummableFamily.instAddCommGroupSummableFamilyToAddCommMonoid
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommGroup R]
{α : Type u_3}
:
Equations
- HahnSeries.SummableFamily.instAddCommGroupSummableFamilyToAddCommMonoid = let __src := inferInstanceAs (AddCommMonoid (HahnSeries.SummableFamily Γ R α)); AddCommGroup.mk ⋯
@[simp]
theorem
HahnSeries.SummableFamily.coe_neg
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommGroup R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
:
theorem
HahnSeries.SummableFamily.neg_apply
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommGroup R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{a : α}
:
@[simp]
theorem
HahnSeries.SummableFamily.coe_sub
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommGroup R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
:
theorem
HahnSeries.SummableFamily.sub_apply
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommGroup R]
{α : Type u_3}
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
{a : α}
:
instance
HahnSeries.SummableFamily.instSMulHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroSummableFamilyToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiring
{Γ : Type u_1}
{R : Type u_2}
[OrderedCancelAddCommMonoid Γ]
[Semiring R]
{α : Type u_3}
:
SMul (HahnSeries Γ R) (HahnSeries.SummableFamily Γ R α)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HahnSeries.SummableFamily.smul_apply
{Γ : Type u_1}
{R : Type u_2}
[OrderedCancelAddCommMonoid Γ]
[Semiring R]
{α : Type u_3}
{x : HahnSeries Γ R}
{s : HahnSeries.SummableFamily Γ R α}
{a : α}
:
instance
HahnSeries.SummableFamily.instModuleHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroSummableFamilyToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroInstAddCommMonoidSummableFamily
{Γ : Type u_1}
{R : Type u_2}
[OrderedCancelAddCommMonoid Γ]
[Semiring R]
{α : Type u_3}
:
Module (HahnSeries Γ R) (HahnSeries.SummableFamily Γ R α)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HahnSeries.SummableFamily.hsum_smul
{Γ : Type u_1}
{R : Type u_2}
[OrderedCancelAddCommMonoid Γ]
[Semiring R]
{α : Type u_3}
{x : HahnSeries Γ R}
{s : HahnSeries.SummableFamily Γ R α}
:
@[simp]
theorem
HahnSeries.SummableFamily.lsum_apply
{Γ : Type u_1}
{R : Type u_2}
[OrderedCancelAddCommMonoid Γ]
[Semiring R]
{α : Type u_3}
(s : HahnSeries.SummableFamily Γ R α)
:
HahnSeries.SummableFamily.lsum s = HahnSeries.SummableFamily.hsum s
def
HahnSeries.SummableFamily.lsum
{Γ : Type u_1}
{R : Type u_2}
[OrderedCancelAddCommMonoid Γ]
[Semiring R]
{α : Type u_3}
:
HahnSeries.SummableFamily Γ R α →ₗ[HahnSeries Γ R] HahnSeries Γ R
The summation of a summable_family as a LinearMap.
Equations
- HahnSeries.SummableFamily.lsum = { toAddHom := { toFun := HahnSeries.SummableFamily.hsum, map_add' := ⋯ }, map_smul' := ⋯ }
Instances For
@[simp]
theorem
HahnSeries.SummableFamily.hsum_sub
{Γ : Type u_1}
[OrderedCancelAddCommMonoid Γ]
{α : Type u_3}
{R : Type u_4}
[Ring R]
{s : HahnSeries.SummableFamily Γ R α}
{t : HahnSeries.SummableFamily Γ R α}
:
def
HahnSeries.SummableFamily.ofFinsupp
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
(f : α →₀ HahnSeries Γ R)
:
A family with only finitely many nonzero elements is summable.
Equations
- HahnSeries.SummableFamily.ofFinsupp f = { toFun := ⇑f, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
@[simp]
theorem
HahnSeries.SummableFamily.coe_ofFinsupp
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{f : α →₀ HahnSeries Γ R}
:
⇑(HahnSeries.SummableFamily.ofFinsupp f) = ⇑f
@[simp]
theorem
HahnSeries.SummableFamily.hsum_ofFinsupp
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{f : α →₀ HahnSeries Γ R}
:
HahnSeries.SummableFamily.hsum (HahnSeries.SummableFamily.ofFinsupp f) = Finsupp.sum f fun (x : α) => id
def
HahnSeries.SummableFamily.embDomain
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{β : Type u_4}
(s : HahnSeries.SummableFamily Γ R α)
(f : α ↪ β)
:
A summable family can be reindexed by an embedding without changing its sum.
Equations
- HahnSeries.SummableFamily.embDomain s f = { toFun := fun (b : β) => if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
theorem
HahnSeries.SummableFamily.embDomain_apply
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{β : Type u_4}
(s : HahnSeries.SummableFamily Γ R α)
(f : α ↪ β)
{b : β}
:
(HahnSeries.SummableFamily.embDomain s f) b = if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0
@[simp]
theorem
HahnSeries.SummableFamily.embDomain_image
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{β : Type u_4}
(s : HahnSeries.SummableFamily Γ R α)
(f : α ↪ β)
{a : α}
:
(HahnSeries.SummableFamily.embDomain s f) (f a) = s a
@[simp]
theorem
HahnSeries.SummableFamily.embDomain_notin_range
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{β : Type u_4}
(s : HahnSeries.SummableFamily Γ R α)
(f : α ↪ β)
{b : β}
(h : b ∉ Set.range ⇑f)
:
(HahnSeries.SummableFamily.embDomain s f) b = 0
@[simp]
theorem
HahnSeries.SummableFamily.hsum_embDomain
{Γ : Type u_1}
{R : Type u_2}
[PartialOrder Γ]
[AddCommMonoid R]
{α : Type u_3}
{β : Type u_4}
(s : HahnSeries.SummableFamily Γ R α)
(f : α ↪ β)
:
def
HahnSeries.SummableFamily.powers
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[CommRing R]
[IsDomain R]
(x : HahnSeries Γ R)
(hx : 0 < (HahnSeries.addVal Γ R) x)
:
The powers of an element of positive valuation form a summable family.
Equations
- HahnSeries.SummableFamily.powers x hx = { toFun := fun (n : ℕ) => x ^ n, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
Instances For
@[simp]
theorem
HahnSeries.SummableFamily.coe_powers
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[CommRing R]
[IsDomain R]
{x : HahnSeries Γ R}
(hx : 0 < (HahnSeries.addVal Γ R) x)
:
⇑(HahnSeries.SummableFamily.powers x hx) = HPow.hPow x
theorem
HahnSeries.SummableFamily.embDomain_succ_smul_powers
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[CommRing R]
[IsDomain R]
{x : HahnSeries Γ R}
(hx : 0 < (HahnSeries.addVal Γ R) x)
:
HahnSeries.SummableFamily.embDomain (x • HahnSeries.SummableFamily.powers x hx)
{ toFun := Nat.succ, inj' := Nat.succ_injective } = HahnSeries.SummableFamily.powers x hx - HahnSeries.SummableFamily.ofFinsupp (Finsupp.single 0 1)
theorem
HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedCancelAddCommMonoid Γ]
[CommRing R]
[IsDomain R]
{x : HahnSeries Γ R}
(hx : 0 < (HahnSeries.addVal Γ R) x)
:
(1 - x) * HahnSeries.SummableFamily.hsum (HahnSeries.SummableFamily.powers x hx) = 1
theorem
HahnSeries.unit_aux
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedAddCommGroup Γ]
[CommRing R]
[IsDomain R]
(x : HahnSeries Γ R)
{r : R}
(hr : r * x.coeff (HahnSeries.order x) = 1)
:
0 < (HahnSeries.addVal Γ R) (1 - HahnSeries.C r * (HahnSeries.single (-HahnSeries.order x)) 1 * x)
theorem
HahnSeries.isUnit_iff
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedAddCommGroup Γ]
[CommRing R]
[IsDomain R]
{x : HahnSeries Γ R}
:
IsUnit x ↔ IsUnit (x.coeff (HahnSeries.order x))
instance
HahnSeries.instFieldHahnSeriesToPartialOrderToOrderedAddCommGroupToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifield
{Γ : Type u_1}
{R : Type u_2}
[LinearOrderedAddCommGroup Γ]
[Field R]
:
Field (HahnSeries Γ R)
Equations
- One or more equations did not get rendered due to their size.