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 Γ R
defines anAddValuation
onHahnSeries Γ R
whenΓ
is linearly ordered.- A
HahnSeries.SummableFamily
is 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 aLinearMap
asHahnSeries.SummableFamily.lsum
. Note that this is different fromSummable
in 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]
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 ↑x.order) ⋯ ⋯ ⋯ ⋯
Instances For
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' : (⋃ (a : α), (self.toFun a).support).IsPWO
- finite_co_support' : ∀ (g : Γ), {a : α | (self.toFun a).coeff g ≠ 0}.Finite
Instances For
Equations
- HahnSeries.SummableFamily.instFunLike = { coe := HahnSeries.SummableFamily.toFun, coe_injective' := ⋯ }
Equations
- HahnSeries.SummableFamily.instAdd = { add := fun (x y : HahnSeries.SummableFamily Γ R α) => { toFun := ⇑x + ⇑y, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
Equations
- HahnSeries.SummableFamily.instZero = { zero := { toFun := 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
Equations
- HahnSeries.SummableFamily.instInhabited = { default := 0 }
Equations
- HahnSeries.SummableFamily.instAddCommMonoid = AddCommMonoid.mk ⋯
The infinite sum of a SummableFamily
of Hahn series.
Equations
- s.hsum = { coeff := fun (g : Γ) => ∑ᶠ (i : α), (s i).coeff g, isPWO_support' := ⋯ }
Instances For
Equations
- HahnSeries.SummableFamily.instNeg = { neg := fun (s : HahnSeries.SummableFamily Γ R α) => { toFun := fun (a : α) => -s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } }
Equations
- HahnSeries.SummableFamily.instAddCommGroup = let __src := inferInstanceAs (AddCommMonoid (HahnSeries.SummableFamily Γ R α)); AddCommGroup.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
The summation of a summable_family
as a LinearMap
.
Equations
- HahnSeries.SummableFamily.lsum = { toFun := HahnSeries.SummableFamily.hsum, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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
A summable family can be reindexed by an embedding without changing its sum.
Equations
- s.embDomain 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
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' := ⋯ }