This is an auxiliary domain to ease the implementation of order computations.
In fact, we want to model that an order of a series can be a non-negative integer, ∞, or unknown. So we have, natural numbers with two more values, infinity and unknown.
Description
Models computations with orders or series.
The domain models ℕ ∪ where ∞ and ? are two new symbols.
The symbol ∞ models the order of the zero series. Its arithmetic is given by
min(∞,x) | = x | ∀x | ∈ ℕ ∪, | (106) |
∞ + x | = ∞ | ∀x | ∈ ℕ ∪, | (107) |
∞⋅ x | = ∞ | ∀x | ∈ ℕ ∪. | (108) |
x ⋅∞ | = | (109) |
Since we deal with a lazy implementation of series, it might be the case that the order of a series is not yet known. The symbol ? models the fact that the order is not known. Its arithmetic is given by
min(?,x) | = ? | ∀x | ∈ ℕ ∪, | (110) |
? + x | = ? | ∀x | ∈ ℕ ∪, | (111) |
? ⋅ x | = ? | ∀x | ∈ ℕ ∪. | (112) |
Corresponding to the differentiation and integration of a formal power series, we have:
boundedDecrement(x) | = x | ∀x | ∈, | (113) |
increment(x) | = x | ∀x | ∈ | (114) |
See also
FormalPowerSeries, OrdinaryGeneratingSeries, ExponentialGeneratingSeries
Exports of SeriesOrder
unknown: % An order if the order is not known.
infinity: % The order of the zero series.
0: % The order of the series 1.
1: % The order of the series x.
coerce: MachineInteger -> % Create an order from a natural number.
coerce: % -> MachineInteger Coercion of an order to a MachineInteger.
=: (%, %) -> Boolean Compares two orders.
min: (%, %) -> % Compute the order of the sum of two series.
+: (%, %) -> % Compute the order of the product of two series.
*: (%, %) -> % Compute the order of the composition of two series.
boundedDecrement: % -> % Compute the order of the derivative of a series.
increment: % -> % Compute the order of the integral of a series.
Export of SeriesOrder
coerce: MachineInteger -> %
Description
Create an order from a natural number.
Export of SeriesOrder
coerce: % -> MachineInteger
Description
Coercion of an order to a MachineInteger.
Export of SeriesOrder
min: (%, %) -> %
Description
Compute the order of the sum of two series.
In general, the order of the sum of two series x and y is coverned by the inequality
(115) |
The operation min turns SeriesOrder into a commutative semigroup.
Export of SeriesOrder
+: (%, %) -> %
Description
Compute the order of the product of two series.
In general, the order of the product of two series x and y is coverned by the equation
(116) |
The operation + together with 0 turns SeriesOrder into a commutative monoid.
Export of SeriesOrder
*: (%, %) -> %
Description
Compute the order of the composition of two series.
In general, the order of the composition of two series x and y is coverned by the equation
(117) |
The operation * together with 1 turns SeriesOrder into a commutative monoid.
Export of SeriesOrder
boundedDecrement: % -> %
Description
Compute the order of the derivative of a series.
The order of the derivative of a series x is given by
(118) |
Export of SeriesOrder
increment: % -> %
Description
Compute the order of the integral of a series.
The order of the integral of a series x is given by
(119) |
min, +, *, boundedDecrement