omnibias.core.verified.taylor_model
Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.
import omnibias.core.verified.taylor_modelModule contract & mathematical conventions
Taylor models: rigorous function enclosures over a whole interval cell.
A degree-d Taylor model on a cell [center - h, center + h] is a pair
f(x) \in P(x - center) + R \quad \forall x \in [center - h, center + h],
where P is a polynomial with Interval coefficients (in the *relative*
variable X = x - center) and R is an Interval *remainder* that
rigorously absorbs everything the polynomial omits. Unlike a bare interval, a
Taylor model keeps the *shape* of the function, so multiplying / composing does
not suffer the wrapping blow-up of naive interval evaluation and the
bound over the cell stays tight.
This is the object that discharges the certified-evidence analytic_tail_operator_bound
and rigorous-quadrature obligations: the truncation remainder R *is* the
certified tail term.
Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.
TaylorModel
omnibias.core.verified.TaylorModelSource ↗class TaylorModelDegree-order Taylor model on a symmetric cell about center.
Parameters
| Name | Type & default | Contract |
|---|---|---|
centerpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
radiuspositional-or-keyword | floatRequired | See the operation contract and implementation below. |
coeffspositional-or-keyword | Sequence[Interval]Required | See the operation contract and implementation below. |
remainderpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
Executed regression · identity bound is cell
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_identity_bound_is_cell() -> None:
tm = TaylorModel.identity(0.5, 0.25, order=4)
b = tm.bound()
assert b.lo <= 0.25
assert b.hi >= 0.75python -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_identity_bound_is_cell" -qRegression example · constant model
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_constant_model() -> None:
tm = TaylorModel.constant(3.5, center=1.0, radius=2.0, order=3)
b = tm.bound()
assert b.lo <= 3.5 <= b.hi
assert b.width < 1e-12python -m pytest packages/omnibias-core/tests/verified/test_taylor_model.py -k test_constant_model -qFields & methods
__init__method
__init__(self, center: float, radius: float, coeffs: Sequence[Interval], remainder: Interval) -> NoneSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
centerpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
radiuspositional-or-keyword | floatRequired | See the operation contract and implementation below. |
coeffspositional-or-keyword | Sequence[Interval]Required | See the operation contract and implementation below. |
remainderpositional-or-keyword | IntervalRequired | See the operation contract and implementation below. |
Returns: None
Validation & failure cases
- When
radius < 0.0, raisesValueError('cell radius must be non-negative'). - When
not coeffs, raisesValueError('a Taylor model needs at least one coefficient').
Executed regression · identity bound is cell
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_identity_bound_is_cell() -> None:
tm = TaylorModel.identity(0.5, 0.25, order=4)
b = tm.bound()
assert b.lo <= 0.25
assert b.hi >= 0.75python -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_identity_bound_is_cell" -qMethod implementation
def __init__(
self,
center: float,
radius: float,
coeffs: Sequence[Interval],
remainder: Interval,
) -> None:
if radius < 0.0:
raise ValueError("cell radius must be non-negative")
if not coeffs:
raise ValueError("a Taylor model needs at least one coefficient")
self.center = float(center)
self.radius = float(radius)
self.order = len(coeffs) - 1
self.coeffs: list[Interval] = list(coeffs)
self.remainder = remainderconstantmethod
constant(cls, value: IntervalLike, center: float, radius: float, order: int) -> TaylorModelSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
valuepositional-or-keyword | IntervalLikeRequired | See the operation contract and implementation below. |
centerpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
radiuspositional-or-keyword | floatRequired | See the operation contract and implementation below. |
orderpositional-or-keyword | intRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Executed regression · g2 non vacuous
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_non_vacuous() -> None:
ex = worked_example()
assert float(ex["remainder_width"]) < 0.1
assert ex["vacuous"] is False
assert float(ex["width"]) < 0.1python -m pytest "packages/omnibias-core/tests/verified/test_tm_neuron.py::test_g2_non_vacuous" -qMethod implementation
def constant(cls, value: IntervalLike, center: float, radius: float, order: int) -> TaylorModel:
coeffs = [Interval.from_value(value)] + [Interval.point(0.0) for _ in range(order)]
return cls(center, radius, coeffs, Interval.point(0.0))identitymethod
identity(cls, center: float, radius: float, order: int) -> TaylorModelThe model of f(x) = x (= center + X) on the cell.
Parameters
| Name | Type & default | Contract |
|---|---|---|
centerpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
radiuspositional-or-keyword | floatRequired | See the operation contract and implementation below. |
orderpositional-or-keyword | intRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Executed regression · identity bound is cell
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_identity_bound_is_cell() -> None:
tm = TaylorModel.identity(0.5, 0.25, order=4)
b = tm.bound()
assert b.lo <= 0.25
assert b.hi >= 0.75python -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_identity_bound_is_cell" -qMethod implementation
def identity(cls, center: float, radius: float, order: int) -> TaylorModel:
"""The model of ``f(x) = x`` (``= center + X``) on the cell."""
coeffs = [Interval.point(center)] + [Interval.point(0.0) for _ in range(order)]
if order >= 1:
coeffs[1] = Interval.point(1.0)
return cls(center, radius, coeffs, Interval.point(0.0))boundmethod
bound(self) -> IntervalGuaranteed enclosure of f over the whole cell.
Returns: Interval
Executed regression · identity bound is cell
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_identity_bound_is_cell() -> None:
tm = TaylorModel.identity(0.5, 0.25, order=4)
b = tm.bound()
assert b.lo <= 0.25
assert b.hi >= 0.75python -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_identity_bound_is_cell" -qMethod implementation
def bound(self) -> Interval:
"""Guaranteed enclosure of ``f`` over the whole cell."""
x = self._rel()
acc = self.coeffs[-1]
for c in reversed(self.coeffs[:-1]):
acc = acc * x + c
return acc + self.remainder__add__method
__add__(self, other: TaylorModel | IntervalLike) -> TaylorModelSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
otherpositional-or-keyword | TaylorModel | IntervalLikeRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Executed regression · g2 non vacuous
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_non_vacuous() -> None:
ex = worked_example()
assert float(ex["remainder_width"]) < 0.1
assert ex["vacuous"] is False
assert float(ex["width"]) < 0.1python -m pytest "packages/omnibias-core/tests/verified/test_tm_neuron.py::test_g2_non_vacuous" -qMethod implementation
def __add__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
if isinstance(other, TaylorModel):
self._check(other)
coeffs = [a + b for a, b in zip(self.coeffs, other.coeffs, strict=True)]
return TaylorModel(self.center, self.radius, coeffs, self.remainder + other.remainder)
coeffs = list(self.coeffs)
coeffs[0] = coeffs[0] + Interval.from_value(other)
return TaylorModel(self.center, self.radius, coeffs, self.remainder)__neg__method
__neg__(self) -> TaylorModelSee the class contract above and the exact method implementation below.
Returns: TaylorModel
Executed regression · reciprocal encloses affine pointwise
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_reciprocal_encloses_affine_pointwise() -> None:
center, radius = 2.0, 0.3
x = TaylorModel.identity(center, radius, order=6)
inv = x.reciprocal()
b = inv.bound()
for xi in _sample(center, radius):
assert b.lo <= 1.0 / xi <= b.hipython -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_reciprocal_encloses_affine_pointwise" -qMethod implementation
def __neg__(self) -> TaylorModel:
return TaylorModel(
self.center, self.radius, [-c for c in self.coeffs], -self.remainder
)__sub__method
__sub__(self, other: TaylorModel | IntervalLike) -> TaylorModelSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
otherpositional-or-keyword | TaylorModel | IntervalLikeRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Executed regression · g2 non vacuous
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_non_vacuous() -> None:
ex = worked_example()
assert float(ex["remainder_width"]) < 0.1
assert ex["vacuous"] is False
assert float(ex["width"]) < 0.1python -m pytest "packages/omnibias-core/tests/verified/test_tm_neuron.py::test_g2_non_vacuous" -qMethod implementation
def __sub__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
return self.__add__(-other if isinstance(other, TaylorModel) else -Interval.from_value(other))__mul__method
__mul__(self, other: TaylorModel | IntervalLike) -> TaylorModelSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
otherpositional-or-keyword | TaylorModel | IntervalLikeRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Executed regression · g2 non vacuous
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_non_vacuous() -> None:
ex = worked_example()
assert float(ex["remainder_width"]) < 0.1
assert ex["vacuous"] is False
assert float(ex["width"]) < 0.1python -m pytest "packages/omnibias-core/tests/verified/test_tm_neuron.py::test_g2_non_vacuous" -qMethod implementation
def __mul__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
if not isinstance(other, TaylorModel):
scal = Interval.from_value(other)
return TaylorModel(
self.center, self.radius, [c * scal for c in self.coeffs], self.remainder * scal
)
self._check(other)
d = self.order
full = _conv(self.coeffs, other.coeffs) # length 2d + 1
low = full[: d + 1]
x = self._rel()
# Bound the truncated high part sum_{k=d+1}^{2d} full[k] * X^k over the cell
# by factoring out X^{d+1} and Horner-evaluating the inner polynomial.
high = Interval.point(0.0)
if d >= 1 and len(full) > d + 1:
inner = full[2 * d]
for k in range(2 * d - 1, d, -1):
inner = inner * x + full[k]
high = inner * x.pow_int(d + 1)
# f*g = P*Q + P*Rg + Q*Rf + Rf*Rg, with P,Q the polynomial parts.
remainder = (
high
+ self._poly_bound() * other.remainder
+ other._poly_bound() * self.remainder
+ self.remainder * other.remainder
)
return TaylorModel(self.center, self.radius, low, remainder)antiderivativemethod
antiderivative(self) -> TaylorModelRigorous antiderivative F(x) = \int_{center}^{x} f(t)\,dt (so F(center)=0).
Integration is the natural *sound* operation on a Taylor model (unlike
differentiation, whose action on a flat remainder is uncontrolled). The
polynomial part integrates term-by-term in the relative variable
X = x - center -- raising the degree by one, so the result has order
order + 1 -- and the remainder integrates rigorously,
\int_0^X R\,dt \in R \cdot [-h, h] \qquad (h = \text{radius}),
because \int_0^X e(t)\,dt = X\cdot\bar e with the mean value
\bar e \in R for any e enclosed by R. Composing
antiderivative with bound gives a certified definite
integral over the cell.
Returns: TaylorModel
Executed regression · antiderivative of x squared
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_antiderivative_of_x_squared() -> None:
# f(x) = x^2 on [-0.5, 0.5]; F = x^3 / 3.
f = TaylorModel(
0.0,
0.5,
[Interval.point(0.0), Interval.point(0.0), Interval.point(1.0)],
Interval.point(0.0),
)
F = f.antiderivative()
assert F.order == 3
assert F.coeffs[0].lo == 0.0 and F.coeffs[0].hi == 0.0
assert abs(F.coeffs[3].mid - 1.0 / 3.0) < 1e-15
assert F.coeffs[1].mid == 0.0 and F.coeffs[2].mid == 0.0python -m pytest "packages/omnibias-core/tests/test_verified_tm_integral.py::test_antiderivative_of_x_squared" -qMethod implementation
def antiderivative(self) -> TaylorModel:
r"""Rigorous antiderivative ``F(x) = \int_{center}^{x} f(t)\,dt`` (so ``F(center)=0``).
Integration is the natural *sound* operation on a Taylor model (unlike
differentiation, whose action on a flat remainder is uncontrolled). The
polynomial part integrates term-by-term in the relative variable
``X = x - center`` -- raising the degree by one, so the result has order
``order + 1`` -- and the remainder integrates rigorously,
.. math::
\int_0^X R\,dt \in R \cdot [-h, h]
\qquad (h = \text{radius}),
because ``\int_0^X e(t)\,dt = X\cdot\bar e`` with the mean value
``\bar e \in R`` for any ``e`` enclosed by ``R``. Composing
:meth:`antiderivative` with :meth:`bound` gives a certified definite
integral over the cell.
"""
new_coeffs = [Interval.point(0.0)]
for k, c in enumerate(self.coeffs):
new_coeffs.append(c * Interval.from_rational(Fraction(1, k + 1)))
rem = self.remainder * self._rel()
return TaylorModel(self.center, self.radius, new_coeffs, rem)definite_integralmethod
definite_integral(self) -> IntervalCertified \int_{center-h}^{center+h} f(x)\,dx over the whole cell.
The symmetric cell kills the odd polynomial terms
(\int_{-h}^{h} X^k\,dX = 0 for odd k, = 2 h^{k+1}/(k+1) for
even k); the remainder contributes R \cdot 2h since
\int_{-h}^{h} e(X)\,dX = 2h\,\bar e with \bar e \in R.
Returns: Interval
Executed regression · higher order gives tighter residual
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_higher_order_gives_tighter_residual() -> None:
a, b = -0.4, 0.4
w_lo = certified_ftc_residual("tanh", a, b, k=1, order=10).width
w_hi = certified_ftc_residual("tanh", a, b, k=1, order=4).width
assert w_lo < w_hi # the Taylor-model remainder shrinks with orderpython -m pytest "packages/omnibias-core/tests/verified/test_ftc.py::test_higher_order_gives_tighter_residual" -qMethod implementation
def definite_integral(self) -> Interval:
r"""Certified ``\int_{center-h}^{center+h} f(x)\,dx`` over the whole cell.
The symmetric cell kills the odd polynomial terms
(``\int_{-h}^{h} X^k\,dX = 0`` for odd ``k``, ``= 2 h^{k+1}/(k+1)`` for
even ``k``); the remainder contributes ``R \cdot 2h`` since
``\int_{-h}^{h} e(X)\,dX = 2h\,\bar e`` with ``\bar e \in R``.
"""
# Use the outward cell radius (``.hi`` of ``_rel``) rather than a bare
# ``Interval.point(radius)`` so the integral width cannot under-cover the
# claimed cell by a ulp.
h = Interval.point(self._rel().hi)
acc = Interval.point(0.0)
for k, c in enumerate(self.coeffs):
if k % 2 == 0:
acc = acc + c * h.pow_int(k + 1) * Interval.from_rational(
Fraction(2, k + 1)
)
return acc + self.remainder * (h * Interval.from_rational(2))pow_intmethod
pow_int(self, n: int) -> TaylorModelSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
npositional-or-keyword | intRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Validation & failure cases
- When
n < 0, raisesValueError('Taylor-model powers require n >= 0').
Executed regression · polynomial product encloses pointwise
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_polynomial_product_encloses_pointwise() -> None:
center, radius = 0.3, 0.4
x = TaylorModel.identity(center, radius, order=5)
# f(x) = (x^2 + 1) * (x - 2)
f = (x.pow_int(2) + 1.0) * (x - 2.0)
b = f.bound()
for xi in _sample(center, radius):
val = (xi * xi + 1.0) * (xi - 2.0)
assert b.lo <= val <= b.hipython -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_polynomial_product_encloses_pointwise" -qMethod implementation
def pow_int(self, n: int) -> TaylorModel:
if n < 0:
raise ValueError("Taylor-model powers require n >= 0")
result = TaylorModel.constant(1.0, self.center, self.radius, self.order)
base = self
e = n
while e > 0:
if e & 1:
result = result * base
e >>= 1
if e > 0:
base = base * base
return resultreciprocalmethod
reciprocal(self) -> TaylorModelRigorous Taylor model of 1 / f over the whole cell.
Factor 1/f = (1/c0) * 1/(1 + g) about the scalar expansion point
c0 = mid(coeffs[0]) with g = (f - c0)/c0 (which has a near-zero
constant term), then expand 1/(1 + g) = sum_{k>=0} (-g)^k. The first
order + 1 terms are kept as a Taylor model; the omitted analytic tail
is bounded by the geometric series tau^{order+1} / (1 - tau) where
tau rigorously bounds |g| over the cell. Requires f to stay
bounded away from 0 on the cell and the cell to be narrow enough that
the relative variation tau < 1 (otherwise ValueError).
Returns: TaylorModel
Validation & failure cases
- When
rng.lo <= 0.0 <= rng.hi, raisesValueError('TaylorModel.reciprocal requires f to be bounded away from 0 on the cell'). - When
c0.lo == 0.0, raisesValueError('TaylorModel.reciprocal needs a non-zero expansion point; narrow the cell'). - When
tau >= 1.0, raisesValueError('TaylorModel.reciprocal series does not converge on this cell (narrow the cell so the relative variation is < 1)').
Executed regression · reciprocal rejects zero crossing
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_reciprocal_rejects_zero_crossing() -> None:
x = TaylorModel.identity(0.0, 1.0, order=4) # range [-1, 1] straddles 0
with pytest.raises(ValueError, match="bounded away from 0"):
x.reciprocal()python -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_reciprocal_rejects_zero_crossing" -qMethod implementation
def reciprocal(self) -> TaylorModel:
r"""Rigorous Taylor model of ``1 / f`` over the whole cell.
Factor ``1/f = (1/c0) * 1/(1 + g)`` about the scalar expansion point
``c0 = mid(coeffs[0])`` with ``g = (f - c0)/c0`` (which has a near-zero
constant term), then expand ``1/(1 + g) = sum_{k>=0} (-g)^k``. The first
``order + 1`` terms are kept as a Taylor model; the omitted analytic tail
is bounded by the geometric series ``tau^{order+1} / (1 - tau)`` where
``tau`` rigorously bounds ``|g|`` over the cell. Requires ``f`` to stay
bounded away from ``0`` on the cell and the cell to be narrow enough that
the relative variation ``tau < 1`` (otherwise :class:`ValueError`).
"""
rng = self.bound()
if rng.lo <= 0.0 <= rng.hi:
raise ValueError(
"TaylorModel.reciprocal requires f to be bounded away from 0 on the cell"
)
c0 = Interval.point(self.coeffs[0].mid)
if c0.lo == 0.0:
raise ValueError(
"TaylorModel.reciprocal needs a non-zero expansion point; narrow the cell"
)
inv_c0 = c0.reciprocal()
shifted = [self.coeffs[0] - c0, *self.coeffs[1:]]
f_minus_c0 = TaylorModel(self.center, self.radius, shifted, self.remainder)
g = f_minus_c0 * inv_c0
# `.mag` is the outward-rounded magnitude accessor (a hand-rolled
# max(abs(lo), abs(hi)) would sit one ulp lower); the geometric tail below
# grows with tau, so only the outward value keeps the remainder sound.
tau = g.bound().mag
if tau >= 1.0:
raise ValueError(
"TaylorModel.reciprocal series does not converge on this cell "
"(narrow the cell so the relative variation is < 1)"
)
neg_g = -g
series = TaylorModel.constant(1.0, self.center, self.radius, self.order)
term = TaylorModel.constant(1.0, self.center, self.radius, self.order)
for _ in range(self.order):
term = term * neg_g
series = series + term
tail = float(
(
Interval.point(tau).pow_int(self.order + 1)
* (Interval.point(1.0) - Interval.point(tau)).reciprocal()
).hi
)
series = TaylorModel(
self.center,
self.radius,
series.coeffs,
series.remainder + Interval(-tail, tail),
)
return series * inv_c0sqrtmethod
sqrt(self) -> TaylorModelRigorous Taylor model of sqrt(f) over the whole cell.
Factor sqrt(f) = sqrt(c0) * sqrt(1 + g) about the scalar expansion
point c0 = mid(coeffs[0]) > 0 with g = (f - c0)/c0 (relative
variation, |g| <= tau), then keep the first order + 1 terms of the
binomial series sqrt(1 + g) = sum_k binom(1/2, k) g^k. The omitted
analytic tail is bounded by the Lagrange remainder
|R| \le \Big|\binom{1/2}{m+1}\Big|\,(1 - \tau)^{1/2 - (m+1)}\,\tau^{m+1} \qquad (m = \text{order}),
valid because 1 + g \ge 1 - tau > 0 on the cell and the (m+1)-st
derivative of sqrt(1+\cdot) is monotone there. Requires f > 0 on
the cell and tau < 1 (otherwise ValueError).
Returns: TaylorModel
Validation & failure cases
- When
rng.lo <= 0.0, raisesValueError('TaylorModel.sqrt requires f > 0 on the cell'). - When
c0.lo <= 0.0, raisesValueError('TaylorModel.sqrt needs a positive expansion point; narrow the cell'). - When
tau >= 1.0, raisesValueError('TaylorModel.sqrt series does not converge on this cell (narrow the cell so the relative variation is < 1)').
Executed regression · sqrt rejects nonpositive cell
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_sqrt_rejects_nonpositive_cell() -> None:
x = TaylorModel.identity(0.0, 1.0, order=4) # range [-1, 1] includes <= 0
with pytest.raises(ValueError, match="requires f > 0"):
x.sqrt()python -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_sqrt_rejects_nonpositive_cell" -qMethod implementation
def sqrt(self) -> TaylorModel:
r"""Rigorous Taylor model of ``sqrt(f)`` over the whole cell.
Factor ``sqrt(f) = sqrt(c0) * sqrt(1 + g)`` about the scalar expansion
point ``c0 = mid(coeffs[0]) > 0`` with ``g = (f - c0)/c0`` (relative
variation, ``|g| <= tau``), then keep the first ``order + 1`` terms of the
binomial series ``sqrt(1 + g) = sum_k binom(1/2, k) g^k``. The omitted
analytic tail is bounded by the Lagrange remainder
.. math::
|R| \le \Big|\binom{1/2}{m+1}\Big|\,(1 - \tau)^{1/2 - (m+1)}\,\tau^{m+1}
\qquad (m = \text{order}),
valid because ``1 + g \ge 1 - tau > 0`` on the cell and the ``(m+1)``-st
derivative of ``sqrt(1+\cdot)`` is monotone there. Requires ``f > 0`` on
the cell and ``tau < 1`` (otherwise :class:`ValueError`).
"""
rng = self.bound()
if rng.lo <= 0.0:
raise ValueError("TaylorModel.sqrt requires f > 0 on the cell")
c0 = Interval.point(self.coeffs[0].mid)
if c0.lo <= 0.0:
raise ValueError("TaylorModel.sqrt needs a positive expansion point; narrow the cell")
inv_c0 = c0.reciprocal()
shifted = [self.coeffs[0] - c0, *self.coeffs[1:]]
g = TaylorModel(self.center, self.radius, shifted, self.remainder) * inv_c0
tau = g.bound().mag
if tau >= 1.0:
raise ValueError(
"TaylorModel.sqrt series does not converge on this cell "
"(narrow the cell so the relative variation is < 1)"
)
series = TaylorModel.constant(1.0, self.center, self.radius, self.order)
gpow = TaylorModel.constant(1.0, self.center, self.radius, self.order)
coeff = Fraction(1, 1)
for k in range(1, self.order + 1):
coeff = coeff * (Fraction(1, 2) - (k - 1)) / k
gpow = gpow * g
series = series + gpow * Interval.from_rational(coeff)
next_coeff = abs(coeff * (Fraction(1, 2) - self.order) / (self.order + 1))
one_minus = Interval.point(1.0) - Interval.point(tau)
# (1 - tau)^{1/2 - (order+1)} = 1 / ((1 - tau)^order * sqrt(1 - tau))
denom = one_minus.pow_int(self.order) * one_minus.sqrt()
tail = float(
(
Interval.from_rational(next_coeff)
* Interval.point(tau).pow_int(self.order + 1)
* denom.reciprocal()
).hi
)
series = TaylorModel(
self.center,
self.radius,
series.coeffs,
series.remainder + Interval(-tail, tail),
)
return series * c0.sqrt()__truediv__method
__truediv__(self, other: TaylorModel | IntervalLike) -> TaylorModelSee the class contract above and the exact method implementation below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
otherpositional-or-keyword | TaylorModel | IntervalLikeRequired | See the operation contract and implementation below. |
Returns: TaylorModel
Executed regression · reciprocal scalar divisor
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_reciprocal_scalar_divisor() -> None:
center, radius = 1.0, 0.2
x = TaylorModel.identity(center, radius, order=4)
half = (x / 2.0).bound()
for xi in _sample(center, radius):
assert half.lo <= xi / 2.0 <= half.hipython -m pytest "packages/omnibias-core/tests/verified/test_taylor_model.py::test_reciprocal_scalar_divisor" -qMethod implementation
def __truediv__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
if isinstance(other, TaylorModel):
self._check(other)
return self * other.reciprocal()
return self * Interval.from_value(other).reciprocal()__repr__method
__repr__(self) -> strSee the class contract above and the exact method implementation below.
Returns: str
Method implementation
def __repr__(self) -> str:
return (
f"TaylorModel(center={self.center!r}, radius={self.radius!r}, "
f"order={self.order}, remainder={self.remainder!r})"
)centerattribute
center = float(center)Public instance attribute assigned by __init__. The source assignment is center = float(center); it describes instance state, not a literal constructor default.
Regression example · taylor model roundtrip is bit exact
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_taylor_model_roundtrip_is_bit_exact() -> None:
tm = TaylorModel(
0.3,
0.25,
[Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
Interval(-1e-12, 1e-12),
)
again = decode_taylor_model(encode_taylor_model(tm))
assert again.center == tm.center
assert again.radius == tm.radius
assert again.order == tm.order
assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_taylor_model_roundtrip_is_bit_exact -qradiusattribute
radius = float(radius)Public instance attribute assigned by __init__. The source assignment is radius = float(radius); it describes instance state, not a literal constructor default.
Regression example · taylor model roundtrip is bit exact
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_taylor_model_roundtrip_is_bit_exact() -> None:
tm = TaylorModel(
0.3,
0.25,
[Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
Interval(-1e-12, 1e-12),
)
again = decode_taylor_model(encode_taylor_model(tm))
assert again.center == tm.center
assert again.radius == tm.radius
assert again.order == tm.order
assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_taylor_model_roundtrip_is_bit_exact -qorderattribute
order = len(coeffs) - 1Public instance attribute assigned by __init__. The source assignment is order = len(coeffs) - 1; it describes instance state, not a literal constructor default.
Regression example · taylor model roundtrip is bit exact
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_taylor_model_roundtrip_is_bit_exact() -> None:
tm = TaylorModel(
0.3,
0.25,
[Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
Interval(-1e-12, 1e-12),
)
again = decode_taylor_model(encode_taylor_model(tm))
assert again.center == tm.center
assert again.radius == tm.radius
assert again.order == tm.order
assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_taylor_model_roundtrip_is_bit_exact -qcoeffsattribute
coeffs: list[Interval] = list(coeffs)Public instance attribute assigned by __init__. The source assignment is coeffs = list(coeffs); it describes instance state, not a literal constructor default.
Regression example · taylor model roundtrip is bit exact
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_taylor_model_roundtrip_is_bit_exact() -> None:
tm = TaylorModel(
0.3,
0.25,
[Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
Interval(-1e-12, 1e-12),
)
again = decode_taylor_model(encode_taylor_model(tm))
assert again.center == tm.center
assert again.radius == tm.radius
assert again.order == tm.order
assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_taylor_model_roundtrip_is_bit_exact -qremainderattribute
remainder: Interval = remainderPublic instance attribute assigned by __init__. The source assignment is remainder = remainder; it describes instance state, not a literal constructor default.
Regression example · taylor model roundtrip is bit exact
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_taylor_model_roundtrip_is_bit_exact() -> None:
tm = TaylorModel(
0.3,
0.25,
[Interval(1.0, 1.0), Interval(-0.5, -0.4999999999999999), Interval(0.0, 1e-17)],
Interval(-1e-12, 1e-12),
)
again = decode_taylor_model(encode_taylor_model(tm))
assert again.center == tm.center
assert again.radius == tm.radius
assert again.order == tm.order
assert [(c.lo, c.hi) for c in again.coeffs] == [(c.lo, c.hi) for c in tm.coeffs]
assert (again.remainder.lo, again.remainder.hi) == (tm.remainder.lo, tm.remainder.hi)python -m pytest packages/omnibias-core/tests/test_certificate.py -k test_taylor_model_roundtrip_is_bit_exact -qRead the implementation
class TaylorModel:
"""Degree-``order`` Taylor model on a symmetric cell about ``center``."""
__slots__ = ("center", "radius", "order", "coeffs", "remainder")
def __init__(
self,
center: float,
radius: float,
coeffs: Sequence[Interval],
remainder: Interval,
) -> None:
if radius < 0.0:
raise ValueError("cell radius must be non-negative")
if not coeffs:
raise ValueError("a Taylor model needs at least one coefficient")
self.center = float(center)
self.radius = float(radius)
self.order = len(coeffs) - 1
self.coeffs: list[Interval] = list(coeffs)
self.remainder = remainder
# ----- constructors -------------------------------------------------- #
@classmethod
def constant(cls, value: IntervalLike, center: float, radius: float, order: int) -> TaylorModel:
coeffs = [Interval.from_value(value)] + [Interval.point(0.0) for _ in range(order)]
return cls(center, radius, coeffs, Interval.point(0.0))
@classmethod
def identity(cls, center: float, radius: float, order: int) -> TaylorModel:
"""The model of ``f(x) = x`` (``= center + X``) on the cell."""
coeffs = [Interval.point(center)] + [Interval.point(0.0) for _ in range(order)]
if order >= 1:
coeffs[1] = Interval.point(1.0)
return cls(center, radius, coeffs, Interval.point(0.0))
# ----- helpers ------------------------------------------------------- #
def _rel(self) -> Interval:
"""The relative variable ``X = x - center`` over the cell.
Always routed through :func:`_cell_rel` so the cell can never be rebuilt
inconsistently and every endpoint is outward-inflated.
"""
return _cell_rel(self.radius)
def _check(self, other: TaylorModel) -> None:
if self.center != other.center or self.radius != other.radius:
raise ValueError("Taylor models must share the same cell")
if self.order != other.order:
raise ValueError("Taylor models must share the same truncation order")
def bound(self) -> Interval:
"""Guaranteed enclosure of ``f`` over the whole cell."""
x = self._rel()
acc = self.coeffs[-1]
for c in reversed(self.coeffs[:-1]):
acc = acc * x + c
return acc + self.remainder
# ----- arithmetic ---------------------------------------------------- #
def __add__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
if isinstance(other, TaylorModel):
self._check(other)
coeffs = [a + b for a, b in zip(self.coeffs, other.coeffs, strict=True)]
return TaylorModel(self.center, self.radius, coeffs, self.remainder + other.remainder)
coeffs = list(self.coeffs)
coeffs[0] = coeffs[0] + Interval.from_value(other)
return TaylorModel(self.center, self.radius, coeffs, self.remainder)
__radd__ = __add__
def __neg__(self) -> TaylorModel:
return TaylorModel(
self.center, self.radius, [-c for c in self.coeffs], -self.remainder
)
def __sub__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
return self.__add__(-other if isinstance(other, TaylorModel) else -Interval.from_value(other))
def __mul__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
if not isinstance(other, TaylorModel):
scal = Interval.from_value(other)
return TaylorModel(
self.center, self.radius, [c * scal for c in self.coeffs], self.remainder * scal
)
self._check(other)
d = self.order
full = _conv(self.coeffs, other.coeffs) # length 2d + 1
low = full[: d + 1]
x = self._rel()
# Bound the truncated high part sum_{k=d+1}^{2d} full[k] * X^k over the cell
# by factoring out X^{d+1} and Horner-evaluating the inner polynomial.
high = Interval.point(0.0)
if d >= 1 and len(full) > d + 1:
inner = full[2 * d]
for k in range(2 * d - 1, d, -1):
inner = inner * x + full[k]
high = inner * x.pow_int(d + 1)
# f*g = P*Q + P*Rg + Q*Rf + Rf*Rg, with P,Q the polynomial parts.
remainder = (
high
+ self._poly_bound() * other.remainder
+ other._poly_bound() * self.remainder
+ self.remainder * other.remainder
)
return TaylorModel(self.center, self.radius, low, remainder)
__rmul__ = __mul__
def _poly_bound(self) -> Interval:
"""Enclosure of the polynomial part only (no remainder)."""
x = self._rel()
acc = self.coeffs[-1]
for c in reversed(self.coeffs[:-1]):
acc = acc * x + c
return acc
def antiderivative(self) -> TaylorModel:
r"""Rigorous antiderivative ``F(x) = \int_{center}^{x} f(t)\,dt`` (so ``F(center)=0``).
Integration is the natural *sound* operation on a Taylor model (unlike
differentiation, whose action on a flat remainder is uncontrolled). The
polynomial part integrates term-by-term in the relative variable
``X = x - center`` -- raising the degree by one, so the result has order
``order + 1`` -- and the remainder integrates rigorously,
.. math::
\int_0^X R\,dt \in R \cdot [-h, h]
\qquad (h = \text{radius}),
because ``\int_0^X e(t)\,dt = X\cdot\bar e`` with the mean value
``\bar e \in R`` for any ``e`` enclosed by ``R``. Composing
:meth:`antiderivative` with :meth:`bound` gives a certified definite
integral over the cell.
"""
new_coeffs = [Interval.point(0.0)]
for k, c in enumerate(self.coeffs):
new_coeffs.append(c * Interval.from_rational(Fraction(1, k + 1)))
rem = self.remainder * self._rel()
return TaylorModel(self.center, self.radius, new_coeffs, rem)
def definite_integral(self) -> Interval:
r"""Certified ``\int_{center-h}^{center+h} f(x)\,dx`` over the whole cell.
The symmetric cell kills the odd polynomial terms
(``\int_{-h}^{h} X^k\,dX = 0`` for odd ``k``, ``= 2 h^{k+1}/(k+1)`` for
even ``k``); the remainder contributes ``R \cdot 2h`` since
``\int_{-h}^{h} e(X)\,dX = 2h\,\bar e`` with ``\bar e \in R``.
"""
# Use the outward cell radius (``.hi`` of ``_rel``) rather than a bare
# ``Interval.point(radius)`` so the integral width cannot under-cover the
# claimed cell by a ulp.
h = Interval.point(self._rel().hi)
acc = Interval.point(0.0)
for k, c in enumerate(self.coeffs):
if k % 2 == 0:
acc = acc + c * h.pow_int(k + 1) * Interval.from_rational(
Fraction(2, k + 1)
)
return acc + self.remainder * (h * Interval.from_rational(2))
def pow_int(self, n: int) -> TaylorModel:
if n < 0:
raise ValueError("Taylor-model powers require n >= 0")
result = TaylorModel.constant(1.0, self.center, self.radius, self.order)
base = self
e = n
while e > 0:
if e & 1:
result = result * base
e >>= 1
if e > 0:
base = base * base
return result
def reciprocal(self) -> TaylorModel:
r"""Rigorous Taylor model of ``1 / f`` over the whole cell.
Factor ``1/f = (1/c0) * 1/(1 + g)`` about the scalar expansion point
``c0 = mid(coeffs[0])`` with ``g = (f - c0)/c0`` (which has a near-zero
constant term), then expand ``1/(1 + g) = sum_{k>=0} (-g)^k``. The first
``order + 1`` terms are kept as a Taylor model; the omitted analytic tail
is bounded by the geometric series ``tau^{order+1} / (1 - tau)`` where
``tau`` rigorously bounds ``|g|`` over the cell. Requires ``f`` to stay
bounded away from ``0`` on the cell and the cell to be narrow enough that
the relative variation ``tau < 1`` (otherwise :class:`ValueError`).
"""
rng = self.bound()
if rng.lo <= 0.0 <= rng.hi:
raise ValueError(
"TaylorModel.reciprocal requires f to be bounded away from 0 on the cell"
)
c0 = Interval.point(self.coeffs[0].mid)
if c0.lo == 0.0:
raise ValueError(
"TaylorModel.reciprocal needs a non-zero expansion point; narrow the cell"
)
inv_c0 = c0.reciprocal()
shifted = [self.coeffs[0] - c0, *self.coeffs[1:]]
f_minus_c0 = TaylorModel(self.center, self.radius, shifted, self.remainder)
g = f_minus_c0 * inv_c0
# `.mag` is the outward-rounded magnitude accessor (a hand-rolled
# max(abs(lo), abs(hi)) would sit one ulp lower); the geometric tail below
# grows with tau, so only the outward value keeps the remainder sound.
tau = g.bound().mag
if tau >= 1.0:
raise ValueError(
"TaylorModel.reciprocal series does not converge on this cell "
"(narrow the cell so the relative variation is < 1)"
)
neg_g = -g
series = TaylorModel.constant(1.0, self.center, self.radius, self.order)
term = TaylorModel.constant(1.0, self.center, self.radius, self.order)
for _ in range(self.order):
term = term * neg_g
series = series + term
tail = float(
(
Interval.point(tau).pow_int(self.order + 1)
* (Interval.point(1.0) - Interval.point(tau)).reciprocal()
).hi
)
series = TaylorModel(
self.center,
self.radius,
series.coeffs,
series.remainder + Interval(-tail, tail),
)
return series * inv_c0
def sqrt(self) -> TaylorModel:
r"""Rigorous Taylor model of ``sqrt(f)`` over the whole cell.
Factor ``sqrt(f) = sqrt(c0) * sqrt(1 + g)`` about the scalar expansion
point ``c0 = mid(coeffs[0]) > 0`` with ``g = (f - c0)/c0`` (relative
variation, ``|g| <= tau``), then keep the first ``order + 1`` terms of the
binomial series ``sqrt(1 + g) = sum_k binom(1/2, k) g^k``. The omitted
analytic tail is bounded by the Lagrange remainder
.. math::
|R| \le \Big|\binom{1/2}{m+1}\Big|\,(1 - \tau)^{1/2 - (m+1)}\,\tau^{m+1}
\qquad (m = \text{order}),
valid because ``1 + g \ge 1 - tau > 0`` on the cell and the ``(m+1)``-st
derivative of ``sqrt(1+\cdot)`` is monotone there. Requires ``f > 0`` on
the cell and ``tau < 1`` (otherwise :class:`ValueError`).
"""
rng = self.bound()
if rng.lo <= 0.0:
raise ValueError("TaylorModel.sqrt requires f > 0 on the cell")
c0 = Interval.point(self.coeffs[0].mid)
if c0.lo <= 0.0:
raise ValueError("TaylorModel.sqrt needs a positive expansion point; narrow the cell")
inv_c0 = c0.reciprocal()
shifted = [self.coeffs[0] - c0, *self.coeffs[1:]]
g = TaylorModel(self.center, self.radius, shifted, self.remainder) * inv_c0
tau = g.bound().mag
if tau >= 1.0:
raise ValueError(
"TaylorModel.sqrt series does not converge on this cell "
"(narrow the cell so the relative variation is < 1)"
)
series = TaylorModel.constant(1.0, self.center, self.radius, self.order)
gpow = TaylorModel.constant(1.0, self.center, self.radius, self.order)
coeff = Fraction(1, 1)
for k in range(1, self.order + 1):
coeff = coeff * (Fraction(1, 2) - (k - 1)) / k
gpow = gpow * g
series = series + gpow * Interval.from_rational(coeff)
next_coeff = abs(coeff * (Fraction(1, 2) - self.order) / (self.order + 1))
one_minus = Interval.point(1.0) - Interval.point(tau)
# (1 - tau)^{1/2 - (order+1)} = 1 / ((1 - tau)^order * sqrt(1 - tau))
denom = one_minus.pow_int(self.order) * one_minus.sqrt()
tail = float(
(
Interval.from_rational(next_coeff)
* Interval.point(tau).pow_int(self.order + 1)
* denom.reciprocal()
).hi
)
series = TaylorModel(
self.center,
self.radius,
series.coeffs,
series.remainder + Interval(-tail, tail),
)
return series * c0.sqrt()
def __truediv__(self, other: TaylorModel | IntervalLike) -> TaylorModel:
if isinstance(other, TaylorModel):
self._check(other)
return self * other.reciprocal()
return self * Interval.from_value(other).reciprocal()
def __repr__(self) -> str:
return (
f"TaylorModel(center={self.center!r}, radius={self.radius!r}, "
f"order={self.order}, remainder={self.remainder!r})"
)Other public import paths
omnibias.core.verified.TaylorModelomnibias.core.verified.taylor_model.TaylorModel